def jam_le

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

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/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

26def jam_le(+hh: Nat, +ll: Nat) -> {Nat.is_le(SW.jam(hh, ll), 1n+hh) == True{} : Bool}:
27  +tt = Nat.max(C.bit(hh), Nat.min(ll, 1n))
28  +h1 = WW.le_add_r(tt, 1n, Nat.double(C.half(hh)), FR.max_le1(C.bit(hh), ll, WW.bit_le1(hh)))
29  +h2 = N.le_add_left(Nat.double(C.half(hh)), hh, 1n, L.subst(Nat, z => {Nat.is_le(Nat.double(C.half(hh)), z) == True{} : Bool}, Nat.add(Nat.double(C.half(hh)), C.bit(hh)), hh, Equal.trans(Nat, Nat.add(Nat.double(C.half(hh)), C.bit(hh)), Nat.add(C.bit(hh), Nat.double(C.half(hh))), hh, NA.add_comm(Nat.double(C.half(hh)), C.bit(hh)), Equal.sym(Nat, hh, Nat.add(C.bit(hh), Nat.double(C.half(hh))), WW.hb(hh))), N.le_add_right(Nat.double(C.half(hh)), C.bit(hh))))
30  L.subst(Nat, z => {Nat.is_le(z, 1n+hh) == True{} : Bool}, Nat.add(tt, Nat.double(C.half(hh))), SW.jam(hh, ll), Equal.sym(Nat, SW.jam(hh, ll), Nat.add(tt, Nat.double(C.half(hh))), FR.jam_form(hh, ll)), N.le_trans(Nat.add(tt, Nat.double(C.half(hh))), Nat.add(1n, Nat.double(C.half(hh))), 1n+hh, h1, h2))