proofs/math/typed/f64rtools.bend

bend-collections-laws-math@1.0.0.0 · 244 lines · 22 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/natural.bend as M
7import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
9import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
10import bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend as BT
11import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as FO
15
16# Two facts about the spec's round (Flocq's round_NE is invariant under
17# exact scaling, and the sticky bit summarizes everything below two guard
18# bits: Boldo and Melquiond's inbetween lemmas, the correctness argument of
19# SoftFloat's shiftRightJam):
20#   round(s, m * 2^k, x) = round(s, m, x + k)
21#   round(s, m, x) = round(s, jam(m >> d, m mod 2^d), x + d)   when m has
22#     at least d + 55 bits
23
24# ---- rounding an exact multiple ----
25
26def lt0f(+h: Nat) -> {Nat.is_lt(h, 0n) == False{} : Bool}:
27  N.not_lt_zero(h)
28
29def rne_exact(+k: Nat, +m: Nat) -> {SF.rne(C.shift(k, m), k) == m : Nat}:
30  match k:
31    case 0n:
32      {==}
33    case 1n+ +i:
34      +S = C.shift(1n+i, m)
35      +h = C.shift(i, 1n)
36      +eq = WW.high_u(1n+i, 0n, m, FR.fz(1n+i))
37      +el = WW.low_u(1n+i, 0n, m, FR.fz(1n+i))
38      +e1 = Equal.cong(Nat, Nat, z => SF.rne_up(z, C.low(1n+i, S), h), C.high(1n+i, S), m, eq)
39      +e2 = Equal.cong(Nat, Nat, z => SF.rne_up(m, z, h), C.low(1n+i, S), 0n, el)
40      +hz = N.is_eq_sym_false(h, 0n, Equal.trans(Bool, Nat.is_eq(h, 0n), Nat.is_eq(1n, 0n), False{}, WW.shift_eq0(i, 1n), {==}))
41      +e3 = Equal.cong(Bool, Nat, t => Nat.add(m, SF.b2n(Bool.or(t, Bool.and(Nat.is_eq(0n, h), Nat.is_eq(Nat.mod(m, 2n), 1n))))), Nat.is_lt(h, 0n), False{}, lt0f(h))
42      +e4 = Equal.cong(Bool, Nat, t => Nat.add(m, SF.b2n(Bool.or(False{}, Bool.and(t, Nat.is_eq(Nat.mod(m, 2n), 1n))))), Nat.is_eq(0n, h), False{}, hz)
43      +e5 = N.add_zero(m)
44      Equal.trans(Nat, SF.rne_up(C.high(1n+i, S), C.low(1n+i, S), h), SF.rne_up(m, C.low(1n+i, S), h), m, e1, Equal.trans(Nat, SF.rne_up(m, C.low(1n+i, S), h), SF.rne_up(m, 0n, h), m, e2, Equal.trans(Nat, SF.rne_up(m, 0n, h), Nat.add(m, SF.b2n(Bool.or(False{}, Bool.and(Nat.is_eq(0n, h), Nat.is_eq(Nat.mod(m, 2n), 1n))))), m, e3, Equal.trans(Nat, Nat.add(m, SF.b2n(Bool.or(False{}, Bool.and(Nat.is_eq(0n, h), Nat.is_eq(Nat.mod(m, 2n), 1n))))), Nat.add(m, 0n), m, e4, e5))))
45
46# rounding m * 2^k by j + k bits is rounding m by j bits
47def rne_shift(+k: Nat, +m: Nat, +j: Nat) -> {SF.rne(C.shift(k, m), Nat.add(j, k)) == SF.rne(m, j) : Nat}:
48  match j:
49    case 0n:
50      rne_exact(k, m)
51    case 1n+ +i:
52      +a = Nat.add(1n+i, k)
53      +ea = NA.add_comm(1n+i, k)
54      +hq = Equal.trans(Nat, C.high(a, C.shift(k, m)), C.high(Nat.add(k, 1n+i), C.shift(k, m)), C.high(1n+i, m), Equal.cong(Nat, Nat, z => C.high(z, C.shift(k, m)), a, Nat.add(k, 1n+i), ea), Equal.trans(Nat, C.high(Nat.add(k, 1n+i), C.shift(k, m)), C.high(1n+i, C.high(k, C.shift(k, m))), C.high(1n+i, m), WW.high_comp(1n+i, k, C.shift(k, m)), Equal.cong(Nat, Nat, z => C.high(1n+i, z), C.high(k, C.shift(k, m)), m, WW.high_u(k, 0n, m, FR.fz(k)))))
55      +hl = Equal.trans(Nat, C.low(a, C.shift(k, m)), C.low(Nat.add(k, 1n+i), C.shift(k, m)), C.shift(k, C.low(1n+i, m)), Equal.cong(Nat, Nat, z => C.low(z, C.shift(k, m)), a, Nat.add(k, 1n+i), ea), WW.low_shift(k, 1n+i, m))
56      +hh = Equal.trans(Nat, C.shift(Nat.add(i, k), 1n), C.shift(Nat.add(k, i), 1n), C.shift(k, C.shift(i, 1n)), Equal.cong(Nat, Nat, z => C.shift(z, 1n), Nat.add(i, k), Nat.add(k, i), NA.add_comm(i, k)), WW.shift_comp(k, i, 1n))
57      +hc = Equal.trans(Cmp, Nat.cmp(C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n)), Nat.cmp(C.shift(k, C.low(1n+i, m)), C.shift(Nat.add(i, k), 1n)), Nat.cmp(C.low(1n+i, m), C.shift(i, 1n)), Equal.cong(Nat, Cmp, z => Nat.cmp(z, C.shift(Nat.add(i, k), 1n)), C.low(a, C.shift(k, m)), C.shift(k, C.low(1n+i, m)), hl), Equal.trans(Cmp, Nat.cmp(C.shift(k, C.low(1n+i, m)), C.shift(Nat.add(i, k), 1n)), Nat.cmp(C.shift(k, C.low(1n+i, m)), C.shift(k, C.shift(i, 1n))), Nat.cmp(C.low(1n+i, m), C.shift(i, 1n)), Equal.cong(Nat, Cmp, z => Nat.cmp(C.shift(k, C.low(1n+i, m)), z), C.shift(Nat.add(i, k), 1n), C.shift(k, C.shift(i, 1n)), hh), NC.cmp_shift(k, C.low(1n+i, m), C.shift(i, 1n))))
58      +l1 = FR.rne_cmp(C.high(a, C.shift(k, m)), C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n))
59      +l2 = Equal.cong(Nat, Nat, z => FR.rne_c(z, Nat.cmp(C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n))), C.high(a, C.shift(k, m)), C.high(1n+i, m), hq)
60      +l3 = Equal.cong(Cmp, Nat, t => FR.rne_c(C.high(1n+i, m), t), Nat.cmp(C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n)), Nat.cmp(C.low(1n+i, m), C.shift(i, 1n)), hc)
61      +r1 = FR.rne_cmp(C.high(1n+i, m), C.low(1n+i, m), C.shift(i, 1n))
62      Equal.trans(Nat, SF.rne_up(C.high(a, C.shift(k, m)), C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n)), FR.rne_c(C.high(1n+i, m), Nat.cmp(C.low(1n+i, m), C.shift(i, 1n))), SF.rne_up(C.high(1n+i, m), C.low(1n+i, m), C.shift(i, 1n)), Equal.trans(Nat, SF.rne_up(C.high(a, C.shift(k, m)), C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n)), FR.rne_c(C.high(a, C.shift(k, m)), Nat.cmp(C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n))), FR.rne_c(C.high(1n+i, m), Nat.cmp(C.low(1n+i, m), C.shift(i, 1n))), l1, Equal.trans(Nat, FR.rne_c(C.high(a, C.shift(k, m)), Nat.cmp(C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n))), FR.rne_c(C.high(1n+i, m), Nat.cmp(C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n))), FR.rne_c(C.high(1n+i, m), Nat.cmp(C.low(1n+i, m), C.shift(i, 1n))), l2, l3)), Equal.sym(Nat, SF.rne_up(C.high(1n+i, m), C.low(1n+i, m), C.shift(i, 1n)), FR.rne_c(C.high(1n+i, m), Nat.cmp(C.low(1n+i, m), C.shift(i, 1n))), r1))
63
64# ---- bit lengths under shifts ----
65
66def bl_fit(+n: Nat) -> {C.fits(M.bit_length(n), n) == True{} : Bool}:
67  WW.fits_of_lt(M.bit_length(n), n, BT.bit_length_lt(n))
68
69def bl_nfit(+n: Nat, +hz: {Nat.is_eq(n, 0n) == False{} : Bool}) -> {C.fits(Nat.sub(M.bit_length(n), 1n), n) == False{} : Bool}:
70  +K = Nat.sub(M.bit_length(n), 1n)
71  +nf = Equal.trans(Bool, C.fits(K, C.pow2(K)), Nat.is_lt(C.pow2(K), C.pow2(K)), False{}, WW.fits_lt(K, C.pow2(K)), N.lt_irrefl(C.pow2(K)))
72  FR.nfit(K, C.pow2(K), n, FO.lower(n, hz), nf)
73
74def fits_sh(+k: Nat, +a: Nat, +m: Nat) -> {C.fits(Nat.add(k, a), C.shift(k, m)) == C.fits(a, m) : Bool}:
75  Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), C.high(Nat.add(k, a), C.shift(k, m)), C.high(a, m), Equal.trans(Nat, C.high(Nat.add(k, a), C.shift(k, m)), C.high(a, C.high(k, C.shift(k, m))), C.high(a, m), WW.high_comp(a, k, C.shift(k, m)), Equal.cong(Nat, Nat, z => C.high(a, z), C.high(k, C.shift(k, m)), m, WW.high_u(k, 0n, m, FR.fz(k)))))
76
77def bl_shift(+k: Nat, +m: Nat, +hz: {Nat.is_eq(m, 0n) == False{} : Bool}) -> {M.bit_length(C.shift(k, m)) == Nat.add(M.bit_length(m), k) : Nat}:
78  +B = M.bit_length(m)
79  +j = Nat.sub(B, 1n)
80  +ej = N.sub_add(B, 1n, FO.bl_pos(m, hz, B, {==}))
81  +nf = Equal.trans(Bool, C.fits(Nat.add(k, j), C.shift(k, m)), C.fits(j, m), False{}, fits_sh(k, j, m), bl_nfit(m, hz))
82  +f0 = L.subst(Nat, z => {C.fits(z, m) == True{} : Bool}, B, 1n+j, Equal.sym(Nat, 1n+j, B, ej), bl_fit(m))
83  +f1 = Equal.trans(Bool, C.fits(Nat.add(k, 1n+j), C.shift(k, m)), C.fits(1n+j, m), True{}, fits_sh(k, 1n+j, m), f0)
84  +f2 = L.subst(Nat, z => {C.fits(z, C.shift(k, m)) == True{} : Bool}, Nat.add(k, 1n+j), 1n+Nat.add(k, j), N.add_succ(k, j), f1)
85  +eb = FR.bl_c(Nat.add(k, j), C.shift(k, m), nf, f2, Nat.cmp(M.bit_length(C.shift(k, m)), 1n+Nat.add(k, j)), {==})
86  +er = Equal.trans(Nat, Nat.add(B, k), Nat.add(1n+j, k), 1n+Nat.add(k, j), Equal.cong(Nat, Nat, z => Nat.add(z, k), B, 1n+j, Equal.sym(Nat, 1n+j, B, ej)), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(j, k), Nat.add(k, j), NA.add_comm(j, k)))
87  Equal.trans(Nat, M.bit_length(C.shift(k, m)), 1n+Nat.add(k, j), Nat.add(B, k), eb, Equal.sym(Nat, Nat.add(B, k), 1n+Nat.add(k, j), er))
88
89# ---- scaling ----
90
91def a1(+x: Nat, +k: Nat, +u: Nat, +h: {Nat.is_le(Nat.add(x, k), u) == True{} : Bool}) -> {Nat.sub(u, x) == Nat.add(Nat.sub(u, Nat.add(x, k)), k) : Nat}:
92  +r = Nat.sub(u, Nat.add(x, k))
93  +eu = N.sub_add(u, Nat.add(x, k), h)
94  Equal.trans(Nat, Nat.sub(u, x), Nat.sub(Nat.add(Nat.add(x, k), r), x), Nat.add(r, k), Equal.cong(Nat, Nat, z => Nat.sub(z, x), u, Nat.add(Nat.add(x, k), r), Equal.sym(Nat, Nat.add(Nat.add(x, k), r), u, eu)), Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(x, k), r), x), Nat.sub(Nat.add(x, Nat.add(k, r)), x), Nat.add(r, k), Equal.cong(Nat, Nat, z => Nat.sub(z, x), Nat.add(Nat.add(x, k), r), Nat.add(x, Nat.add(k, r)), NA.add_assoc(x, k, r)), Equal.trans(Nat, Nat.sub(Nat.add(x, Nat.add(k, r)), x), Nat.add(k, r), Nat.add(r, k), N.add_sub_cancel(x, Nat.add(k, r)), NA.add_comm(k, r))))
95
96def qeq_f(+k: Nat, +m: Nat, +x: Nat, +u: Nat, +c1: Bool, +hc1: {Nat.is_le(x, u) == c1 : Bool}, +hc2: {Nat.is_le(Nat.add(x, k), u) == False{} : Bool}) -> {SF.pick(Nat, c1, SF.rne(C.shift(k, m), Nat.sub(u, x)), C.shift(Nat.sub(x, u), C.shift(k, m))) == C.shift(Nat.sub(Nat.add(x, k), u), m) : Nat}:
97  match c1:
98    case True{}:
99      +t = Nat.sub(u, x)
100      +eu = N.sub_add(u, x, hc1)
101      +hlt0 = N.not_le_lt(Nat.add(x, k), u, hc2)
102      +hlt1 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(x, k)) == True{} : Bool}, u, Nat.add(x, t), Equal.sym(Nat, Nat.add(x, t), u, eu), hlt0)
103      +hlt2 = Equal.trans(Bool, Nat.is_lt(t, k), Nat.is_lt(Nat.add(x, t), Nat.add(x, k)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(x, t), Nat.add(x, k)), Nat.is_lt(t, k), WW.lt_cancel_l(x, t, k)), hlt1)
104      +htk = N.lt_le(t, k, hlt2)
105      +es = NC.sh_split(k, t, m, htk)
106      +e1 = Equal.trans(Nat, SF.rne(C.shift(k, m), t), SF.rne(C.shift(t, C.shift(Nat.sub(k, t), m)), t), C.shift(Nat.sub(k, t), m), Equal.cong(Nat, Nat, z => SF.rne(z, t), C.shift(k, m), C.shift(t, C.shift(Nat.sub(k, t), m)), es), rne_exact(t, C.shift(Nat.sub(k, t), m)))
107      +e2 = Equal.trans(Nat, Nat.sub(k, t), Nat.sub(Nat.add(k, x), Nat.add(t, x)), Nat.sub(Nat.add(x, k), u), Equal.sym(Nat, Nat.sub(Nat.add(k, x), Nat.add(t, x)), Nat.sub(k, t), FR.sub_cancel_r(k, t, x)), Equal.trans(Nat, Nat.sub(Nat.add(k, x), Nat.add(t, x)), Nat.sub(Nat.add(x, k), Nat.add(t, x)), Nat.sub(Nat.add(x, k), u), Equal.cong(Nat, Nat, z => Nat.sub(z, Nat.add(t, x)), Nat.add(k, x), Nat.add(x, k), NA.add_comm(k, x)), Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(x, k), z), Nat.add(t, x), u, Equal.trans(Nat, Nat.add(t, x), Nat.add(x, t), u, NA.add_comm(t, x), eu))))
108      Equal.trans(Nat, SF.pick(Nat, True{}, SF.rne(C.shift(k, m), Nat.sub(u, x)), C.shift(Nat.sub(x, u), C.shift(k, m))), SF.rne(C.shift(k, m), Nat.sub(u, x)), C.shift(Nat.sub(Nat.add(x, k), u), m), FR.pk_t(Nat, SF.rne(C.shift(k, m), Nat.sub(u, x)), C.shift(Nat.sub(x, u), C.shift(k, m))), Equal.trans(Nat, SF.rne(C.shift(k, m), t), C.shift(Nat.sub(k, t), m), C.shift(Nat.sub(Nat.add(x, k), u), m), e1, Equal.cong(Nat, Nat, z => C.shift(z, m), Nat.sub(k, t), Nat.sub(Nat.add(x, k), u), e2)))
109    case False{}:
110      +hux = N.lt_le(u, x, N.not_le_lt(x, u, hc1))
111      Equal.trans(Nat, SF.pick(Nat, False{}, SF.rne(C.shift(k, m), Nat.sub(u, x)), C.shift(Nat.sub(x, u), C.shift(k, m))), C.shift(Nat.sub(x, u), C.shift(k, m)), C.shift(Nat.sub(Nat.add(x, k), u), m), FR.pk_f(Nat, SF.rne(C.shift(k, m), Nat.sub(u, x)), C.shift(Nat.sub(x, u), C.shift(k, m))), Equal.trans(Nat, C.shift(Nat.sub(x, u), C.shift(k, m)), C.shift(Nat.add(Nat.sub(x, u), k), m), C.shift(Nat.sub(Nat.add(x, k), u), m), Equal.sym(Nat, C.shift(Nat.add(Nat.sub(x, u), k), m), C.shift(Nat.sub(x, u), C.shift(k, m)), WW.shift_comp(Nat.sub(x, u), k, m)), Equal.cong(Nat, Nat, z => C.shift(z, m), Nat.add(Nat.sub(x, u), k), Nat.sub(Nat.add(x, k), u), Equal.sym(Nat, Nat.sub(Nat.add(x, k), u), Nat.add(Nat.sub(x, u), k), FR.sub_add_r(x, k, u, hux)))))
112
113def qeq_c(+k: Nat, +m: Nat, +x: Nat, +u: Nat, +c1: Bool, +hc1: {Nat.is_le(x, u) == c1 : Bool}, +c2: Bool, +hc2: {Nat.is_le(Nat.add(x, k), u) == c2 : Bool}) -> {SF.pick(Nat, c1, SF.rne(C.shift(k, m), Nat.sub(u, x)), C.shift(Nat.sub(x, u), C.shift(k, m))) == SF.pick(Nat, c2, SF.rne(m, Nat.sub(u, Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), u), m)) : Nat}:
114  match c2:
115    case True{}:
116      +h1 = N.le_trans(x, Nat.add(x, k), u, N.le_add_right(x, k), hc2)
117      +ec1 = Equal.trans(Bool, c1, Nat.is_le(x, u), True{}, Equal.sym(Bool, Nat.is_le(x, u), c1, hc1), h1)
118      +r = Nat.sub(u, Nat.add(x, k))
119      +base = Equal.trans(Nat, SF.rne(C.shift(k, m), Nat.sub(u, x)), SF.rne(C.shift(k, m), Nat.add(r, k)), SF.rne(m, r), Equal.cong(Nat, Nat, z => SF.rne(C.shift(k, m), z), Nat.sub(u, x), Nat.add(r, k), a1(x, k, u, hc2)), rne_shift(k, m, r))
120      Equal.trans(Nat, SF.pick(Nat, c1, SF.rne(C.shift(k, m), Nat.sub(u, x)), C.shift(Nat.sub(x, u), C.shift(k, m))), SF.rne(m, Nat.sub(u, Nat.add(x, k))), SF.pick(Nat, True{}, SF.rne(m, Nat.sub(u, Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), u), m)), L.subst(Bool, t => {SF.pick(Nat, t, SF.rne(C.shift(k, m), Nat.sub(u, x)), C.shift(Nat.sub(x, u), C.shift(k, m))) == SF.rne(m, r) : Nat}, True{}, c1, Equal.sym(Bool, c1, True{}, ec1), base), Equal.sym(Nat, SF.pick(Nat, True{}, SF.rne(m, Nat.sub(u, Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), u), m)), SF.rne(m, Nat.sub(u, Nat.add(x, k))), FR.pk_t(Nat, SF.rne(m, Nat.sub(u, Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), u), m))))
121    case False{}:
122      Equal.trans(Nat, SF.pick(Nat, c1, SF.rne(C.shift(k, m), Nat.sub(u, x)), C.shift(Nat.sub(x, u), C.shift(k, m))), C.shift(Nat.sub(Nat.add(x, k), u), m), SF.pick(Nat, False{}, SF.rne(m, Nat.sub(u, Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), u), m)), qeq_f(k, m, x, u, c1, hc1, hc2), Equal.sym(Nat, SF.pick(Nat, False{}, SF.rne(m, Nat.sub(u, Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), u), m)), C.shift(Nat.sub(Nat.add(x, k), u), m), FR.pk_f(Nat, SF.rne(m, Nat.sub(u, Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), u), m))))
123
124
125# SF.round, SF.round_u and SF.pick unfolded once, over variables: proofs
126# rewrite with these instead of letting a conversion unfold (and normalize)
127# the rounding on both sides
128def rd(+s: Bool, +m: Nat, +x: Nat) -> {SF.round(s, m, x) == SF.pick(F.F64, Nat.is_eq(m, 0n), SF.zero(s), SF.round_u(s, m, x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))) : F.F64}:
129  {==}
130
131def rud(+s: Bool, +m: Nat, +x: Nat, +u: Nat) -> {SF.round_u(s, m, x, u) == SF.pack(s, SF.pick(Nat, Nat.is_le(x, u), SF.rne(m, Nat.sub(u, x)), C.shift(Nat.sub(x, u), m)), u) : F.F64}:
132  {==}
133
134def rs_c(+s: Bool, +k: Nat, +m: Nat, +x: Nat, +z: Bool, +hz: {Nat.is_eq(m, 0n) == z : Bool}) -> {SF.round(s, C.shift(k, m), x) == SF.round(s, m, Nat.add(x, k)) : F.F64}:
135  match z:
136    case True{}:
137      +e0 = Equal.trans(Bool, Nat.is_eq(C.shift(k, m), 0n), Nat.is_eq(m, 0n), True{}, WW.shift_eq0(k, m), hz)
138      Equal.trans(F.F64, SF.round(s, C.shift(k, m), x), SF.pick(F.F64, Nat.is_eq(C.shift(k, m), 0n), SF.zero(s), SF.round_u(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(C.shift(k, m))), 53n), Nat.sub(SF.zb(), 1074n)))), SF.round(s, m, Nat.add(x, k)), rd(s, C.shift(k, m), x), Equal.trans(F.F64, SF.pick(F.F64, Nat.is_eq(C.shift(k, m), 0n), SF.zero(s), SF.round_u(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(C.shift(k, m))), 53n), Nat.sub(SF.zb(), 1074n)))), SF.pick(F.F64, True{}, SF.zero(s), SF.round_u(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(C.shift(k, m))), 53n), Nat.sub(SF.zb(), 1074n)))), SF.round(s, m, Nat.add(x, k)), Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.zero(s), SF.round_u(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(C.shift(k, m))), 53n), Nat.sub(SF.zb(), 1074n)))), Nat.is_eq(C.shift(k, m), 0n), True{}, e0), Equal.trans(F.F64, SF.pick(F.F64, True{}, SF.zero(s), SF.round_u(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(C.shift(k, m))), 53n), Nat.sub(SF.zb(), 1074n)))), SF.zero(s), SF.round(s, m, Nat.add(x, k)), FR.pk_t(F.F64, SF.zero(s), SF.round_u(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(C.shift(k, m))), 53n), Nat.sub(SF.zb(), 1074n)))), Equal.trans(F.F64, SF.zero(s), SF.pick(F.F64, True{}, SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), SF.round(s, m, Nat.add(x, k)), Equal.sym(F.F64, SF.pick(F.F64, True{}, SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), SF.zero(s), FR.pk_t(F.F64, SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))))), Equal.trans(F.F64, SF.pick(F.F64, True{}, SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), SF.pick(F.F64, Nat.is_eq(m, 0n), SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), SF.round(s, m, Nat.add(x, k)), Equal.sym(F.F64, SF.pick(F.F64, Nat.is_eq(m, 0n), SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), SF.pick(F.F64, True{}, SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), Nat.is_eq(m, 0n), True{}, hz)), Equal.sym(F.F64, SF.round(s, m, Nat.add(x, k)), SF.pick(F.F64, Nat.is_eq(m, 0n), SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), rd(s, m, Nat.add(x, k))))))))
139    case False{}:
140      +B = M.bit_length(m)
141      +e0 = Equal.trans(Bool, Nat.is_eq(C.shift(k, m), 0n), Nat.is_eq(m, 0n), False{}, WW.shift_eq0(k, m), hz)
142      +l1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.zero(s), SF.round_u(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(C.shift(k, m))), 53n), Nat.sub(SF.zb(), 1074n)))), Nat.is_eq(C.shift(k, m), 0n), False{}, e0)
143      +ea = Equal.trans(Nat, Nat.add(x, Nat.add(B, k)), Nat.add(x, Nat.add(k, B)), Nat.add(Nat.add(x, k), B), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(B, k), Nat.add(k, B), NA.add_comm(B, k)), Equal.sym(Nat, Nat.add(Nat.add(x, k), B), Nat.add(x, Nat.add(k, B)), NA.add_assoc(x, k, B)))
144      +eu = Equal.trans(Nat, Nat.max(Nat.sub(Nat.add(x, M.bit_length(C.shift(k, m))), 53n), Nat.sub(SF.zb(), 1074n)), Nat.max(Nat.sub(Nat.add(x, Nat.add(B, k)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Equal.cong(Nat, Nat, w => Nat.max(Nat.sub(Nat.add(x, w), 53n), Nat.sub(SF.zb(), 1074n)), M.bit_length(C.shift(k, m)), Nat.add(B, k), bl_shift(k, m, hz)), Equal.cong(Nat, Nat, w => Nat.max(Nat.sub(w, 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, Nat.add(B, k)), Nat.add(Nat.add(x, k), B), ea))
145      +l2 = Equal.cong(Nat, F.F64, w => SF.round_u(s, C.shift(k, m), x, w), Nat.max(Nat.sub(Nat.add(x, M.bit_length(C.shift(k, m))), 53n), Nat.sub(SF.zb(), 1074n)), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), eu)
146      +l3 = Equal.cong(Nat, F.F64, w => SF.pack(s, w, Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pick(Nat, Nat.is_le(x, Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.rne(C.shift(k, m), Nat.sub(Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), x)), C.shift(Nat.sub(x, Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), C.shift(k, m))), SF.pick(Nat, Nat.is_le(Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.rne(m, Nat.sub(Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), m)), qeq_c(k, m, x, Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.is_le(x, Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), {==}, Nat.is_le(Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), {==}))
147      +r1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), Nat.is_eq(m, 0n), False{}, hz)
148      Equal.trans(F.F64, SF.round(s, C.shift(k, m), x), SF.pick(F.F64, Nat.is_eq(C.shift(k, m), 0n), SF.zero(s), SF.round_u(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(C.shift(k, m))), 53n), Nat.sub(SF.zb(), 1074n)))), SF.round(s, m, Nat.add(x, k)), rd(s, C.shift(k, m), x), Equal.trans(F.F64, SF.pick(F.F64, Nat.is_eq(C.shift(k, m), 0n), SF.zero(s), SF.round_u(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(C.shift(k, m))), 53n), Nat.sub(SF.zb(), 1074n)))), SF.pick(F.F64, False{}, SF.zero(s), SF.round_u(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(C.shift(k, m))), 53n), Nat.sub(SF.zb(), 1074n)))), SF.round(s, m, Nat.add(x, k)), l1, Equal.trans(F.F64, SF.pick(F.F64, False{}, SF.zero(s), SF.round_u(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(C.shift(k, m))), 53n), Nat.sub(SF.zb(), 1074n)))), SF.round_u(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(C.shift(k, m))), 53n), Nat.sub(SF.zb(), 1074n))), SF.round(s, m, Nat.add(x, k)), FR.pk_f(F.F64, SF.zero(s), SF.round_u(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(C.shift(k, m))), 53n), Nat.sub(SF.zb(), 1074n)))), Equal.trans(F.F64, SF.round_u(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(C.shift(k, m))), 53n), Nat.sub(SF.zb(), 1074n))), SF.round_u(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.round(s, m, Nat.add(x, k)), l2, Equal.trans(F.F64, SF.round_u(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.pick(Nat, Nat.is_le(x, Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.rne(C.shift(k, m), Nat.sub(Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), x)), C.shift(Nat.sub(x, Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), C.shift(k, m))), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.round(s, m, Nat.add(x, k)), rud(s, C.shift(k, m), x, Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), Equal.trans(F.F64, SF.pack(s, SF.pick(Nat, Nat.is_le(x, Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.rne(C.shift(k, m), Nat.sub(Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), x)), C.shift(Nat.sub(x, Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), C.shift(k, m))), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.pick(Nat, Nat.is_le(Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.rne(m, Nat.sub(Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), m)), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.round(s, m, Nat.add(x, k)), l3, Equal.trans(F.F64, SF.pack(s, SF.pick(Nat, Nat.is_le(Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.rne(m, Nat.sub(Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), m)), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.round(s, m, Nat.add(x, k)), Equal.sym(F.F64, SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.pick(Nat, Nat.is_le(Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.rne(m, Nat.sub(Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, k))), C.shift(Nat.sub(Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), m)), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), rud(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), Equal.trans(F.F64, SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pick(F.F64, False{}, SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), SF.round(s, m, Nat.add(x, k)), Equal.sym(F.F64, SF.pick(F.F64, False{}, SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), FR.pk_f(F.F64, SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))))), Equal.trans(F.F64, SF.pick(F.F64, False{}, SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), SF.pick(F.F64, Nat.is_eq(m, 0n), SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), SF.round(s, m, Nat.add(x, k)), Equal.sym(F.F64, SF.pick(F.F64, Nat.is_eq(m, 0n), SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), SF.pick(F.F64, False{}, SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), r1), Equal.sym(F.F64, SF.round(s, m, Nat.add(x, k)), SF.pick(F.F64, Nat.is_eq(m, 0n), SF.zero(s), SF.round_u(s, m, Nat.add(x, k), Nat.max(Nat.sub(Nat.add(Nat.add(x, k), M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), rd(s, m, Nat.add(x, k))))))))))))
149
150# round(s, m * 2^k, x) = round(s, m, x + k)
151def round_shift(+s: Bool, +k: Nat, +m: Nat, +x: Nat) -> {SF.round(s, C.shift(k, m), x) == SF.round(s, m, Nat.add(x, k)) : F.F64}:
152  rs_c(s, k, m, x, Nat.is_eq(m, 0n), {==})
153
154# round_shift with the new exponent y == x + k given (a literal at the use), so
155# the result needs no conversion of Nat.add(x, k) inside SF.round
156def round_shift_to(+s: Bool, +k: Nat, +m: Nat, +x: Nat, +y: Nat, +hy: {Nat.add(x, k) == y : Nat}) -> {SF.round(s, C.shift(k, m), x) == SF.round(s, m, y) : F.F64}:
157  Equal.trans(F.F64, SF.round(s, C.shift(k, m), x), SF.round(s, m, Nat.add(x, k)), SF.round(s, m, y), round_shift(s, k, m, x), Equal.cong(Nat, F.F64, z => SF.round(s, m, z), Nat.add(x, k), y, hy))
158
159# ---- the sticky bit under the spec's round ----
160
161def max_ge_l(+a: Nat, +b: Nat) -> {Nat.is_le(a, Nat.max(a, b)) == True{} : Bool}:
162  match a b:
163    case 0n _:
164      N.zero_le(b)
165    case 1n+ +ap 0n:
166      N.le_refl(1n+ap)
167    case 1n+ +ap 1n+ +bp:
168      max_ge_l(ap, bp)
169
170def le_sub(+a: Nat, +c: Nat, +b: Nat, +h: {Nat.is_le(Nat.add(a, c), b) == True{} : Bool}) -> {Nat.is_le(a, Nat.sub(b, c)) == True{} : Bool}:
171  +eb = N.sub_add(b, Nat.add(a, c), h)
172  +r = Nat.sub(b, Nat.add(a, c))
173  +e1 = Equal.trans(Nat, Nat.sub(b, c), Nat.sub(Nat.add(Nat.add(a, c), r), c), Nat.add(a, r), Equal.cong(Nat, Nat, z => Nat.sub(z, c), b, Nat.add(Nat.add(a, c), r), Equal.sym(Nat, Nat.add(Nat.add(a, c), r), b, eb)), Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(a, c), r), c), Nat.sub(Nat.add(c, Nat.add(a, r)), c), Nat.add(a, r), Equal.cong(Nat, Nat, z => Nat.sub(z, c), Nat.add(Nat.add(a, c), r), Nat.add(c, Nat.add(a, r)), Equal.trans(Nat, Nat.add(Nat.add(a, c), r), Nat.add(Nat.add(c, a), r), Nat.add(c, Nat.add(a, r)), Equal.cong(Nat, Nat, z => Nat.add(z, r), Nat.add(a, c), Nat.add(c, a), NA.add_comm(a, c)), NA.add_assoc(c, a, r))), N.add_sub_cancel(c, Nat.add(a, r))))
174  L.subst(Nat, z => {Nat.is_le(a, z) == True{} : Bool}, Nat.add(a, r), Nat.sub(b, c), Equal.sym(Nat, Nat.sub(b, c), Nat.add(a, r), e1), N.le_add_right(a, r))
175
176# a bit t <= 1 below 2 y leaves the width of y
177def fit_td(+a: Nat, +t: Nat, +y: Nat, +ht: {Nat.is_le(t, 1n) == True{} : Bool}) -> {C.fits(1n+a, Nat.add(t, Nat.double(y))) == C.fits(a, y) : Bool}:
178  Equal.cong(Nat, Bool, z => C.fits(a, z), C.half(Nat.add(t, Nat.double(y))), y, Equal.trans(Nat, C.half(Nat.add(t, Nat.double(y))), Nat.add(C.half(t), y), y, WW.half_dbl(t, y), Equal.cong(Nat, Nat, z => Nat.add(z, y), C.half(t), 0n, FR.half_small(t, ht))))
179
180def jam_fits(+a: Nat, +h: Nat, +l: Nat) -> {C.fits(1n+a, SW.jam(h, l)) == C.fits(1n+a, h) : Bool}:
181  +t = Nat.max(C.bit(h), Nat.min(l, 1n))
182  +e1 = Equal.cong(Nat, Bool, z => C.fits(1n+a, z), SW.jam(h, l), Nat.add(t, Nat.double(C.half(h))), FR.jam_form(h, l))
183  +e2 = fit_td(a, t, C.half(h), FR.max_le1(C.bit(h), l, WW.bit_le1(h)))
184  +e3 = Equal.sym(Bool, C.fits(1n+a, Nat.add(C.bit(h), Nat.double(C.half(h)))), C.fits(a, C.half(h)), fit_td(a, C.bit(h), C.half(h), WW.bit_le1(h)))
185  +e4 = Equal.cong(Nat, Bool, z => C.fits(1n+a, z), 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)))
186  Equal.trans(Bool, C.fits(1n+a, SW.jam(h, l)), C.fits(1n+a, Nat.add(t, Nat.double(C.half(h)))), C.fits(1n+a, h), e1, Equal.trans(Bool, C.fits(1n+a, Nat.add(t, Nat.double(C.half(h)))), C.fits(a, C.half(h)), C.fits(1n+a, h), e2, Equal.trans(Bool, C.fits(a, C.half(h)), C.fits(1n+a, Nat.add(C.bit(h), Nat.double(C.half(h)))), C.fits(1n+a, h), e3, e4)))
187
188def nz_bl(+m: Nat, +K: Nat, +hb: {Nat.is_le(1n+K, M.bit_length(m)) == True{} : Bool}, +z: Bool, +hz: {Nat.is_eq(m, 0n) == z : Bool}) -> {z == False{} : Bool}:
189  match z:
190    case True{}:
191      +e0 = N.eq_from_is_eq(m, 0n, hz)
192      +h0 = L.subst(Nat, w => {Nat.is_le(1n+K, M.bit_length(w)) == True{} : Bool}, m, 0n, e0, hb)
193      +h1 = L.subst(Nat, w => {Nat.is_le(1n+K, w) == True{} : Bool}, M.bit_length(0n), 0n, BT.bit_length_zero(), h0)
194      NC.absurd_tf({True{} == False{} : Bool}, h1)
195    case False{}:
196      {==}
197
198def rj2(+s: Bool, +d: Nat, +m: Nat, +x: Nat, +hb: {Nat.is_le(Nat.add(d, 55n), M.bit_length(m)) == True{} : Bool}, +hz: {Nat.is_eq(m, 0n) == False{} : Bool}, +e: Nat, +fh0: {C.fits(e, C.high(d, m)) == False{} : Bool}, +fh1: {C.fits(1n+e, C.high(d, m)) == True{} : Bool}, +eB: {Nat.add(d, 1n+e) == M.bit_length(m) : Nat}) -> {SF.round(s, m, x) == SF.round(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d)) : F.F64}:
199  +ejf = FR.jam_form(C.high(d, m), C.low(d, m))
200  +hhb = WW.le_add_r(C.bit(C.high(d, m)), Nat.max(C.bit(C.high(d, m)), Nat.min(C.low(d, m), 1n)), Nat.double(C.half(C.high(d, m))), max_ge_l(C.bit(C.high(d, m)), Nat.min(C.low(d, m), 1n)))
201  +hhJ = L.subst(Nat, z => {Nat.is_le(z, SW.jam(C.high(d, m), C.low(d, m))) == True{} : Bool}, Nat.add(C.bit(C.high(d, m)), Nat.double(C.half(C.high(d, m)))), C.high(d, m), Equal.sym(Nat, C.high(d, m), Nat.add(C.bit(C.high(d, m)), Nat.double(C.half(C.high(d, m)))), WW.hb(C.high(d, m))), L.subst(Nat, z => {Nat.is_le(Nat.add(C.bit(C.high(d, m)), Nat.double(C.half(C.high(d, m)))), z) == True{} : Bool}, Nat.add(Nat.max(C.bit(C.high(d, m)), Nat.min(C.low(d, m), 1n)), Nat.double(C.half(C.high(d, m)))), SW.jam(C.high(d, m), C.low(d, m)), Equal.sym(Nat, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(Nat.max(C.bit(C.high(d, m)), Nat.min(C.low(d, m), 1n)), Nat.double(C.half(C.high(d, m)))), ejf), hhb))
202  +nfJ = FR.nfit(e, C.high(d, m), SW.jam(C.high(d, m), C.low(d, m)), hhJ, fh0)
203  +fJ1 = Equal.trans(Bool, C.fits(1n+e, SW.jam(C.high(d, m), C.low(d, m))), C.fits(1n+e, C.high(d, m)), True{}, jam_fits(e, C.high(d, m), C.low(d, m)), fh1)
204  +eblJ = FR.bl_c(e, SW.jam(C.high(d, m), C.low(d, m)), nfJ, fJ1, Nat.cmp(M.bit_length(SW.jam(C.high(d, m), C.low(d, m))), 1n+e), {==})
205  +hzJ = FR.nz_of(e, SW.jam(C.high(d, m), C.low(d, m)), nfJ)
206  +ea = Equal.trans(Nat, Nat.add(Nat.add(x, d), M.bit_length(SW.jam(C.high(d, m), C.low(d, m)))), Nat.add(Nat.add(x, d), 1n+e), Nat.add(x, M.bit_length(m)), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(x, d), z), M.bit_length(SW.jam(C.high(d, m), C.low(d, m))), 1n+e, eblJ), Equal.trans(Nat, Nat.add(Nat.add(x, d), 1n+e), Nat.add(x, Nat.add(d, 1n+e)), Nat.add(x, M.bit_length(m)), NA.add_assoc(x, d, 1n+e), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(d, 1n+e), M.bit_length(m), eB)))
207  +eU = Equal.cong(Nat, Nat, z => Nat.max(Nat.sub(z, 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(Nat.add(x, d), M.bit_length(SW.jam(C.high(d, m), C.low(d, m)))), Nat.add(x, M.bit_length(m)), ea)
208  +ed55 = Equal.trans(Nat, Nat.add(Nat.add(x, Nat.add(d, 2n)), 53n), Nat.add(x, Nat.add(Nat.add(d, 2n), 53n)), Nat.add(x, Nat.add(d, 55n)), NA.add_assoc(x, Nat.add(d, 2n), 53n), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(Nat.add(d, 2n), 53n), Nat.add(d, 55n), NA.add_assoc(d, 2n, 53n)))
209  +a0 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(x, M.bit_length(m))) == True{} : Bool}, Nat.add(x, Nat.add(d, 55n)), Nat.add(Nat.add(x, Nat.add(d, 2n)), 53n), Equal.sym(Nat, Nat.add(Nat.add(x, Nat.add(d, 2n)), 53n), Nat.add(x, Nat.add(d, 55n)), ed55), N.le_add_left(Nat.add(d, 55n), M.bit_length(m), x, hb))
210  +hu = N.le_trans(Nat.add(x, Nat.add(d, 2n)), Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), le_sub(Nat.add(x, Nat.add(d, 2n)), 53n, Nat.add(x, M.bit_length(m)), a0), max_ge_l(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))
211  +i = Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, Nat.add(d, 2n)))
212  +eu = N.sub_add(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, Nat.add(d, 2n)), hu)
213  +k1 = Equal.trans(Nat, Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), x), Nat.sub(Nat.add(Nat.add(x, Nat.add(d, 2n)), i), x), Nat.add(2n+i, d), Equal.cong(Nat, Nat, z => Nat.sub(z, x), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(Nat.add(x, Nat.add(d, 2n)), i), Equal.sym(Nat, Nat.add(Nat.add(x, Nat.add(d, 2n)), i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), eu)), Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(x, Nat.add(d, 2n)), i), x), Nat.sub(Nat.add(x, Nat.add(Nat.add(d, 2n), i)), x), Nat.add(2n+i, d), Equal.cong(Nat, Nat, z => Nat.sub(z, x), Nat.add(Nat.add(x, Nat.add(d, 2n)), i), Nat.add(x, Nat.add(Nat.add(d, 2n), i)), NA.add_assoc(x, Nat.add(d, 2n), i)), Equal.trans(Nat, Nat.sub(Nat.add(x, Nat.add(Nat.add(d, 2n), i)), x), Nat.add(Nat.add(d, 2n), i), Nat.add(2n+i, d), N.add_sub_cancel(x, Nat.add(Nat.add(d, 2n), i)), Equal.trans(Nat, Nat.add(Nat.add(d, 2n), i), Nat.add(d, 2n+i), Nat.add(2n+i, d), NA.add_assoc(d, 2n, i), NA.add_comm(d, 2n+i)))))
214  +k2 = Equal.trans(Nat, Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, d)), Nat.sub(Nat.add(Nat.add(x, Nat.add(d, 2n)), i), Nat.add(x, d)), 2n+i, Equal.cong(Nat, Nat, z => Nat.sub(z, Nat.add(x, d)), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(Nat.add(x, Nat.add(d, 2n)), i), Equal.sym(Nat, Nat.add(Nat.add(x, Nat.add(d, 2n)), i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), eu)), Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(x, Nat.add(d, 2n)), i), Nat.add(x, d)), Nat.sub(Nat.add(Nat.add(Nat.add(x, d), 2n), i), Nat.add(x, d)), 2n+i, Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(z, i), Nat.add(x, d)), Nat.add(x, Nat.add(d, 2n)), Nat.add(Nat.add(x, d), 2n), Equal.sym(Nat, Nat.add(Nat.add(x, d), 2n), Nat.add(x, Nat.add(d, 2n)), NA.add_assoc(x, d, 2n))), Equal.trans(Nat, Nat.sub(Nat.add(Nat.add(Nat.add(x, d), 2n), i), Nat.add(x, d)), Nat.sub(Nat.add(Nat.add(x, d), 2n+i), Nat.add(x, d)), 2n+i, Equal.cong(Nat, Nat, z => Nat.sub(z, Nat.add(x, d)), Nat.add(Nat.add(Nat.add(x, d), 2n), i), Nat.add(Nat.add(x, d), 2n+i), NA.add_assoc(Nat.add(x, d), 2n, i)), N.add_sub_cancel(Nat.add(x, d), 2n+i))))
215  +hle1 = N.le_trans(x, Nat.add(x, Nat.add(d, 2n)), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), N.le_add_right(x, Nat.add(d, 2n)), hu)
216  +hle2 = N.le_trans(Nat.add(x, d), Nat.add(x, Nat.add(d, 2n)), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), N.le_add_left(d, Nat.add(d, 2n), x, N.le_add_right(d, 2n)), hu)
217  +l1 = Equal.cong(Bool, F.F64, z => SF.pick(F.F64, z, SF.zero(s), SF.round_u(s, m, x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)))), Nat.is_eq(m, 0n), False{}, hz)
218  +l2 = Equal.cong(Bool, F.F64, z => SF.pack(s, SF.pick(Nat, z, SF.rne(m, Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), x)), C.shift(Nat.sub(x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), m)), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), Nat.is_le(x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), True{}, hle1)
219  +l3 = Equal.cong(Nat, F.F64, z => SF.pack(s, SF.rne(m, z), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), x), Nat.add(2n+i, d), k1)
220  +l4 = Equal.cong(Nat, F.F64, z => SF.pack(s, z, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.rne(m, Nat.add(2n+i, d)), SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), FR.sticky(i, d, m))
221  +r1 = Equal.cong(Bool, F.F64, z => SF.pick(F.F64, z, SF.zero(s), SF.round_u(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d), Nat.max(Nat.sub(Nat.add(Nat.add(x, d), M.bit_length(SW.jam(C.high(d, m), C.low(d, m)))), 53n), Nat.sub(SF.zb(), 1074n)))), Nat.is_eq(SW.jam(C.high(d, m), C.low(d, m)), 0n), False{}, hzJ)
222  +r2 = Equal.cong(Nat, F.F64, z => SF.round_u(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d), z), Nat.max(Nat.sub(Nat.add(Nat.add(x, d), M.bit_length(SW.jam(C.high(d, m), C.low(d, m)))), 53n), Nat.sub(SF.zb(), 1074n)), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), eU)
223  +r3 = Equal.cong(Bool, F.F64, z => SF.pack(s, SF.pick(Nat, z, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, d))), C.shift(Nat.sub(Nat.add(x, d), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SW.jam(C.high(d, m), C.low(d, m)))), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), Nat.is_le(Nat.add(x, d), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), True{}, hle2)
224  +r4 = Equal.cong(Nat, F.F64, z => SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), z), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, d)), 2n+i, k2)
225  +lhs = Equal.trans(F.F64, SF.round(s, m, x), SF.round_u(s, m, x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), l1, Equal.trans(F.F64, SF.round_u(s, m, x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(m, Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), x)), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), l2, Equal.trans(F.F64, SF.pack(s, SF.rne(m, Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), x)), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(m, Nat.add(2n+i, d)), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), l3, l4)))
226  +rhs = Equal.trans(F.F64, SF.round(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d)), SF.round_u(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d), Nat.max(Nat.sub(Nat.add(Nat.add(x, d), M.bit_length(SW.jam(C.high(d, m), C.low(d, m)))), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), r1, Equal.trans(F.F64, SF.round_u(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d), Nat.max(Nat.sub(Nat.add(Nat.add(x, d), M.bit_length(SW.jam(C.high(d, m), C.low(d, m)))), 53n), Nat.sub(SF.zb(), 1074n))), SF.round_u(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), r2, Equal.trans(F.F64, SF.round_u(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), Nat.sub(Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n)), Nat.add(x, d))), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), r3, r4)))
227  Equal.trans(F.F64, SF.round(s, m, x), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), SF.round(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d)), lhs, Equal.sym(F.F64, SF.round(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d)), SF.pack(s, SF.rne(SW.jam(C.high(d, m), C.low(d, m)), 2n+i), Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), Nat.sub(SF.zb(), 1074n))), rhs))
228
229# round(s, m, x) = round(s, jam(m >> d, m mod 2^d), x + d) when m has d + 55 bits
230def round_jam(+s: Bool, +d: Nat, +m: Nat, +x: Nat, +hb: {Nat.is_le(Nat.add(d, 55n), M.bit_length(m)) == True{} : Bool}) -> {SF.round(s, m, x) == SF.round(s, SW.jam(C.high(d, m), C.low(d, m)), Nat.add(x, d)) : F.F64}:
231  +hb1 = L.subst(Nat, z => {Nat.is_le(z, M.bit_length(m)) == True{} : Bool}, Nat.add(d, 55n), 1n+Nat.add(d, 54n), Equal.trans(Nat, Nat.add(d, 55n), 1n+Nat.add(d, 54n), 1n+Nat.add(d, 54n), N.add_succ(d, 54n), {==}), hb)
232  +hz = nz_bl(m, Nat.add(d, 54n), hb1, Nat.is_eq(m, 0n), {==})
233  +j = Nat.sub(M.bit_length(m), 1n)
234  +ej = N.sub_add(M.bit_length(m), 1n, FO.bl_pos(m, hz, M.bit_length(m), {==}))
235  +hdj = N.le_trans(d, Nat.add(d, 54n), j, N.le_add_right(d, 54n), N.lt_succ_le(Nat.add(d, 54n), j, N.succ_le_lt(Nat.add(d, 54n), 1n+j, L.subst(Nat, z => {Nat.is_le(1n+Nat.add(d, 54n), z) == True{} : Bool}, M.bit_length(m), 1n+j, Equal.sym(Nat, 1n+j, M.bit_length(m), ej), hb1))))
236  +e = Nat.sub(j, d)
237  +eje = Equal.trans(Nat, Nat.add(e, d), Nat.add(d, e), j, NA.add_comm(e, d), N.sub_add(j, d, hdj))
238  +h = C.high(d, m)
239  +eB = Equal.trans(Nat, Nat.add(d, 1n+e), 1n+Nat.add(d, e), M.bit_length(m), N.add_succ(d, e), Equal.trans(Nat, 1n+Nat.add(d, e), 1n+j, M.bit_length(m), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(d, e), j, N.sub_add(j, d, hdj)), ej))
240  +fB = L.subst(Nat, z => {C.fits(z, m) == True{} : Bool}, M.bit_length(m), Nat.add(d, 1n+e), Equal.sym(Nat, Nat.add(d, 1n+e), M.bit_length(m), eB), bl_fit(m))
241  +fh1 = Equal.trans(Bool, C.fits(1n+e, h), C.fits(Nat.add(d, 1n+e), m), True{}, Equal.sym(Bool, C.fits(Nat.add(d, 1n+e), m), C.fits(1n+e, h), FR.fits_hc(d, 1n+e, m)), fB)
242  +nj = L.subst(Nat, z => {C.fits(z, m) == False{} : Bool}, j, Nat.add(d, e), Equal.sym(Nat, Nat.add(d, e), j, N.sub_add(j, d, hdj)), bl_nfit(m, hz))
243  +fh0 = Equal.trans(Bool, C.fits(e, h), C.fits(Nat.add(d, e), m), False{}, Equal.sym(Bool, C.fits(Nat.add(d, e), m), C.fits(e, h), FR.fits_hc(d, e, m)), nj)
244  rj2(s, d, m, x, hb, hz, e, fh0, fh1, eB)