def hlt2

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addb.bend:48

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/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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adds.bend as AS

48def hlt2(+one: Nat, +h1: {one == 1n : Nat}, +t: Nat, +S1: Nat, +d: Nat, +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}) -> {Nat.is_le(SW.jam(C.high(d, C.shift(10n, S1)), C.low(d, C.shift(10n, S1))), Nat.double(t)) == True{} : Bool}:
49  +S = C.shift(10n, S1)
50  +f62 = Equal.trans(Bool, C.fits(62n, C.high(d, S)), C.fits(Nat.add(d, 62n), S), True{}, Equal.sym(Bool, C.fits(Nat.add(d, 62n), S), C.fits(62n, C.high(d, S)), FR.fits_hc(d, 62n, S)), SH.fits_mono(63n, Nat.add(d, 62n), S, 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))
51  +P62 = C.shift(62n, one)
52  +hh = N.lt_le_trans(C.high(d, S), P62, Nat.double(t), Equal.trans(Bool, Nat.is_lt(C.high(d, S), P62), C.fits(62n, C.high(d, S)), True{}, FR.lt_fit(62n, one, h1, C.high(d, S)), 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)))
53  N.le_trans(SW.jam(C.high(d, S), C.low(d, S)), 1n+C.high(d, S), Nat.double(t), AS.jam_le(C.high(d, S), C.low(d, S)), N.lt_succ_le_succ(C.high(d, S), Nat.double(t), hh))