def n2

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64norm.bend:117

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/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
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/lib/u32half.bend as UH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend as CLZ
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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC

117# the exponent: norm_e + sa = xexp + 2171
118def n2(+ea: Nat, +fa: WU.U64, +E: Nat, +Fr: Nat, +hea: {ea == E : Nat}, +hfa: {SW.value(fa) == Fr : Nat}, +hF: {C.fits(52n, Fr) == True{} : Bool}, +hnz: {Bool.and(Nat.is_eq(E, 0n), Nat.is_eq(Fr, 0n)) == False{} : Bool}) -> {Nat.add(F.norm_e(ea, fa), sa(ea, fa)) == Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n) : Nat}:
119  match ea:
120    case 0n:
121      +ez = ez0(E, hea)
122      +hz = L.subst(Bool, t => {Bool.and(t, Nat.is_eq(Fr, 0n)) == False{} : Bool}, Nat.is_eq(E, 0n), True{}, ez, hnz)
123      +hb = BL.bl_le(52n, Fr, hF, Nat.is_le(M.bit_length(Fr), 52n), {==})
124      +ec = Equal.trans(Nat, X.clz(fa), Nat.sub(64n, M.bit_length(SW.value(fa))), Nat.sub(64n, M.bit_length(Fr)), CLZ.clz_value(fa), Equal.cong(Nat, Nat, z => Nat.sub(64n, M.bit_length(z)), SW.value(fa), Fr, hfa))
125      +h11 = L.subst(Nat, z => {Nat.is_le(11n, z) == True{} : Bool}, Nat.sub(64n, M.bit_length(Fr)), X.clz(fa), Equal.sym(Nat, X.clz(fa), Nat.sub(64n, M.bit_length(Fr)), ec), RT.le_sub(11n, M.bit_length(Fr), 64n, N.le_add_left(M.bit_length(Fr), 53n, 11n, N.le_trans(M.bit_length(Fr), 52n, 53n, hb, {==}))))
126      +h4108 = L.subst(Nat, z => {Nat.is_le(z, 4108n) == True{} : Bool}, Nat.sub(64n, M.bit_length(Fr)), X.clz(fa), Equal.sym(Nat, X.clz(fa), Nat.sub(64n, M.bit_length(Fr)), ec), N.le_trans(Nat.sub(64n, M.bit_length(Fr)), 64n, 4108n, UH.sub_le(64n, M.bit_length(Fr)), {==}))
127      +l1 = sub_sum(4108n, X.clz(fa), 11n, h11, h4108)
128      +r1 = Equal.cong(Bool, Nat, t => Nat.add(SF.pick(Nat, t, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), Nat.is_eq(E, 0n), True{}, ez)
129      Equal.trans(Nat, Nat.add(Nat.sub(4108n, X.clz(fa)), Nat.sub(X.clz(fa), 11n)), 4097n, Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), l1, Equal.sym(Nat, Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), 4097n, r1))
130    case 1n+ +p:
131      +ez = ezs(p, E, hea)
132      +r1 = Equal.cong(Bool, Nat, t => Nat.add(SF.pick(Nat, t, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), Nat.is_eq(E, 0n), False{}, ez)
133      +r2 = Equal.cong(Nat, Nat, z => Nat.add(z, 2171n), Nat.sub(Nat.add(E, SF.zb()), 1075n), Nat.add(1925n, E), FC.esub(E))
134      +r3 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(1925n, z), 2171n), E, 1n+p, Equal.sym(Nat, 1n+p, E, hea))
135      +r4 = Equal.cong(Nat, Nat, z => Nat.add(1926n, z), Nat.add(p, 2171n), Nat.add(2171n, p), NA.add_comm(p, 2171n))
136      +rr = Equal.trans(Nat, Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), Nat.add(Nat.sub(Nat.add(E, SF.zb()), 1075n), 2171n), Nat.add(4096n, 1n+p), r1, Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(E, SF.zb()), 1075n), 2171n), Nat.add(Nat.add(1925n, E), 2171n), Nat.add(4096n, 1n+p), r2, Equal.trans(Nat, Nat.add(Nat.add(1925n, E), 2171n), Nat.add(Nat.add(1925n, 1n+p), 2171n), Nat.add(4096n, 1n+p), r3, r4)))
137      Equal.trans(Nat, Nat.add(Nat.add(F.off(), 1n+p), 0n), Nat.add(4096n, 1n+p), Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), N.add_zero(Nat.add(F.off(), 1n+p)), Equal.sym(Nat, Nat.add(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 2171n), Nat.add(4096n, 1n+p), rr))