def jam_fits

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64rtools.bend:180

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

180def jam_fits(+a: Nat, +h: Nat, +l: Nat) -> {C.fits(1n+a, SW.jam(h, l)) == C.fits(1n+a, h) : Bool}:
181  +t = Nat.max(C.bit(h), Nat.min(l, 1n))
182  +e1 = Equal.cong(Nat, Bool, z => C.fits(1n+a, z), SW.jam(h, l), Nat.add(t, Nat.double(C.half(h))), FR.jam_form(h, l))
183  +e2 = fit_td(a, t, C.half(h), FR.max_le1(C.bit(h), l, WW.bit_le1(h)))
184  +e3 = Equal.sym(Bool, C.fits(1n+a, Nat.add(C.bit(h), Nat.double(C.half(h)))), C.fits(a, C.half(h)), fit_td(a, C.bit(h), C.half(h), WW.bit_le1(h)))
185  +e4 = Equal.cong(Nat, Bool, z => C.fits(1n+a, z), 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)))
186  Equal.trans(Bool, C.fits(1n+a, SW.jam(h, l)), C.fits(1n+a, Nat.add(t, Nat.double(C.half(h)))), C.fits(1n+a, h), e1, Equal.trans(Bool, C.fits(1n+a, Nat.add(t, Nat.double(C.half(h)))), C.fits(a, C.half(h)), C.fits(1n+a, h), e2, Equal.trans(Bool, C.fits(a, C.half(h)), C.fits(1n+a, Nat.add(C.bit(h), Nat.double(C.half(h)))), C.fits(1n+a, h), e3, e4)))