def p1_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64next.bend:219

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/src/math/f64.bend as F
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/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/f64bits.bend as FB
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

219def p1_c(+one: Nat, +h1: {one == 1n : Nat}, +x: F.F64, +hn: {SF.is_nan(x) == False{} : Bool}, +b: Bool, +hb: {Nat.is_eq(SF.efield(x), 2047n) == b : Bool}) -> {C.fits(63n, Nat.add(SF.pat(x), 1n)) == True{} : Bool}:
220  match b:
221    case True{}:
222      +E = SF.efield(x)
223      +Fr = SF.frac(x)
224      +S = C.shift(52n, E)
225      +fE = WW.low_fits(11n, C.high(20n, SF.hi_nat(x)))
226      +er = per1(x)
227      +hn2 = Equal.trans(Bool, Bool.not(Nat.is_eq(Fr, 0n)), SF.is_nan(x), False{}, Equal.sym(Bool, SF.is_nan(x), Bool.not(Nat.is_eq(Fr, 0n)), Equal.cong(Bool, Bool, t => Bool.and(t, Bool.not(Nat.is_eq(Fr, 0n))), Nat.is_eq(E, 2047n), True{}, hb)), hn)
228      +f0 = N.eq_from_is_eq(Fr, 0n, FR.not_f(Nat.is_eq(Fr, 0n), hn2))
229      +e1 = Equal.cong(Nat, Nat, t => Nat.add(Nat.add(t, 1n), S), Fr, 0n, f0)
230      +e2 = Equal.trans(Nat, Nat.add(SF.pat(x), 1n), Nat.add(Nat.add(Fr, 1n), S), Nat.add(1n, S), er, e1)
231      L.subst(Nat, t => {C.fits(63n, t) == True{} : Bool}, Nat.add(1n, S), Nat.add(SF.pat(x), 1n), Equal.sym(Nat, Nat.add(SF.pat(x), 1n), Nat.add(1n, S), e2), WW.limbs_fit(52n, 11n, 1n, E, {==}, fE))
232    case False{}:
233      +E = SF.efield(x)
234      +Fr = SF.frac(x)
235      +S = C.shift(52n, E)
236      +fE = WW.low_fits(11n, C.high(20n, SF.hi_nat(x)))
237      +er = per1(x)
238      +hlt0 = WW.lt_of_fits(11n, E, fE)
239      +hlt = Equal.trans(Bool, Nat.is_lt(E, 2047n), Bool.not(Nat.is_eq(E, 2047n)), True{}, FB.lt_ne(E, 2047n, hlt0), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_eq(E, 2047n), False{}, hb))
240      +f11a = WW.fits_of_lt(11n, 1n+E, hlt)
241      +f11 = L.subst(Nat, t => {C.fits(11n, Nat.add(t, E)) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), f11a)
242      +hF = Equal.trans(Bool, Nat.is_lt(Fr, C.shift(52n, one)), C.fits(52n, Fr), True{}, FR.lt_fit(52n, one, h1, Fr), frac52(x))
243      +h1a = FR.succ_le(Fr, C.shift(52n, one), hF)
244      +h2 = Equal.trans(Bool, Nat.is_le(Nat.add(Nat.add(Fr, 1n), S), Nat.add(C.shift(52n, one), S)), Nat.is_le(Nat.add(Fr, 1n), C.shift(52n, one)), True{}, FR.le_cancel_r(Nat.add(Fr, 1n), C.shift(52n, one), S), h1a)
245      +e3 = Equal.sym(Nat, C.shift(52n, Nat.add(one, E)), Nat.add(C.shift(52n, one), S), WW.shift_add(52n, one, E))
246      +h3 = L.subst(Nat, t => {Nat.is_le(Nat.add(Nat.add(Fr, 1n), S), t) == True{} : Bool}, Nat.add(C.shift(52n, one), S), C.shift(52n, Nat.add(one, E)), e3, h2)
247      +f3 = Equal.trans(Bool, C.fits(Nat.add(52n, 11n), C.shift(52n, Nat.add(one, E))), C.fits(11n, Nat.add(one, E)), True{}, RT.fits_sh(52n, 11n, Nat.add(one, E)), f11)
248      +f4 = SH.fits_lek(Nat.add(52n, 11n), Nat.add(Nat.add(Fr, 1n), S), C.shift(52n, Nat.add(one, E)), h3, f3)
249      L.subst(Nat, t => {C.fits(Nat.add(52n, 11n), t) == True{} : Bool}, Nat.add(Nat.add(Fr, 1n), S), Nat.add(SF.pat(x), 1n), Equal.sym(Nat, Nat.add(SF.pat(x), 1n), Nat.add(Nat.add(Fr, 1n), S), er), f4)