def on_gt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64ofnat.bend:60

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/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
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/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/f64rtools.bend as RT
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as BL

60# b > 63: a sticky jam of n >> (b - 63)
61def on_gt(+n: Nat, +hz: {Nat.is_eq(n, 0n) == False{} : Bool}, +hc: {Nat.is_le(M.bit_length(n), 63n) == False{} : Bool}) -> {F.round_pack(False{}, Nat.add(5117n, M.bit_length(n)), F.word64(F.jam_nat(Nat.sub(M.bit_length(n), 63n), n))) == SF.round(False{}, n, SF.zb()) : F.F64}:
62  +h63b = N.lt_le(63n, M.bit_length(n), N.not_le_lt(M.bit_length(n), 63n, hc))
63  +eb = N.sub_add(M.bit_length(n), 63n, h63b)
64  +ed63 = Equal.trans(Nat, Nat.add(Nat.sub(M.bit_length(n), 63n), 63n), Nat.add(63n, Nat.sub(M.bit_length(n), 63n)), M.bit_length(n), NA.add_comm(Nat.sub(M.bit_length(n), 63n), 63n), eb)
65  +epb = N.sub_add(M.bit_length(n), 1n, BL.bl_pos(n, hz, M.bit_length(n), {==}))
66  +ed62 = N.succ_inj(Nat.add(Nat.sub(M.bit_length(n), 63n), 62n), Nat.sub(M.bit_length(n), 1n), Equal.trans(Nat, 1n+Nat.add(Nat.sub(M.bit_length(n), 63n), 62n), Nat.add(Nat.sub(M.bit_length(n), 63n), 63n), 1n+Nat.sub(M.bit_length(n), 1n), Equal.sym(Nat, Nat.add(Nat.sub(M.bit_length(n), 63n), 63n), 1n+Nat.add(Nat.sub(M.bit_length(n), 63n), 62n), N.add_succ(Nat.sub(M.bit_length(n), 63n), 62n)), Equal.trans(Nat, Nat.add(Nat.sub(M.bit_length(n), 63n), 63n), M.bit_length(n), 1n+Nat.sub(M.bit_length(n), 1n), ed63, Equal.sym(Nat, 1n+Nat.sub(M.bit_length(n), 1n), M.bit_length(n), epb))))
67  +h = C.high(Nat.sub(M.bit_length(n), 63n), n)
68  +fh63 = Equal.trans(Bool, C.fits(63n, h), C.fits(Nat.add(Nat.sub(M.bit_length(n), 63n), 63n), n), True{}, Equal.sym(Bool, C.fits(Nat.add(Nat.sub(M.bit_length(n), 63n), 63n), n), C.fits(63n, h), FR.fits_hc(Nat.sub(M.bit_length(n), 63n), 63n, n)), L.subst(Nat, z => {C.fits(z, n) == True{} : Bool}, M.bit_length(n), Nat.add(Nat.sub(M.bit_length(n), 63n), 63n), Equal.sym(Nat, Nat.add(Nat.sub(M.bit_length(n), 63n), 63n), M.bit_length(n), ed63), RT.bl_fit(n)))
69  +fh62 = Equal.trans(Bool, C.fits(62n, h), C.fits(Nat.add(Nat.sub(M.bit_length(n), 63n), 62n), n), False{}, Equal.sym(Bool, C.fits(Nat.add(Nat.sub(M.bit_length(n), 63n), 62n), n), C.fits(62n, h), FR.fits_hc(Nat.sub(M.bit_length(n), 63n), 62n, n)), L.subst(Nat, z => {C.fits(z, n) == False{} : Bool}, Nat.sub(M.bit_length(n), 1n), Nat.add(Nat.sub(M.bit_length(n), 63n), 62n), Equal.sym(Nat, Nat.add(Nat.sub(M.bit_length(n), 63n), 62n), Nat.sub(M.bit_length(n), 1n), ed62), RT.bl_nfit(n, hz)))
70  +f63 = Equal.trans(Bool, C.fits(63n, SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n))), C.fits(63n, h), True{}, RT.jam_fits(62n, h, C.low(Nat.sub(M.bit_length(n), 63n), n)), fh63)
71  +t = Nat.max(C.bit(h), Nat.min(C.low(Nat.sub(M.bit_length(n), 63n), n), 1n))
72  +ejf = FR.jam_form(h, C.low(Nat.sub(M.bit_length(n), 63n), n))
73  +hhb = WW.le_add_r(C.bit(h), t, Nat.double(C.half(h)), RT.max_ge_l(C.bit(h), Nat.min(C.low(Nat.sub(M.bit_length(n), 63n), n), 1n)))
74  +hhJ = L.subst(Nat, z => {Nat.is_le(z, SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n))) == 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)), L.subst(Nat, z => {Nat.is_le(Nat.add(C.bit(h), Nat.double(C.half(h))), z) == True{} : Bool}, Nat.add(t, Nat.double(C.half(h))), SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n)), Equal.sym(Nat, SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n)), Nat.add(t, Nat.double(C.half(h))), ejf), hhb))
75  +f62 = FR.nfit(62n, h, SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n)), hhJ, fh62)
76  +ej = jn(Nat.sub(M.bit_length(n), 63n), n)
77  +ew = Equal.trans(Nat, SW.value(F.word64(F.jam_nat(Nat.sub(M.bit_length(n), 63n), n))), F.jam_nat(Nat.sub(M.bit_length(n), 63n), n), SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n)), BL.wval(F.jam_nat(Nat.sub(M.bit_length(n), 63n), n), SH.fits_mono(63n, 64n, F.jam_nat(Nat.sub(M.bit_length(n), 63n), n), {==}, L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n)), F.jam_nat(Nat.sub(M.bit_length(n), 63n), n), Equal.sym(Nat, F.jam_nat(Nat.sub(M.bit_length(n), 63n), n), SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n)), ej), f63))), ej)
78  +h62 = L.subst(Nat, z => {C.fits(62n, z) == False{} : Bool}, SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n)), SW.value(F.word64(F.jam_nat(Nat.sub(M.bit_length(n), 63n), n))), Equal.sym(Nat, SW.value(F.word64(F.jam_nat(Nat.sub(M.bit_length(n), 63n), n))), SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n)), ew), f62)
79  +h63 = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n)), SW.value(F.word64(F.jam_nat(Nat.sub(M.bit_length(n), 63n), n))), Equal.sym(Nat, SW.value(F.word64(F.jam_nat(Nat.sub(M.bit_length(n), 63n), n))), SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n)), ew), f63)
80  +r1 = FR.round_pack(False{}, Nat.add(5117n, M.bit_length(n)), F.word64(F.jam_nat(Nat.sub(M.bit_length(n), 63n), n)), Nat.add(2937n, M.bit_length(n)), hx(M.bit_length(n)), h62, h63)
81  +r2 = Equal.cong(Nat, F.F64, z => SF.round(False{}, z, Nat.add(2937n, M.bit_length(n))), SW.value(F.word64(F.jam_nat(Nat.sub(M.bit_length(n), 63n), n))), SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n)), ew)
82  +ex = Equal.trans(Nat, Nat.add(2937n, M.bit_length(n)), Nat.add(2937n, Nat.add(63n, Nat.sub(M.bit_length(n), 63n))), Nat.add(SF.zb(), Nat.sub(M.bit_length(n), 63n)), Equal.cong(Nat, Nat, z => Nat.add(2937n, z), M.bit_length(n), Nat.add(63n, Nat.sub(M.bit_length(n), 63n)), Equal.sym(Nat, Nat.add(63n, Nat.sub(M.bit_length(n), 63n)), M.bit_length(n), eb)), {==})
83  +r3 = Equal.cong(Nat, F.F64, z => SF.round(False{}, SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n)), z), Nat.add(2937n, M.bit_length(n)), Nat.add(SF.zb(), Nat.sub(M.bit_length(n), 63n)), ex)
84  +hb55 = L.subst(Nat, z => {Nat.is_le(Nat.add(Nat.sub(M.bit_length(n), 63n), 55n), z) == True{} : Bool}, Nat.add(Nat.sub(M.bit_length(n), 63n), 63n), M.bit_length(n), ed63, N.le_add_left(55n, 63n, Nat.sub(M.bit_length(n), 63n), {==}))
85  +r4 = Equal.sym(F.F64, SF.round(False{}, n, SF.zb()), SF.round(False{}, SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n)), Nat.add(SF.zb(), Nat.sub(M.bit_length(n), 63n))), RT.round_jam(False{}, Nat.sub(M.bit_length(n), 63n), n, SF.zb(), hb55))
86  Equal.trans(F.F64, F.round_pack(False{}, Nat.add(5117n, M.bit_length(n)), F.word64(F.jam_nat(Nat.sub(M.bit_length(n), 63n), n))), SF.round(False{}, SW.value(F.word64(F.jam_nat(Nat.sub(M.bit_length(n), 63n), n))), Nat.add(2937n, M.bit_length(n))), SF.round(False{}, n, SF.zb()), r1, Equal.trans(F.F64, SF.round(False{}, SW.value(F.word64(F.jam_nat(Nat.sub(M.bit_length(n), 63n), n))), Nat.add(2937n, M.bit_length(n))), SF.round(False{}, SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n)), Nat.add(2937n, M.bit_length(n))), SF.round(False{}, n, SF.zb()), r2, Equal.trans(F.F64, SF.round(False{}, SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n)), Nat.add(2937n, M.bit_length(n))), SF.round(False{}, SW.jam(C.high(Nat.sub(M.bit_length(n), 63n), n), C.low(Nat.sub(M.bit_length(n), 63n), n)), Nat.add(SF.zb(), Nat.sub(M.bit_length(n), 63n))), SF.round(False{}, n, SF.zb()), r3, r4)))