def jfit

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:831

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/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/w64sh.bend as SH

831def jfit(+d: Nat, +m: Nat, +hd: {Nat.is_le(1n, d) == True{} : Bool}, +h63: {C.fits(63n, m) == True{} : Bool}) -> {C.fits(63n, SW.jam(C.high(d, m), C.low(d, m))) == True{} : Bool}:
832  +h = C.high(d, m)
833  +t = Nat.max(C.bit(h), Nat.min(C.low(d, m), 1n))
834  +hle = L.subst(Nat, z => {Nat.is_le(63n, z) == True{} : Bool}, Nat.add(62n, d), Nat.add(d, 62n), NA.add_comm(62n, d), hd)
835  +fh = Equal.trans(Bool, C.fits(62n, h), C.fits(Nat.add(d, 62n), m), True{}, Equal.sym(Bool, C.fits(Nat.add(d, 62n), m), C.fits(62n, h), fits_hc(d, 62n, m)), SH.fits_mono(63n, Nat.add(d, 62n), m, hle, h63))
836  +fhh = SH.fits_lek(62n, C.half(h), h, half_le(h), fh)
837  +ft = small(t, max_le1(C.bit(h), C.low(d, m), WW.bit_le1(h)))
838  +f = WW.limbs_fit(1n, 62n, t, C.half(h), ft, fhh)
839  L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, Nat.add(t, Nat.double(C.half(h))), SW.jam(h, C.low(d, m)), Equal.sym(Nat, SW.jam(h, C.low(d, m)), Nat.add(t, Nat.double(C.half(h))), jam_form(h, C.low(d, m))), f)