def le_jam

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64tools.bend:107

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/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
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/f64rtools.bend as RT

107# h <= jam(h, l)
108def le_jam(+h: Nat, +l: Nat) -> {Nat.is_le(h, SW.jam(h, l)) == True{} : Bool}:
109  +t = Nat.max(C.bit(h), Nat.min(l, 1n))
110  +ejf = FR.jam_form(h, l)
111  +hhb = WW.le_add_r(C.bit(h), t, Nat.double(C.half(h)), RT.max_ge_l(C.bit(h), Nat.min(l, 1n)))
112  +h1 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(t, Nat.double(C.half(h)))) == True{} : Bool}, Nat.add(C.bit(h), Nat.double(C.half(h))), h, Equal.sym(Nat, h, Nat.add(C.bit(h), Nat.double(C.half(h))), WW.hb(h)), hhb)
113  L.subst(Nat, z => {Nat.is_le(h, z) == True{} : Bool}, Nat.add(t, Nat.double(C.half(h))), SW.jam(h, l), Equal.sym(Nat, SW.jam(h, l), Nat.add(t, Nat.double(C.half(h))), ejf), h1)