def rt_norm

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:248

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/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/math/typed/width.bend as WW
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/f64light.bend as FL
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/f64adda.bend as AA

248def rt_norm(+s: Bool, +E: Nat, +Fr: Nat, +one: Nat, +h1: {one == 1n : Nat}, +hE0: {Nat.is_eq(E, 0n) == False{} : Bool}, +hE: {Nat.is_lt(E, 2047n) == True{} : Bool}, +hF: {C.fits(52n, Fr) == True{} : Bool}) -> {SF.round(s, Nat.add(Fr, C.shift(52n, one)), Nat.add(1925n, E)) == SF.encode(s, E, Fr) : F.F64}:
249  +Mn = Nat.add(Fr, C.shift(52n, one))
250  +X0 = Nat.add(1925n, E)
251  +hz0 = Equal.trans(Bool, Nat.is_eq(Mn, 0n), Bool.and(Nat.is_eq(Fr, 0n), Nat.is_eq(one, 0n)), False{}, FB.z2(Fr, 52n, one), Equal.trans(Bool, Bool.and(Nat.is_eq(Fr, 0n), Nat.is_eq(one, 0n)), Bool.and(Nat.is_eq(Fr, 0n), False{}), False{}, Equal.cong(Nat, Bool, t => Bool.and(Nat.is_eq(Fr, 0n), Nat.is_eq(t, 0n)), one, 1n, h1), FR.and_f(Nat.is_eq(Fr, 0n))))
252  +ebl = FR.bl_c(52n, Mn, AA.n52(one, h1, Fr), AA.f53(one, h1, Fr, hF), Nat.cmp(M.bit_length(Mn), 53n), {==})
253  +emx = FR.max_l(X0, 1926n, FL.nz_le(E, hE0))
254  +e1 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.zero(s), SF.round_u(s, Mn, X0, Nat.max(Nat.sub(Nat.add(X0, M.bit_length(Mn)), 53n), Nat.sub(SF.zb(), 1074n)))), Nat.is_eq(Mn, 0n), False{}, hz0)
255  +e2 = Equal.cong(Nat, F.F64, t => SF.round_u(s, Mn, X0, Nat.max(Nat.sub(Nat.add(X0, t), 53n), 1926n)), M.bit_length(Mn), 53n, ebl)
256  +e3 = Equal.cong(Nat, F.F64, t => SF.round_u(s, Mn, X0, Nat.max(t, 1926n)), Nat.sub(Nat.add(X0, 53n), 53n), X0, FR.sub_add_l(X0, 53n))
257  +e4 = Equal.cong(Nat, F.F64, t => SF.round_u(s, Mn, X0, t), Nat.max(X0, 1926n), X0, emx)
258  +e5 = Equal.cong(Bool, F.F64, b => SF.pack(s, SF.pick(Nat, b, SF.rne(Mn, Nat.sub(X0, X0)), C.shift(Nat.sub(X0, X0), Mn)), X0), Nat.is_le(X0, X0), True{}, N.le_refl(X0))
259  +e6 = Equal.cong(Nat, F.F64, t => SF.pack(s, SF.rne(Mn, t), X0), Nat.sub(X0, X0), 0n, N.sub_self(X0))
260  +e7 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.pack_n(s, Mn, X0), SF.pack_e(s, Nat.sub(Nat.add(1n+X0, 1075n), SF.zb()), 0n)), C.fits(53n, Mn), True{}, AA.f53(one, h1, Fr, hF))
261  +e8 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.encode(s, 0n, Mn), SF.pack_e(s, Nat.sub(Nat.add(X0, 1075n), SF.zb()), C.low(52n, Mn))), C.fits(52n, Mn), False{}, AA.n52(one, h1, Fr))
262  +e9 = Equal.cong(Nat, F.F64, t => SF.pack_e(s, t, C.low(52n, Mn)), Nat.sub(Nat.add(X0, 1075n), SF.zb()), E, FR.sub_add_l(E, 1075n))
263  +e10 = Equal.cong(Nat, F.F64, t => SF.pack_e(s, E, t), C.low(52n, Mn), Fr, WW.low_u(52n, Fr, one, hF))
264  +e11 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.inf(s), SF.encode(s, E, Fr)), Nat.is_le(2047n, E), False{}, N.lt_not_le(E, 2047n, hE))
265  +r1 = SF.round_u(s, Mn, X0, Nat.max(Nat.sub(Nat.add(X0, M.bit_length(Mn)), 53n), 1926n))
266  +r2 = SF.round_u(s, Mn, X0, Nat.max(Nat.sub(Nat.add(X0, 53n), 53n), 1926n))
267  +r3 = SF.round_u(s, Mn, X0, Nat.max(X0, 1926n))
268  +r4 = SF.round_u(s, Mn, X0, X0)
269  +r5 = SF.pack(s, SF.rne(Mn, Nat.sub(X0, X0)), X0)
270  +r6 = SF.pack(s, Mn, X0)
271  +r7 = SF.pack_n(s, Mn, X0)
272  +r8 = SF.pack_e(s, Nat.sub(Nat.add(X0, 1075n), SF.zb()), C.low(52n, Mn))
273  +r9 = SF.pack_e(s, E, C.low(52n, Mn))
274  +r10 = SF.pack_e(s, E, Fr)
275  +G = SF.encode(s, E, Fr)
276  Equal.trans(F.F64, SF.round(s, Mn, X0), r1, G, e1, Equal.trans(F.F64, r1, r2, G, e2, Equal.trans(F.F64, r2, r3, G, e3, Equal.trans(F.F64, r3, r4, G, e4, Equal.trans(F.F64, r4, r5, G, e5, Equal.trans(F.F64, r5, r6, G, e6, Equal.trans(F.F64, r6, r7, G, e7, Equal.trans(F.F64, r7, r8, G, e8, Equal.trans(F.F64, r8, r9, G, e9, Equal.trans(F.F64, r9, r10, G, e10, e11))))))))))