def hlt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64adds.bend:75

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

75def hlt(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +t: Nat, +S1: Nat, +d: Nat, +x0: Nat, +hsig: {SW.value(sig) == Nat.sub(Nat.double(t), SW.jam(C.high(d, C.shift(10n, S1)), C.low(d, C.shift(10n, S1)))) : Nat}, +he: {Nat.add(Nat.add(x0, d), 2180n) == e : Nat}, +hx63: {Nat.is_le(63n, Nat.add(x0, d)) == True{} : Bool}, +hd1: {Nat.is_le(1n, d) == True{} : Bool}, +hS: {C.fits(63n, C.shift(10n, S1)) == True{} : Bool}, +hT62: {C.fits(62n, Nat.double(t)) == False{} : Bool}, +hT63: {C.fits(63n, Nat.double(t)) == True{} : Bool}) -> {Nat.is_lt(C.high(d, C.shift(10n, S1)), Nat.double(t)) == True{} : Bool}:
76  +f62 = Equal.trans(Bool, C.fits(62n, C.high(d, C.shift(10n, S1))), C.fits(Nat.add(d, 62n), C.shift(10n, S1)), True{}, Equal.sym(Bool, C.fits(Nat.add(d, 62n), C.shift(10n, S1)), C.fits(62n, C.high(d, C.shift(10n, S1))), FR.fits_hc(d, 62n, C.shift(10n, S1))), SH.fits_mono(63n, Nat.add(d, 62n), C.shift(10n, S1), L.subst(Nat, z => {Nat.is_le(63n, z) == True{} : Bool}, Nat.add(62n, d), Nat.add(d, 62n), NA.add_comm(62n, d), N.le_add_left(1n, d, 62n, hd1)), hS))
77  +P62 = C.shift(62n, one)
78  N.lt_le_trans(C.high(d, C.shift(10n, S1)), P62, Nat.double(t), Equal.trans(Bool, Nat.is_lt(C.high(d, C.shift(10n, S1)), P62), C.fits(62n, C.high(d, C.shift(10n, S1))), True{}, FR.lt_fit(62n, one, h1, C.high(d, C.shift(10n, S1))), f62), N.not_lt_le(Nat.double(t), P62, Equal.trans(Bool, Nat.is_lt(Nat.double(t), P62), C.fits(62n, Nat.double(t)), False{}, FR.lt_fit(62n, one, h1, Nat.double(t)), hT62)))