proofs/math/typed/f64nrp.bend

bend-collections-laws-math@1.0.0.0 · 158 lines · 13 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
4import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
5import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
6import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
7import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
8import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
9import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
10import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
11import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
12import bend-collections-laws-math@1.0.0.0/proofs/lib/u32half.bend as UH
13import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend as CLZ
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
20import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
21import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as BL
22
23# SoftFloat's normRoundPackToF64: shift a nonzero significand up to bit 62
24# and round, or, when it has at most 53 bits and lands in the normal range,
25# pack it exactly. Either way it is the spec's round of the significand.
26
27def shl_v(+a: WU.U64, +k: Nat, +j: Nat, +hk: {Nat.is_lt(k, 64n) == True{} : Bool}, +hj: {Nat.is_le(Nat.add(k, j), 64n) == True{} : Bool}, +ha: {C.fits(j, SW.value(a)) == True{} : Bool}) -> {SW.value(X.shl(a, k)) == C.shift(k, SW.value(a)) : Nat}:
28  sv = SH.shl_value(a, k, hk)
29  +f = SH.fits_mono(Nat.add(k, j), 64n, C.shift(k, SW.value(a)), hj, Equal.trans(Bool, C.fits(Nat.add(k, j), C.shift(k, SW.value(a))), C.fits(j, SW.value(a)), True{}, RT.fits_sh(k, j, SW.value(a)), ha))
30  Equal.trans(Nat, SW.value(X.shl(a, k)), C.low(64n, C.shift(k, SW.value(a))), C.shift(k, SW.value(a)), sv, WW.low_fit(64n, C.shift(k, SW.value(a)), f))
31
32# a 53-bit q at ulp x' >= 1926 rounds to itself
33def rq(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +q: Nat, +xq: Nat, +h53: {C.fits(53n, q) == True{} : Bool}, +h52: {C.fits(52n, q) == False{} : Bool}, +hx: {Nat.is_le(1926n, xq) == True{} : Bool}, +hov: {Nat.is_lt(Nat.add(Nat.sub(xq, 1926n), 1n), 2047n) == True{} : Bool}) -> {SF.round(s, q, xq) == FR.bits(s, Nat.add(q, C.shift(52n, Nat.sub(xq, 1926n)))) : F.F64}:
34  +ebl = FR.bl_c(52n, q, h52, h53, Nat.cmp(M.bit_length(q), 53n), {==})
35  +eu0 = Equal.trans(Nat, Nat.sub(Nat.add(xq, M.bit_length(q)), 53n), Nat.sub(Nat.add(xq, 53n), 53n), xq, Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(xq, z), 53n), M.bit_length(q), 53n, ebl), FR.sub_add_l(xq, 53n))
36  +eu = Equal.trans(Nat, Nat.max(Nat.sub(Nat.add(xq, M.bit_length(q)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.max(xq, 1926n), xq, Equal.cong(Nat, Nat, z => Nat.max(z, 1926n), Nat.sub(Nat.add(xq, M.bit_length(q)), 53n), xq, eu0), FR.max_l(xq, 1926n, hx))
37  +hz = FR.nz_of(52n, q, h52)
38  +l1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.zero(s), SF.round_u(s, q, xq, Nat.max(Nat.sub(Nat.add(xq, M.bit_length(q)), 53n), Nat.sub(SF.zb(), 1074n)))), Nat.is_eq(q, 0n), False{}, hz)
39  +l2 = Equal.cong(Nat, F.F64, z => SF.round_u(s, q, xq, z), Nat.max(Nat.sub(Nat.add(xq, M.bit_length(q)), 53n), Nat.sub(SF.zb(), 1074n)), xq, eu)
40  +l3 = Equal.cong(Bool, F.F64, t => SF.pack(s, SF.pick(Nat, t, SF.rne(q, Nat.sub(xq, xq)), C.shift(Nat.sub(xq, xq), q)), xq), Nat.is_le(xq, xq), True{}, N.le_refl(xq))
41  +l4 = Equal.cong(Nat, F.F64, z => SF.pack(s, SF.rne(q, z), xq), Nat.sub(xq, xq), 0n, N.sub_self(xq))
42  +EF = Nat.sub(xq, 1926n)
43  +hEF = Equal.trans(Nat, Nat.add(EF, 1926n), Nat.add(1926n, EF), xq, NA.add_comm(EF, 1926n), N.sub_add(xq, 1926n, hx))
44  +hq = N.lt_le(q, C.shift(53n, one), Equal.trans(Bool, Nat.is_lt(q, C.shift(53n, one)), C.fits(53n, q), True{}, FR.lt_fit(53n, one, h1, q), h53))
45  +h0 = Equal.cong(Bool, Bool, t => Bool.or(Bool.not(t), Nat.is_eq(EF, 0n)), C.fits(52n, q), False{}, h52)
46  +hov2 = L.subst(Nat, z => {Nat.is_lt(Nat.add(EF, z), 2047n) == True{} : Bool}, 1n, SF.pick(Nat, C.fits(53n, q), 1n, 2n), Equal.sym(Nat, SF.pick(Nat, C.fits(53n, q), 1n, 2n), 1n, Equal.cong(Bool, Nat, t => SF.pick(Nat, t, 1n, 2n), C.fits(53n, q), True{}, h53)), hov)
47  +l5 = FR.pkg(one, h1, s, q, xq, EF, hEF, hq, h0, hov2)
48  Equal.trans(F.F64, SF.round(s, q, xq), SF.round_u(s, q, xq, Nat.max(Nat.sub(Nat.add(xq, M.bit_length(q)), 53n), Nat.sub(SF.zb(), 1074n))), FR.bits(s, Nat.add(q, C.shift(52n, EF))), l1, Equal.trans(F.F64, SF.round_u(s, q, xq, Nat.max(Nat.sub(Nat.add(xq, M.bit_length(q)), 53n), Nat.sub(SF.zb(), 1074n))), SF.round_u(s, q, xq, xq), FR.bits(s, Nat.add(q, C.shift(52n, EF))), l2, Equal.trans(F.F64, SF.round_u(s, q, xq, xq), SF.pack(s, SF.rne(q, Nat.sub(xq, xq)), xq), FR.bits(s, Nat.add(q, C.shift(52n, EF))), l3, Equal.trans(F.F64, SF.pack(s, SF.rne(q, Nat.sub(xq, xq)), xq), SF.pack(s, q, xq), FR.bits(s, Nat.add(q, C.shift(52n, EF))), l4, l5))))
49
50# the top bits of shift(k, V) when k + bit_length(V) = J
51def tbf(+k: Nat, +V: Nat, +J: Nat, +ek: {Nat.add(k, M.bit_length(V)) == J : Nat}) -> {C.fits(J, C.shift(k, V)) == True{} : Bool}:
52  L.subst(Nat, z => {C.fits(z, C.shift(k, V)) == True{} : Bool}, Nat.add(k, M.bit_length(V)), J, ek, Equal.trans(Bool, C.fits(Nat.add(k, M.bit_length(V)), C.shift(k, V)), C.fits(M.bit_length(V), V), True{}, RT.fits_sh(k, M.bit_length(V), V), RT.bl_fit(V)))
53
54def tbn(+k: Nat, +V: Nat, +K: Nat, +hz: {Nat.is_eq(V, 0n) == False{} : Bool}, +ek: {Nat.add(k, M.bit_length(V)) == 1n+K : Nat}) -> {C.fits(K, C.shift(k, V)) == False{} : Bool}:
55  +epb = N.sub_add(M.bit_length(V), 1n, BL.bl_pos(V, hz, M.bit_length(V), {==}))
56  +K2 = Nat.add(k, Nat.sub(M.bit_length(V), 1n))
57  +e2 = N.succ_inj(K2, K, Equal.trans(Nat, 1n+K2, Nat.add(k, 1n+Nat.sub(M.bit_length(V), 1n)), 1n+K, Equal.sym(Nat, Nat.add(k, 1n+Nat.sub(M.bit_length(V), 1n)), 1n+K2, N.add_succ(k, Nat.sub(M.bit_length(V), 1n))), Equal.trans(Nat, Nat.add(k, 1n+Nat.sub(M.bit_length(V), 1n)), Nat.add(k, M.bit_length(V)), 1n+K, Equal.cong(Nat, Nat, z => Nat.add(k, z), 1n+Nat.sub(M.bit_length(V), 1n), M.bit_length(V), epb), ek)))
58  +hql = L.subst(Nat, z => {Nat.is_le(z, C.shift(k, V)) == True{} : Bool}, C.shift(k, C.pow2(Nat.sub(M.bit_length(V), 1n))), C.pow2(K2), WW.shift_pow2(k, Nat.sub(M.bit_length(V), 1n)), WW.shift_mono(k, C.pow2(Nat.sub(M.bit_length(V), 1n)), V, BL.lower(V, hz)))
59  +nf = Equal.trans(Bool, C.fits(K2, C.pow2(K2)), Nat.is_lt(C.pow2(K2), C.pow2(K2)), False{}, WW.fits_lt(K2, C.pow2(K2)), N.lt_irrefl(C.pow2(K2)))
60  L.subst(Nat, z => {C.fits(z, C.shift(k, V)) == False{} : Bool}, K2, K, e2, FR.nfit(K2, C.pow2(K2), C.shift(k, V), hql, nf))
61
62def esd(+sig: WU.U64, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}) -> {Nat.sub(X.clz(sig), 1n) == Nat.sub(63n, M.bit_length(SW.value(sig))) : Nat}:
63  +hb = BL.bl_le(63n, SW.value(sig), h63, Nat.is_le(M.bit_length(SW.value(sig)), 63n), {==})
64  ec = CLZ.clz_value(sig)
65  Equal.trans(Nat, Nat.sub(X.clz(sig), 1n), Nat.sub(Nat.sub(64n, M.bit_length(SW.value(sig))), 1n), Nat.sub(63n, M.bit_length(SW.value(sig))), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), X.clz(sig), Nat.sub(64n, M.bit_length(SW.value(sig))), ec), Equal.trans(Nat, Nat.sub(Nat.sub(64n, M.bit_length(SW.value(sig))), 1n), Nat.sub(Nat.add(1n, Nat.sub(63n, M.bit_length(SW.value(sig)))), 1n), Nat.sub(63n, M.bit_length(SW.value(sig))), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), Nat.sub(64n, M.bit_length(SW.value(sig))), Nat.add(1n, Nat.sub(63n, M.bit_length(SW.value(sig)))), FR.sub_add_a(1n, 63n, M.bit_length(SW.value(sig)), hb)), N.add_sub_cancel(1n, Nat.sub(63n, M.bit_length(SW.value(sig))))))
66
67def sdb(+sig: WU.U64, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}) -> {Nat.add(Nat.sub(X.clz(sig), 1n), M.bit_length(SW.value(sig))) == 63n : Nat}:
68  +hb = BL.bl_le(63n, SW.value(sig), h63, Nat.is_le(M.bit_length(SW.value(sig)), 63n), {==})
69  Equal.trans(Nat, Nat.add(Nat.sub(X.clz(sig), 1n), M.bit_length(SW.value(sig))), Nat.add(Nat.sub(63n, M.bit_length(SW.value(sig))), M.bit_length(SW.value(sig))), 63n, Equal.cong(Nat, Nat, z => Nat.add(z, M.bit_length(SW.value(sig))), Nat.sub(X.clz(sig), 1n), Nat.sub(63n, M.bit_length(SW.value(sig))), esd(sig, h63)), Equal.trans(Nat, Nat.add(Nat.sub(63n, M.bit_length(SW.value(sig))), M.bit_length(SW.value(sig))), Nat.add(M.bit_length(SW.value(sig)), Nat.sub(63n, M.bit_length(SW.value(sig)))), 63n, NA.add_comm(Nat.sub(63n, M.bit_length(SW.value(sig))), M.bit_length(SW.value(sig))), N.sub_add(63n, M.bit_length(SW.value(sig)), hb)))
70
71def sd_le(+sig: WU.U64, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}) -> {Nat.is_le(Nat.sub(X.clz(sig), 1n), 63n) == True{} : Bool}:
72  L.subst(Nat, z => {Nat.is_le(z, 63n) == True{} : Bool}, Nat.sub(63n, M.bit_length(SW.value(sig))), Nat.sub(X.clz(sig), 1n), Equal.sym(Nat, Nat.sub(X.clz(sig), 1n), Nat.sub(63n, M.bit_length(SW.value(sig))), esd(sig, h63)), UH.sub_le(63n, M.bit_length(SW.value(sig))))
73
74# the rounding branch
75def nrp_r(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +hz: {Nat.is_eq(SW.value(sig), 0n) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +hx63: {Nat.is_le(63n, x) == True{} : Bool}) -> {F.round_pack(s, Nat.sub(e, Nat.sub(X.clz(sig), 1n)), X.shl(sig, Nat.sub(X.clz(sig), 1n))) == SF.round(s, SW.value(sig), x) : F.F64}:
76  +k = Nat.sub(X.clz(sig), 1n)
77  +ek = sdb(sig, h63)
78  +hk = N.le_lt_trans(k, 63n, 64n, sd_le(sig, h63), {==})
79  +ev = shl_v(sig, k, M.bit_length(SW.value(sig)), hk, L.subst(Nat, z => {Nat.is_le(z, 64n) == True{} : Bool}, 63n, Nat.add(k, M.bit_length(SW.value(sig))), Equal.sym(Nat, Nat.add(k, M.bit_length(SW.value(sig))), 63n, ek), {==}), RT.bl_fit(SW.value(sig)))
80  +f63 = tbf(k, SW.value(sig), 63n, ek)
81  +f62 = tbn(k, SW.value(sig), 62n, hz, ek)
82  +h62v = L.subst(Nat, z => {C.fits(62n, z) == False{} : Bool}, C.shift(k, SW.value(sig)), SW.value(X.shl(sig, k)), Equal.sym(Nat, SW.value(X.shl(sig, k)), C.shift(k, SW.value(sig)), ev), f62)
83  +h63v = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, C.shift(k, SW.value(sig)), SW.value(X.shl(sig, k)), Equal.sym(Nat, SW.value(X.shl(sig, k)), C.shift(k, SW.value(sig)), ev), f63)
84  +hkx = N.le_trans(k, 63n, x, sd_le(sig, h63), hx63)
85  +exk = Equal.sym(Nat, Nat.sub(e, k), Nat.add(Nat.sub(x, k), 2180n), Equal.trans(Nat, Nat.sub(e, k), Nat.sub(Nat.add(x, 2180n), k), Nat.add(Nat.sub(x, k), 2180n), Equal.cong(Nat, Nat, z => Nat.sub(z, k), e, Nat.add(x, 2180n), Equal.sym(Nat, Nat.add(x, 2180n), e, hx)), FR.sub_add_r(x, 2180n, k, hkx)))
86  +r1 = FR.round_pack(s, Nat.sub(e, k), X.shl(sig, k), Nat.sub(x, k), exk, h62v, h63v)
87  +r2 = Equal.cong(Nat, F.F64, z => SF.round(s, z, Nat.sub(x, k)), SW.value(X.shl(sig, k)), C.shift(k, SW.value(sig)), ev)
88  +r3 = RT.round_shift(s, k, SW.value(sig), Nat.sub(x, k))
89  +r4 = Equal.cong(Nat, F.F64, z => SF.round(s, SW.value(sig), z), Nat.add(Nat.sub(x, k), k), x, Equal.trans(Nat, Nat.add(Nat.sub(x, k), k), Nat.add(k, Nat.sub(x, k)), x, NA.add_comm(Nat.sub(x, k), k), N.sub_add(x, k, hkx)))
90  Equal.trans(F.F64, F.round_pack(s, Nat.sub(e, k), X.shl(sig, k)), SF.round(s, SW.value(X.shl(sig, k)), Nat.sub(x, k)), SF.round(s, SW.value(sig), x), r1, Equal.trans(F.F64, SF.round(s, SW.value(X.shl(sig, k)), Nat.sub(x, k)), SF.round(s, C.shift(k, SW.value(sig)), Nat.sub(x, k)), SF.round(s, SW.value(sig), x), r2, Equal.trans(F.F64, SF.round(s, C.shift(k, SW.value(sig)), Nat.sub(x, k)), SF.round(s, SW.value(sig), Nat.add(Nat.sub(x, k), k)), SF.round(s, SW.value(sig), x), r3, r4)))
91
92def and_l(+a: Bool, +b: Bool, +h: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
93  match a:
94    case True{}:
95      {==}
96    case False{}:
97      NC.absurd_tf({False{} == True{} : Bool}, h)
98
99def and_r(+a: Bool, +b: Bool, +h: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
100  match a:
101    case True{}:
102      h
103    case False{}:
104      NC.absurd_tf({b == True{} : Bool}, h)
105
106# the exact branch: at most 53 bits, landing in the normal range
107def nrp_d(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +hz: {Nat.is_eq(SW.value(sig), 0n) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +hx63: {Nat.is_le(63n, x) == True{} : Bool}, +h10: {Nat.is_le(10n, Nat.sub(X.clz(sig), 1n)) == True{} : Bool}, +hoff: {Nat.is_le(Nat.add(F.off(), Nat.sub(X.clz(sig), 1n)), e) == True{} : Bool}, +hov: {Nat.is_lt(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), Nat.add(F.off(), 2045n)) == True{} : Bool}) -> {F.pack(s, F.nrp_exp(e, Nat.sub(X.clz(sig), 1n), X.is_zero(sig)), X.shl(sig, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))) == SF.round(s, SW.value(sig), x) : F.F64}:
108  +k = Nat.sub(X.clz(sig), 1n)
109  +ez = Equal.trans(Bool, X.is_zero(sig), Nat.is_eq(SW.value(sig), 0n), False{}, WA.is_zero_value(sig), hz)
110  +i1 = Equal.cong(Bool, F.F64, t => F.pack(s, F.nrp_exp(e, k, t), X.shl(sig, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), X.is_zero(sig), False{}, ez)
111  +ek = sdb(sig, h63)
112  +ek0 = N.sub_add(k, 10n, h10)
113  +ek10 = A.add_cancel_r(Nat.add(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), M.bit_length(SW.value(sig))), 53n, 10n, Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), M.bit_length(SW.value(sig))), 10n), Nat.add(Nat.add(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), 10n), M.bit_length(SW.value(sig))), 63n, A.add_rot(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), M.bit_length(SW.value(sig)), 10n), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), 10n), M.bit_length(SW.value(sig))), Nat.add(k, M.bit_length(SW.value(sig))), 63n, Equal.cong(Nat, Nat, w => Nat.add(w, M.bit_length(SW.value(sig))), Nat.add(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), 10n), k, Equal.trans(Nat, Nat.add(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), 10n), Nat.add(10n, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), k, NA.add_comm(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), 10n), ek0)), ek)))
114  +hk10 = N.le_lt_trans(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), 53n, 64n, L.subst(Nat, w => {Nat.is_le(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), w) == True{} : Bool}, Nat.add(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), M.bit_length(SW.value(sig))), 53n, ek10, N.le_add_right(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), M.bit_length(SW.value(sig)))), {==})
115  +eq = shl_v(sig, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), M.bit_length(SW.value(sig)), hk10, L.subst(Nat, w => {Nat.is_le(w, 64n) == True{} : Bool}, 53n, Nat.add(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), M.bit_length(SW.value(sig))), Equal.sym(Nat, Nat.add(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), M.bit_length(SW.value(sig))), 53n, ek10), {==}), RT.bl_fit(SW.value(sig)))
116  +h53 = tbf(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig), 53n, ek10)
117  +h52 = tbn(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig), 52n, hz, ek10)
118  +hkx = N.le_trans(k, 63n, x, sd_le(sig, h63), hx63)
119  +ex = N.sub_add(x, k, hkx)
120  +eek = Equal.trans(Nat, Nat.sub(e, k), Nat.sub(Nat.add(x, 2180n), k), Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 2180n), Equal.cong(Nat, Nat, w => Nat.sub(w, k), e, Nat.add(x, 2180n), Equal.sym(Nat, Nat.add(x, 2180n), e, hx)), FR.sub_add_r(x, 2180n, k, hkx))
121  +hw = L.subst(Nat, w => {Nat.is_le(4096n, w) == True{} : Bool}, Nat.sub(e, k), Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 2180n), eek, RT.le_sub(4096n, k, e, L.subst(Nat, w => {Nat.is_le(w, e) == True{} : Bool}, Nat.add(F.off(), k), Nat.add(4096n, k), {==}, hoff)))
122  +hy = Equal.trans(Bool, Nat.is_le(1916n, Nat.sub(x, Nat.sub(X.clz(sig), 1n))), Nat.is_le(Nat.add(1916n, 2180n), Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 2180n)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(1916n, 2180n), Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 2180n)), Nat.is_le(1916n, Nat.sub(x, Nat.sub(X.clz(sig), 1n))), FR.le_cancel_r(1916n, Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 2180n)), hw)
123  +ey = N.sub_add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n, hy)
124  +eE = Equal.trans(Nat, Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off()), Nat.sub(Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 2180n), F.off()), Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), Equal.cong(Nat, Nat, w => Nat.sub(w, F.off()), Nat.sub(e, k), Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 2180n), eek), Equal.trans(Nat, Nat.sub(Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 2180n), F.off()), Nat.sub(Nat.add(Nat.add(1916n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), 2180n), F.off()), Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), Equal.cong(Nat, Nat, w => Nat.sub(Nat.add(w, 2180n), F.off()), Nat.sub(x, Nat.sub(X.clz(sig), 1n)), Nat.add(1916n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), Equal.sym(Nat, Nat.add(1916n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), Nat.sub(x, Nat.sub(X.clz(sig), 1n)), ey)), Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(1916n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), 2180n), F.off()), Nat.sub(Nat.add(4096n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), 4096n), Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), Equal.cong(Nat, Nat, w => Nat.sub(1916n+w, F.off()), Nat.add(Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), 2180n), Nat.add(2180n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), NA.add_comm(Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), 2180n)), N.add_sub_cancel(4096n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)))))
125  +exq = Equal.trans(Nat, Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.sub(Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), k), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.add(1926n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), Equal.cong(Nat, Nat, w => Nat.sub(w, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), x, Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), k), Equal.sym(Nat, Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), k), x, Equal.trans(Nat, Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), k), Nat.add(k, Nat.sub(x, Nat.sub(X.clz(sig), 1n))), x, NA.add_comm(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), k), ex))), Equal.trans(Nat, Nat.sub(Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), k), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.sub(Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), Nat.add(10n, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.add(1926n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), Equal.cong(Nat, Nat, w => Nat.sub(Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), w), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), k, Nat.add(10n, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Equal.sym(Nat, Nat.add(10n, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), k, ek0)), Equal.trans(Nat, Nat.sub(Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), Nat.add(10n, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.sub(Nat.add(Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 10n), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.add(1926n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), Equal.cong(Nat, Nat, w => Nat.sub(w, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), Nat.add(10n, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), Nat.add(Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 10n), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 10n), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), Nat.add(10n, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), NA.add_assoc(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 10n, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)))), Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 10n), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 10n), Nat.add(1926n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), FR.sub_add_l(Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 10n), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Equal.trans(Nat, Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 10n), Nat.add(Nat.add(1916n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), 10n), Nat.add(1926n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), Equal.cong(Nat, Nat, w => Nat.add(w, 10n), Nat.sub(x, Nat.sub(X.clz(sig), 1n)), Nat.add(1916n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), Equal.sym(Nat, Nat.add(1916n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), Nat.sub(x, Nat.sub(X.clz(sig), 1n)), ey)), Equal.cong(Nat, Nat, w => 1916n+w, Nat.add(Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), 10n), Nat.add(10n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), NA.add_comm(Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), 10n)))))))
126  +exz = Equal.trans(Nat, Nat.sub(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), 1926n), Nat.sub(Nat.add(1926n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), 1926n), Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), Equal.cong(Nat, Nat, w => Nat.sub(w, 1926n), Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.add(1926n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), exq), N.add_sub_cancel(1926n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)))
127  +hz45 = Equal.trans(Bool, Nat.is_lt(Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), 2045n), Nat.is_lt(Nat.add(4096n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), Nat.add(4096n, 2045n)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(4096n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), Nat.add(4096n, 2045n)), Nat.is_lt(Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), 2045n), WW.lt_cancel_l(4096n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), 2045n)), L.subst(Nat, w => {Nat.is_lt(w, 6141n) == True{} : Bool}, Nat.sub(e, k), Nat.add(4096n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), Equal.trans(Nat, Nat.sub(e, k), Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 2180n), Nat.add(4096n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), eek, Equal.trans(Nat, Nat.add(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 2180n), Nat.add(Nat.add(1916n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), 2180n), Nat.add(4096n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), Equal.cong(Nat, Nat, w => Nat.add(w, 2180n), Nat.sub(x, Nat.sub(X.clz(sig), 1n)), Nat.add(1916n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), Equal.sym(Nat, Nat.add(1916n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), Nat.sub(x, Nat.sub(X.clz(sig), 1n)), ey)), Equal.cong(Nat, Nat, w => 1916n+w, Nat.add(Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), 2180n), Nat.add(2180n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), NA.add_comm(Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), 2180n)))), hov))
128  +hz1 = Equal.trans(Bool, Nat.is_lt(Nat.add(Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), 1n), 2047n), Nat.is_lt(Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), 2046n), True{}, WW.lt_cancel_r(Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), 2046n, 1n), N.lt_trans(Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), 2045n, 2046n, hz45, {==}))
129  +hxq = L.subst(Nat, w => {Nat.is_le(1926n, w) == True{} : Bool}, Nat.add(1926n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Equal.sym(Nat, Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.add(1926n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)), exq), N.le_add_right(1926n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n)))
130  +hovq = L.subst(Nat, w => {Nat.is_lt(Nat.add(w, 1n), 2047n) == True{} : Bool}, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), Nat.sub(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), 1926n), Equal.sym(Nat, Nat.sub(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), 1926n), Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), exz), hz1)
131  +fE = L.subst(Nat, w => {C.fits(11n, w) == True{} : Bool}, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off()), Equal.sym(Nat, Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off()), Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), eE), WW.fits_of_lt(11n, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), N.lt_trans(Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), 2045n, 2048n, hz45, {==})))
132  +hq = N.lt_le(C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), C.shift(53n, one), Equal.trans(Bool, Nat.is_lt(C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), C.shift(53n, one)), C.fits(53n, C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig))), True{}, FR.lt_fit(53n, one, h1, C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig))), h53))
133  +hovE = L.subst(Nat, w => {Nat.is_lt(Nat.add(Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off()), w), 2047n) == True{} : Bool}, 1n, SF.pick(Nat, C.fits(53n, C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig))), 1n, 2n), Equal.sym(Nat, SF.pick(Nat, C.fits(53n, C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig))), 1n, 2n), 1n, Equal.cong(Bool, Nat, t => SF.pick(Nat, t, 1n, 2n), C.fits(53n, C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig))), True{}, h53)), L.subst(Nat, w => {Nat.is_lt(Nat.add(w, 1n), 2047n) == True{} : Bool}, Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off()), Equal.sym(Nat, Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off()), Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), eE), hz1))
134  +hn0 = FR.qfit(one, h1, C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off()), hq, h52, hovE)
135  +hn = L.subst(Nat, w => {C.fits(63n, Nat.add(w, C.shift(52n, Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off())))) == True{} : Bool}, C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), SW.value(X.shl(sig, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), Equal.sym(Nat, SW.value(X.shl(sig, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), eq), hn0)
136  +i2 = FR.pack_v(s, Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off()), fE, X.shl(sig, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), hn)
137  +i3 = Equal.cong(Nat, F.F64, w => FR.bits(s, Nat.add(w, C.shift(52n, Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off())))), SW.value(X.shl(sig, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), eq)
138  +i4 = Equal.cong(Nat, F.F64, w => FR.bits(s, Nat.add(C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), C.shift(52n, w))), Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off()), Nat.sub(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), 1926n), Equal.trans(Nat, Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off()), Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), Nat.sub(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), 1926n), eE, Equal.sym(Nat, Nat.sub(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), 1926n), Nat.sub(Nat.sub(x, Nat.sub(X.clz(sig), 1n)), 1916n), exz)))
139  +exk = Equal.trans(Nat, Nat.add(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.add(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), x, NA.add_comm(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), N.sub_add(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), N.le_trans(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), k, x, UH.sub_le(k, 10n), hkx)))
140  +s1 = Equal.cong(Nat, F.F64, w => SF.round(s, SW.value(sig), w), x, Nat.add(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Equal.sym(Nat, Nat.add(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), x, exk))
141  +s2 = Equal.sym(F.F64, SF.round(s, C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), SF.round(s, SW.value(sig), Nat.add(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), RT.round_shift(s, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig), Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))))
142  +s3 = rq(one, h1, s, C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), h53, h52, hxq, hovq)
143  +sp = Equal.trans(F.F64, SF.round(s, SW.value(sig), x), SF.round(s, SW.value(sig), Nat.add(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), FR.bits(s, Nat.add(C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), C.shift(52n, Nat.sub(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), 1926n)))), s1, Equal.trans(F.F64, SF.round(s, SW.value(sig), Nat.add(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), SF.round(s, C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), FR.bits(s, Nat.add(C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), C.shift(52n, Nat.sub(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), 1926n)))), s2, s3))
144  +im = Equal.trans(F.F64, F.pack(s, F.nrp_exp(e, k, X.is_zero(sig)), X.shl(sig, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), F.pack(s, Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off()), X.shl(sig, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), FR.bits(s, Nat.add(C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), C.shift(52n, Nat.sub(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), 1926n)))), i1, Equal.trans(F.F64, F.pack(s, Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off()), X.shl(sig, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), FR.bits(s, Nat.add(SW.value(X.shl(sig, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), C.shift(52n, Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off())))), FR.bits(s, Nat.add(C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), C.shift(52n, Nat.sub(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), 1926n)))), i2, Equal.trans(F.F64, FR.bits(s, Nat.add(SW.value(X.shl(sig, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), C.shift(52n, Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off())))), FR.bits(s, Nat.add(C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), C.shift(52n, Nat.sub(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), F.off())))), FR.bits(s, Nat.add(C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), C.shift(52n, Nat.sub(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), 1926n)))), i3, i4)))
145  Equal.trans(F.F64, F.pack(s, F.nrp_exp(e, k, X.is_zero(sig)), X.shl(sig, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n))), FR.bits(s, Nat.add(C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), C.shift(52n, Nat.sub(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), 1926n)))), SF.round(s, SW.value(sig), x), im, Equal.sym(F.F64, SF.round(s, SW.value(sig), x), FR.bits(s, Nat.add(C.shift(Nat.sub(Nat.sub(X.clz(sig), 1n), 10n), SW.value(sig)), C.shift(52n, Nat.sub(Nat.sub(x, Nat.sub(Nat.sub(X.clz(sig), 1n), 10n)), 1926n)))), sp))
146
147def nrp_c(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +hz: {Nat.is_eq(SW.value(sig), 0n) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +hx63: {Nat.is_le(63n, x) == True{} : Bool}, +d: Bool, +hd: {Bool.and(Nat.is_le(10n, Nat.sub(X.clz(sig), 1n)), Bool.and(Nat.is_le(Nat.add(F.off(), Nat.sub(X.clz(sig), 1n)), e), Nat.is_lt(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), Nat.add(F.off(), 2045n)))) == d : Bool}) -> {F.nrp_pick(s, e, sig, Nat.sub(X.clz(sig), 1n), d) == SF.round(s, SW.value(sig), x) : F.F64}:
148  match d:
149    case True{}:
150      +ha = and_l(Nat.is_le(10n, Nat.sub(X.clz(sig), 1n)), Bool.and(Nat.is_le(Nat.add(F.off(), Nat.sub(X.clz(sig), 1n)), e), Nat.is_lt(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), Nat.add(F.off(), 2045n))), hd)
151      +hb = and_r(Nat.is_le(10n, Nat.sub(X.clz(sig), 1n)), Bool.and(Nat.is_le(Nat.add(F.off(), Nat.sub(X.clz(sig), 1n)), e), Nat.is_lt(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), Nat.add(F.off(), 2045n))), hd)
152      nrp_d(one, h1, s, e, sig, x, hx, hz, h63, hx63, ha, and_l(Nat.is_le(Nat.add(F.off(), Nat.sub(X.clz(sig), 1n)), e), Nat.is_lt(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), Nat.add(F.off(), 2045n)), hb), and_r(Nat.is_le(Nat.add(F.off(), Nat.sub(X.clz(sig), 1n)), e), Nat.is_lt(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), Nat.add(F.off(), 2045n)), hb))
153    case False{}:
154      nrp_r(one, h1, s, e, sig, x, hx, hz, h63, hx63)
155
156# SoftFloat's normRoundPackToF64 is round
157def nrp(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +hz: {Nat.is_eq(SW.value(sig), 0n) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +hx63: {Nat.is_le(63n, x) == True{} : Bool}) -> {F.norm_round_pack(s, e, sig) == SF.round(s, SW.value(sig), x) : F.F64}:
158  nrp_c(one, h1, s, e, sig, x, hx, hz, h63, hx63, Bool.and(Nat.is_le(10n, Nat.sub(X.clz(sig), 1n)), Bool.and(Nat.is_le(Nat.add(F.off(), Nat.sub(X.clz(sig), 1n)), e), Nat.is_lt(Nat.sub(e, Nat.sub(X.clz(sig), 1n)), Nat.add(F.off(), 2045n)))), {==})