proofs/math/typed/f64sqc.bend

bend-collections-laws-math@1.0.0.0 · 356 lines · 31 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
3import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
4import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
5import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
6import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
7import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
8import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
9import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
10import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
11import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
12import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
13import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
14import bend-collections-laws-math@1.0.0.0/proofs/math/natural/sqrtn.bend as SQ2
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
20import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC
21import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
22import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
23import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64norm.bend as NM
24import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mexp.bend as EX
25import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqf.bend as QF
26
27# Sqrt.value of spec/math/f64.bend: SoftFloat's f64_sqrt (NaN, infinity,
28# zero and negative cases, then the root of the normalized significand with
29# its exponent made even) is the spec's sqrt, IEEE 754-2019 §5.4.1 around the
30# exact-then-round square root.
31
32def m01(+m: Nat, +hl: {Nat.is_lt(m, 2n) == True{} : Bool}, +h: {Nat.is_eq(m, 1n) == False{} : Bool}) -> {m == 0n : Nat}:
33  match m:
34    case 0n:
35      {==}
36    case 1n+ +mp:
37      match mp:
38        case 0n:
39          NC.absurd_tf({1n == 0n : Nat}, Equal.sym(Bool, True{}, False{}, h))
40        case 1n+ +mq:
41          Empty.absurd({2n+mq == 0n : Nat}, N.lt_zero_absurd(mq, hl))
42
43def m10(+m: Nat, +hl: {Nat.is_lt(m, 2n) == True{} : Bool}, +h: {Nat.is_eq(m, 0n) == False{} : Bool}) -> {m == 1n : Nat}:
44  match m:
45    case 0n:
46      NC.absurd_tf({0n == 1n : Nat}, Equal.sym(Bool, True{}, False{}, h))
47    case 1n+ +mp:
48      match mp:
49        case 0n:
50          {==}
51        case 1n+ +mq:
52          Empty.absurd({2n+mq == 1n : Nat}, N.lt_zero_absurd(mq, hl))
53
54def halve_c(+x: Nat, +y: Nat, +h: {Nat.is_le(Nat.add(x, x), Nat.add(y, y)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_le(x, y) == c : Bool}) -> {c == True{} : Bool}:
55  match c:
56    case True{}:
57      {==}
58    case False{}:
59      +l = FL.add_lt2(y, x, N.not_le_lt(x, y, hc))
60      Equal.trans(Bool, False{}, Nat.is_le(Nat.add(x, x), Nat.add(y, y)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(x, x), Nat.add(y, y)), False{}, N.lt_not_le(Nat.add(y, y), Nat.add(x, x), l)), h)
61
62def halve(+x: Nat, +y: Nat, +h: {Nat.is_le(Nat.add(x, x), Nat.add(y, y)) == True{} : Bool}) -> {Nat.is_le(x, y) == True{} : Bool}:
63  halve_c(x, y, h, Nat.is_le(x, y), {==})
64
65def two_add(+a: Nat) -> {Nat.add(Nat.mul(a, 2n), 0n) == Nat.add(a, a) : Nat}:
66  Equal.trans(Nat, Nat.add(Nat.mul(a, 2n), 0n), Nat.mul(a, 2n), Nat.add(a, a), N.add_zero(Nat.mul(a, 2n)), Equal.trans(Nat, Nat.mul(a, 2n), Nat.mul(2n, a), Nat.add(a, a), NA.mul_comm(a, 2n), Equal.cong(Nat, Nat, z => Nat.add(a, z), Nat.mul(1n, a), a, Equal.trans(Nat, Nat.mul(1n, a), Nat.mul(a, 1n), a, NA.mul_comm(1n, a), NA.mul_one(a)))))
67
68def div_dbl(+p: Nat) -> {Nat.div(Nat.add(p, p), 2n) == p : Nat}:
69  L.subst(Nat, z => {Nat.div(z, 2n) == p : Nat}, Nat.add(Nat.mul(p, 2n), 0n), Nat.add(p, p), two_add(p), NR.div_of(p, 1n, 0n, {==}))
70
71# n = 2 * (n / 2) + (n mod 2)
72def half_eq(+n: Nat) -> {n == Nat.add(Nat.add(Nat.div(n, 2n), Nat.div(n, 2n)), Nat.mod(n, 2n)) : Nat}:
73  Equal.trans(Nat, n, Nat.add(Nat.mul(Nat.div(n, 2n), 2n), Nat.mod(n, 2n)), Nat.add(Nat.add(Nat.div(n, 2n), Nat.div(n, 2n)), Nat.mod(n, 2n)), NR.dm_eq(1n, n), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mod(n, 2n)), Nat.mul(Nat.div(n, 2n), 2n), Nat.add(Nat.div(n, 2n), Nat.div(n, 2n)), Equal.trans(Nat, Nat.mul(Nat.div(n, 2n), 2n), Nat.add(Nat.mul(Nat.div(n, 2n), 2n), 0n), Nat.add(Nat.div(n, 2n), Nat.div(n, 2n)), Equal.sym(Nat, Nat.add(Nat.mul(Nat.div(n, 2n), 2n), 0n), Nat.mul(Nat.div(n, 2n), 2n), N.add_zero(Nat.mul(Nat.div(n, 2n), 2n))), two_add(Nat.div(n, 2n)))))
74
75# (b + (K + D)) twice, then p, then s, regrouped
76def jperm(+b: Nat, +K: Nat, +D: Nat, +p: Nat, +s: Nat) -> {Nat.add(Nat.add(Nat.add(Nat.add(b, Nat.add(K, D)), Nat.add(b, Nat.add(K, D))), p), s) == Nat.add(Nat.add(b, b), Nat.add(Nat.add(Nat.add(K, K), p), Nat.add(Nat.add(D, D), s))) : Nat}:
77  +KD = Nat.add(K, D)
78  +e1 = NA.add_assoc(b, KD, Nat.add(b, KD))
79  +e2 = Equal.cong(Nat, Nat, z => Nat.add(b, z), Nat.add(KD, Nat.add(b, KD)), Nat.add(b, Nat.add(KD, KD)), NA.add_swap(KD, b, KD))
80  +e3 = Equal.sym(Nat, Nat.add(Nat.add(b, b), Nat.add(KD, KD)), Nat.add(b, Nat.add(b, Nat.add(KD, KD))), NA.add_assoc(b, b, Nat.add(KD, KD)))
81  +eA = Equal.trans(Nat, Nat.add(Nat.add(b, KD), Nat.add(b, KD)), Nat.add(b, Nat.add(KD, Nat.add(b, KD))), Nat.add(Nat.add(b, b), Nat.add(KD, KD)), e1, Equal.trans(Nat, Nat.add(b, Nat.add(KD, Nat.add(b, KD))), Nat.add(b, Nat.add(b, Nat.add(KD, KD))), Nat.add(Nat.add(b, b), Nat.add(KD, KD)), e2, e3))
82  +f1 = NA.add_assoc(K, D, Nat.add(K, D))
83  +f2 = Equal.cong(Nat, Nat, z => Nat.add(K, z), Nat.add(D, Nat.add(K, D)), Nat.add(K, Nat.add(D, D)), NA.add_swap(D, K, D))
84  +f3 = Equal.sym(Nat, Nat.add(Nat.add(K, K), Nat.add(D, D)), Nat.add(K, Nat.add(K, Nat.add(D, D))), NA.add_assoc(K, K, Nat.add(D, D)))
85  +eKD = Equal.trans(Nat, Nat.add(KD, KD), Nat.add(K, Nat.add(D, Nat.add(K, D))), Nat.add(Nat.add(K, K), Nat.add(D, D)), f1, Equal.trans(Nat, Nat.add(K, Nat.add(D, Nat.add(K, D))), Nat.add(K, Nat.add(K, Nat.add(D, D))), Nat.add(Nat.add(K, K), Nat.add(D, D)), f2, f3))
86  +B2 = Nat.add(b, b)
87  +K2 = Nat.add(K, K)
88  +D2 = Nat.add(D, D)
89  +g0 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(z, p), s), Nat.add(Nat.add(b, KD), Nat.add(b, KD)), Nat.add(B2, Nat.add(K2, D2)), Equal.trans(Nat, Nat.add(Nat.add(b, KD), Nat.add(b, KD)), Nat.add(B2, Nat.add(KD, KD)), Nat.add(B2, Nat.add(K2, D2)), eA, Equal.cong(Nat, Nat, z => Nat.add(B2, z), Nat.add(KD, KD), Nat.add(K2, D2), eKD)))
90  +g1 = Equal.cong(Nat, Nat, z => Nat.add(z, s), Nat.add(Nat.add(B2, Nat.add(K2, D2)), p), Nat.add(B2, Nat.add(Nat.add(K2, D2), p)), NA.add_assoc(B2, Nat.add(K2, D2), p))
91  +g2 = NA.add_assoc(B2, Nat.add(Nat.add(K2, D2), p), s)
92  +h1 = Equal.cong(Nat, Nat, z => Nat.add(z, s), Nat.add(Nat.add(K2, D2), p), Nat.add(K2, Nat.add(D2, p)), NA.add_assoc(K2, D2, p))
93  +h2 = Equal.cong(Nat, Nat, z => Nat.add(z, s), Nat.add(K2, Nat.add(D2, p)), Nat.add(K2, Nat.add(p, D2)), Equal.cong(Nat, Nat, z => Nat.add(K2, z), Nat.add(D2, p), Nat.add(p, D2), NA.add_comm(D2, p)))
94  +h3 = Equal.trans(Nat, Nat.add(Nat.add(K2, Nat.add(p, D2)), s), Nat.add(Nat.add(Nat.add(K2, p), D2), s), Nat.add(Nat.add(K2, p), Nat.add(D2, s)), Equal.cong(Nat, Nat, z => Nat.add(z, s), Nat.add(K2, Nat.add(p, D2)), Nat.add(Nat.add(K2, p), D2), Equal.sym(Nat, Nat.add(Nat.add(K2, p), D2), Nat.add(K2, Nat.add(p, D2)), NA.add_assoc(K2, p, D2))), NA.add_assoc(Nat.add(K2, p), D2, s))
95  +hh = Equal.trans(Nat, Nat.add(Nat.add(Nat.add(K2, D2), p), s), Nat.add(Nat.add(K2, Nat.add(D2, p)), s), Nat.add(Nat.add(K2, p), Nat.add(D2, s)), h1, Equal.trans(Nat, Nat.add(Nat.add(K2, Nat.add(D2, p)), s), Nat.add(Nat.add(K2, Nat.add(p, D2)), s), Nat.add(Nat.add(K2, p), Nat.add(D2, s)), h2, h3))
96  Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(b, KD), Nat.add(b, KD)), p), s), Nat.add(Nat.add(Nat.add(B2, Nat.add(K2, D2)), p), s), Nat.add(B2, Nat.add(Nat.add(K2, p), Nat.add(D2, s))), g0, Equal.trans(Nat, Nat.add(Nat.add(Nat.add(B2, Nat.add(K2, D2)), p), s), Nat.add(B2, Nat.add(Nat.add(Nat.add(K2, D2), p), s)), Nat.add(B2, Nat.add(Nat.add(K2, p), Nat.add(D2, s))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(B2, Nat.add(K2, D2)), p), s), Nat.add(Nat.add(B2, Nat.add(Nat.add(K2, D2), p)), s), Nat.add(B2, Nat.add(Nat.add(Nat.add(K2, D2), p), s)), g1, g2), Equal.cong(Nat, Nat, z => Nat.add(B2, z), Nat.add(Nat.add(Nat.add(K2, D2), p), s), Nat.add(Nat.add(K2, p), Nat.add(D2, s)), hh)))
97
98# the exponent step of sqn_c for any parity: 2a + p + s = 2b + q + 2171 with
99# s <= 53, p <= 1, K <= 1022 and 2K + p = 2043 + u gives
100# 2 ((a - b) - K) + 72 + s + u = 200 + q
101def jfg(+a: Nat, +b: Nat, +sa: Nat, +p: Nat, +q: Nat, +K: Nat, +u: Nat, +hEN2: {Nat.add(Nat.add(Nat.add(a, a), p), sa) == Nat.add(Nat.add(Nat.add(b, b), q), 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hp: {Nat.is_le(p, 1n) == True{} : Bool}, +hK: {Nat.is_le(K, 1022n) == True{} : Bool}, +hKu: {Nat.add(Nat.add(K, K), p) == Nat.add(2043n, u) : Nat}) -> {Nat.add(Nat.add(Nat.sub(Nat.sub(a, b), K), Nat.sub(Nat.sub(a, b), K)), Nat.add(72n, Nat.add(sa, u))) == Nat.add(200n, q) : Nat}:
102  +aa = Nat.add(a, a)
103  +bb = Nat.add(b, b)
104  +c54 = Nat.add(1n, 53n)
105  +l0 = Equal.trans(Bool, Nat.is_le(Nat.add(bb, 2171n), Nat.add(Nat.add(bb, q), 2171n)), Nat.is_le(bb, Nat.add(bb, q)), True{}, FR.le_cancel_r(bb, Nat.add(bb, q), 2171n), N.le_add_right(bb, q))
106  +l1 = L.subst(Nat, z => {Nat.is_le(Nat.add(bb, 2171n), z) == True{} : Bool}, Nat.add(Nat.add(bb, q), 2171n), Nat.add(Nat.add(aa, p), sa), Equal.sym(Nat, Nat.add(Nat.add(aa, p), sa), Nat.add(Nat.add(bb, q), 2171n), hEN2), l0)
107  +l2 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(aa, c54)) == True{} : Bool}, Nat.add(aa, Nat.add(p, sa)), Nat.add(Nat.add(aa, p), sa), Equal.sym(Nat, Nat.add(Nat.add(aa, p), sa), Nat.add(aa, Nat.add(p, sa)), NA.add_assoc(aa, p, sa)), N.le_add_left(Nat.add(p, sa), c54, aa, SQ2.le_add2(p, 1n, sa, 53n, hp, hsa)))
108  +l3 = N.le_trans(Nat.add(bb, 2171n), Nat.add(Nat.add(aa, p), sa), Nat.add(aa, c54), l1, l2)
109  +e4 = Equal.trans(Nat, Nat.add(Nat.add(bb, 2117n), c54), Nat.add(bb, Nat.add(2117n, c54)), Nat.add(bb, 2171n), NA.add_assoc(bb, 2117n, c54), Equal.cong(Nat, Nat, z => Nat.add(bb, z), Nat.add(2117n, c54), 2171n, {==}))
110  +l4 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(aa, c54)) == True{} : Bool}, Nat.add(bb, 2171n), Nat.add(Nat.add(bb, 2117n), c54), Equal.sym(Nat, Nat.add(Nat.add(bb, 2117n), c54), Nat.add(bb, 2171n), e4), l3)
111  +l5 = Equal.trans(Bool, Nat.is_le(Nat.add(bb, 2117n), aa), Nat.is_le(Nat.add(Nat.add(bb, 2117n), c54), Nat.add(aa, c54)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(Nat.add(bb, 2117n), c54), Nat.add(aa, c54)), Nat.is_le(Nat.add(bb, 2117n), aa), FR.le_cancel_r(Nat.add(bb, 2117n), aa, c54)), l4)
112  +k3 = N.le_add_left(Nat.add(K, K), Nat.add(1022n, 1022n), bb, SQ2.le_add2(K, 1022n, K, 1022n, hK, hK))
113  +k5 = N.le_trans(Nat.add(bb, Nat.add(K, K)), Nat.add(bb, Nat.add(1022n, 1022n)), Nat.add(bb, 2117n), k3, N.le_add_left(Nat.add(1022n, 1022n), 2117n, bb, {==}))
114  +k6 = N.le_trans(Nat.add(bb, Nat.add(K, K)), Nat.add(bb, 2117n), aa, k5, l5)
115  +eBK = Equal.trans(Nat, Nat.add(Nat.add(b, K), Nat.add(b, K)), Nat.add(b, Nat.add(K, Nat.add(b, K))), Nat.add(bb, Nat.add(K, K)), NA.add_assoc(b, K, Nat.add(b, K)), Equal.trans(Nat, Nat.add(b, Nat.add(K, Nat.add(b, K))), Nat.add(b, Nat.add(b, Nat.add(K, K))), Nat.add(bb, Nat.add(K, K)), Equal.cong(Nat, Nat, z => Nat.add(b, z), Nat.add(K, Nat.add(b, K)), Nat.add(b, Nat.add(K, K)), NA.add_swap(K, b, K)), Equal.sym(Nat, Nat.add(bb, Nat.add(K, K)), Nat.add(b, Nat.add(b, Nat.add(K, K))), NA.add_assoc(b, b, Nat.add(K, K)))))
116  +k7 = L.subst(Nat, z => {Nat.is_le(z, aa) == True{} : Bool}, Nat.add(bb, Nat.add(K, K)), Nat.add(Nat.add(b, K), Nat.add(b, K)), Equal.sym(Nat, Nat.add(Nat.add(b, K), Nat.add(b, K)), Nat.add(bb, Nat.add(K, K)), eBK), k6)
117  +hbK = halve(Nat.add(b, K), a, k7)
118  +hb = N.le_trans(b, Nat.add(b, K), a, N.le_add_right(b, K), hbK)
119  +hK2 = RT.le_sub(K, b, a, L.subst(Nat, z => {Nat.is_le(z, a) == True{} : Bool}, Nat.add(b, K), Nat.add(K, b), NA.add_comm(b, K), hbK))
120  +D = Nat.sub(Nat.sub(a, b), K)
121  +DD = Nat.add(D, D)
122  +ea = Equal.trans(Nat, a, Nat.add(b, Nat.sub(a, b)), Nat.add(b, Nat.add(K, D)), Equal.sym(Nat, Nat.add(b, Nat.sub(a, b)), a, N.sub_add(a, b, hb)), Equal.cong(Nat, Nat, z => Nat.add(b, z), Nat.sub(a, b), Nat.add(K, D), Equal.sym(Nat, Nat.add(K, D), Nat.sub(a, b), N.sub_add(Nat.sub(a, b), K, hK2))))
123  +h2 = L.subst(Nat, z => {Nat.add(Nat.add(Nat.add(z, z), p), sa) == Nat.add(Nat.add(bb, q), 2171n) : Nat}, a, Nat.add(b, Nat.add(K, D)), ea, hEN2)
124  +h3 = Equal.trans(Nat, Nat.add(bb, Nat.add(Nat.add(Nat.add(K, K), p), Nat.add(DD, sa))), Nat.add(Nat.add(Nat.add(Nat.add(b, Nat.add(K, D)), Nat.add(b, Nat.add(K, D))), p), sa), Nat.add(bb, Nat.add(q, 2171n)), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.add(b, Nat.add(K, D)), Nat.add(b, Nat.add(K, D))), p), sa), Nat.add(bb, Nat.add(Nat.add(Nat.add(K, K), p), Nat.add(DD, sa))), jperm(b, K, D, p, sa)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(b, Nat.add(K, D)), Nat.add(b, Nat.add(K, D))), p), sa), Nat.add(Nat.add(bb, q), 2171n), Nat.add(bb, Nat.add(q, 2171n)), h2, NA.add_assoc(bb, q, 2171n)))
125  +h4 = NR.add_cancel(bb, Nat.add(Nat.add(Nat.add(K, K), p), Nat.add(DD, sa)), Nat.add(q, 2171n), h3)
126  +h5 = L.subst(Nat, z => {Nat.add(z, Nat.add(DD, sa)) == Nat.add(q, 2171n) : Nat}, Nat.add(Nat.add(K, K), p), Nat.add(2043n, u), hKu, h4)
127  +W = Nat.add(u, Nat.add(DD, sa))
128  +m1 = Equal.trans(Nat, Nat.add(Nat.add(2043n, u), Nat.add(DD, sa)), Nat.add(2043n, W), Nat.add(1971n, Nat.add(72n, W)), NA.add_assoc(2043n, u, Nat.add(DD, sa)), {==})
129  +m2 = Equal.trans(Nat, W, Nat.add(DD, Nat.add(u, sa)), Nat.add(DD, Nat.add(sa, u)), NA.add_swap(u, DD, sa), Equal.cong(Nat, Nat, z => Nat.add(DD, z), Nat.add(u, sa), Nat.add(sa, u), NA.add_comm(u, sa)))
130  +m3 = Equal.trans(Nat, Nat.add(72n, W), Nat.add(72n, Nat.add(DD, Nat.add(sa, u))), Nat.add(DD, Nat.add(72n, Nat.add(sa, u))), Equal.cong(Nat, Nat, z => Nat.add(72n, z), W, Nat.add(DD, Nat.add(sa, u)), m2), NA.add_swap(72n, DD, Nat.add(sa, u)))
131  +m4 = Equal.trans(Nat, Nat.add(Nat.add(2043n, u), Nat.add(DD, sa)), Nat.add(1971n, Nat.add(72n, W)), Nat.add(1971n, Nat.add(DD, Nat.add(72n, Nat.add(sa, u)))), m1, Equal.cong(Nat, Nat, z => Nat.add(1971n, z), Nat.add(72n, W), Nat.add(DD, Nat.add(72n, Nat.add(sa, u))), m3))
132  +r1 = Equal.trans(Nat, Nat.add(q, 2171n), Nat.add(2171n, q), Nat.add(1971n, Nat.add(200n, q)), NA.add_comm(q, 2171n), {==})
133  +fin = Equal.trans(Nat, Nat.add(1971n, Nat.add(DD, Nat.add(72n, Nat.add(sa, u)))), Nat.add(Nat.add(2043n, u), Nat.add(DD, sa)), Nat.add(1971n, Nat.add(200n, q)), Equal.sym(Nat, Nat.add(Nat.add(2043n, u), Nat.add(DD, sa)), Nat.add(1971n, Nat.add(DD, Nat.add(72n, Nat.add(sa, u)))), m4), Equal.trans(Nat, Nat.add(Nat.add(2043n, u), Nat.add(DD, sa)), Nat.add(q, 2171n), Nat.add(1971n, Nat.add(200n, q)), h5, r1))
134  NR.add_cancel(1971n, Nat.add(DD, Nat.add(72n, Nat.add(sa, u))), Nat.add(200n, q), fin)
135
136def jf00(+a: Nat, +b: Nat, +sa: Nat, +hEN2: {Nat.add(Nat.add(Nat.add(a, a), 0n), sa) == Nat.add(Nat.add(Nat.add(b, b), 0n), 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}) -> {Nat.add(Nat.add(Nat.sub(Nat.sub(a, b), 1022n), Nat.sub(Nat.sub(a, b), 1022n)), Nat.add(72n, Nat.add(sa, 1n))) == Nat.add(200n, 0n) : Nat}:
137  jfg(a, b, sa, 0n, 0n, 1022n, 1n, hEN2, hsa, {==}, {==}, {==})
138
139def jf01(+a: Nat, +b: Nat, +sa: Nat, +hEN2: {Nat.add(Nat.add(Nat.add(a, a), 0n), sa) == Nat.add(Nat.add(Nat.add(b, b), 1n), 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}) -> {Nat.add(Nat.add(Nat.sub(Nat.sub(a, b), 1022n), Nat.sub(Nat.sub(a, b), 1022n)), Nat.add(72n, Nat.add(sa, 1n))) == Nat.add(200n, 1n) : Nat}:
140  jfg(a, b, sa, 0n, 1n, 1022n, 1n, hEN2, hsa, {==}, {==}, {==})
141
142def jf10(+a: Nat, +b: Nat, +sa: Nat, +hEN2: {Nat.add(Nat.add(Nat.add(a, a), 1n), sa) == Nat.add(Nat.add(Nat.add(b, b), 0n), 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}) -> {Nat.add(Nat.add(Nat.sub(Nat.sub(a, b), 1021n), Nat.sub(Nat.sub(a, b), 1021n)), Nat.add(72n, Nat.add(sa, 0n))) == Nat.add(200n, 0n) : Nat}:
143  jfg(a, b, sa, 1n, 0n, 1021n, 0n, hEN2, hsa, {==}, {==}, {==})
144
145def jf11(+a: Nat, +b: Nat, +sa: Nat, +hEN2: {Nat.add(Nat.add(Nat.add(a, a), 1n), sa) == Nat.add(Nat.add(Nat.add(b, b), 1n), 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}) -> {Nat.add(Nat.add(Nat.sub(Nat.sub(a, b), 1021n), Nat.sub(Nat.sub(a, b), 1021n)), Nat.add(72n, Nat.add(sa, 0n))) == Nat.add(200n, 1n) : Nat}:
146  jfg(a, b, sa, 1n, 1n, 1021n, 0n, hEN2, hsa, {==}, {==}, {==})
147
148def sqn_c_g1(+av0_: Nat, +eEN: {av0_ == Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n) : Nat}) -> {Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), 1075n) == Nat.add(av0_, 4096n) : Nat}:
149  Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), 1075n), Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n), 4096n), Nat.add(av0_, 4096n), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), 1075n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4097n)), Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n), 4096n), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), 1075n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3022n)), 1075n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4097n)), Equal.cong(Nat, Nat, z => Nat.add(z, 1075n), Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3022n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3022n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n), Equal.trans(Nat, Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n), Equal.cong(Nat, Nat, z => Nat.add(z, 1511n), Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.sym(Nat, Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n), N.add_zero(Nat.div(av0_, 2n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1511n), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 1511n)), Nat.add(Nat.div(av0_, 2n), 1511n), NA.add_assoc(Nat.div(av0_, 2n), 0n, 1511n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), z), Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n), Equal.trans(Nat, Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n), Equal.cong(Nat, Nat, z => Nat.add(z, 1511n), Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.sym(Nat, Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n), N.add_zero(Nat.div(av0_, 2n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1511n), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 1511n)), Nat.add(Nat.div(av0_, 2n), 1511n), NA.add_assoc(Nat.div(av0_, 2n), 0n, 1511n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.div(av0_, 2n), Nat.add(1511n, Nat.add(Nat.div(av0_, 2n), 1511n))), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3022n)), NA.add_assoc(Nat.div(av0_, 2n), 1511n, Nat.add(Nat.div(av0_, 2n), 1511n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(1511n, Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.div(av0_, 2n), 3022n), Equal.trans(Nat, Nat.add(1511n, Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.div(av0_, 2n), Nat.add(1511n, 1511n)), Nat.add(Nat.div(av0_, 2n), 3022n), NA.add_swap(1511n, Nat.div(av0_, 2n), 1511n), {==}))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3022n)), 1075n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.add(Nat.div(av0_, 2n), 3022n), 1075n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4097n)), NA.add_assoc(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3022n), 1075n), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(Nat.add(Nat.div(av0_, 2n), 3022n), 1075n), Nat.add(Nat.div(av0_, 2n), 4097n), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 3022n), 1075n), Nat.add(Nat.div(av0_, 2n), Nat.add(3022n, 1075n)), Nat.add(Nat.div(av0_, 2n), 4097n), NA.add_assoc(Nat.div(av0_, 2n), 3022n, 1075n), {==})))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n), 4096n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4097n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n), 4096n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 1n)), 4096n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4097n)), Equal.cong(Nat, Nat, z => Nat.add(z, 4096n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 1n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), 1n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), Equal.trans(Nat, Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), Nat.add(Nat.div(av0_, 2n), 0n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), Equal.trans(Nat, Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), Nat.add(Nat.div(av0_, 2n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.div(av0_, 2n)), Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.sym(Nat, Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n), N.add_zero(Nat.div(av0_, 2n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), z), Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.sym(Nat, Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n), N.add_zero(Nat.div(av0_, 2n))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), Nat.add(Nat.div(av0_, 2n), 0n)), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, Nat.add(Nat.div(av0_, 2n), 0n))), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), NA.add_assoc(Nat.div(av0_, 2n), 0n, Nat.add(Nat.div(av0_, 2n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(0n, Nat.add(Nat.div(av0_, 2n), 0n)), Nat.add(Nat.div(av0_, 2n), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.div(av0_, 2n), 0n)), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 0n)), Nat.add(Nat.div(av0_, 2n), 0n), NA.add_swap(0n, Nat.div(av0_, 2n), 0n), {==}))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), 1n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 1n)), NA.add_assoc(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), 1n), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1n), Nat.add(Nat.div(av0_, 2n), 1n), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1n), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 1n)), Nat.add(Nat.div(av0_, 2n), 1n), NA.add_assoc(Nat.div(av0_, 2n), 0n, 1n), {==}))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 1n)), 4096n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.add(Nat.div(av0_, 2n), 1n), 4096n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4097n)), NA.add_assoc(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 1n), 4096n), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(Nat.add(Nat.div(av0_, 2n), 1n), 4096n), Nat.add(Nat.div(av0_, 2n), 4097n), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 1n), 4096n), Nat.add(Nat.div(av0_, 2n), Nat.add(1n, 4096n)), Nat.add(Nat.div(av0_, 2n), 4097n), NA.add_assoc(Nat.div(av0_, 2n), 1n, 4096n), {==})))))), Equal.cong(Nat, Nat, z => Nat.add(z, 4096n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n), av0_, Equal.sym(Nat, av0_, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n), eEN)))
150
151def sqn_c_g2(+av0_: Nat, +hp: {Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), 1075n) == Nat.add(av0_, 4096n) : Nat}) -> {Nat.div(Nat.sub(Nat.add(av0_, F.off()), 1075n), 2n) == Nat.add(Nat.div(av0_, 2n), 1511n) : Nat}:
152  Equal.trans(Nat, Nat.div(Nat.sub(Nat.add(av0_, F.off()), 1075n), 2n), Nat.div(Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), 2n), Nat.add(Nat.div(av0_, 2n), 1511n), Equal.cong(Nat, Nat, z => Nat.div(z, 2n), Nat.sub(Nat.add(av0_, 4096n), 1075n), Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), Equal.trans(Nat, Nat.sub(Nat.add(av0_, 4096n), 1075n), Nat.sub(Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), 1075n), 1075n), Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), Equal.cong(Nat, Nat, z => Nat.sub(z, 1075n), Nat.add(av0_, 4096n), Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), 1075n), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), 1075n), Nat.add(av0_, 4096n), hp)), FR.sub_add_l(Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), 1075n))), div_dbl(Nat.add(Nat.div(av0_, 2n), 1511n)))
153
154def sqn_c_g3(+av0_: Nat, +eEN: {av0_ == Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n) : Nat}, +hE: {Nat.add(Nat.sub(av0_, 1n), 1n) == av0_ : Nat}) -> {Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n) == Nat.add(Nat.sub(av0_, 1n), 4096n) : Nat}:
155  Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n), Nat.add(Nat.add(Nat.sub(av0_, 1n), 1n), 4095n), Nat.add(Nat.sub(av0_, 1n), 4096n), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n), Nat.add(av0_, 4095n), Nat.add(Nat.add(Nat.sub(av0_, 1n), 1n), 4095n), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n), Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n), 4095n), Nat.add(av0_, 4095n), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4095n)), Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n), 4095n), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3020n)), 1075n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4095n)), Equal.cong(Nat, Nat, z => Nat.add(z, 1075n), Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3020n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3020n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n), Equal.trans(Nat, Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n), Equal.cong(Nat, Nat, z => Nat.add(z, 1510n), Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.sym(Nat, Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n), N.add_zero(Nat.div(av0_, 2n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1510n), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 1510n)), Nat.add(Nat.div(av0_, 2n), 1510n), NA.add_assoc(Nat.div(av0_, 2n), 0n, 1510n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), z), Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n), Equal.trans(Nat, Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n), Equal.cong(Nat, Nat, z => Nat.add(z, 1510n), Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.sym(Nat, Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n), N.add_zero(Nat.div(av0_, 2n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1510n), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 1510n)), Nat.add(Nat.div(av0_, 2n), 1510n), NA.add_assoc(Nat.div(av0_, 2n), 0n, 1510n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.div(av0_, 2n), Nat.add(1510n, Nat.add(Nat.div(av0_, 2n), 1510n))), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3020n)), NA.add_assoc(Nat.div(av0_, 2n), 1510n, Nat.add(Nat.div(av0_, 2n), 1510n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(1510n, Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.div(av0_, 2n), 3020n), Equal.trans(Nat, Nat.add(1510n, Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.div(av0_, 2n), Nat.add(1510n, 1510n)), Nat.add(Nat.div(av0_, 2n), 3020n), NA.add_swap(1510n, Nat.div(av0_, 2n), 1510n), {==}))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3020n)), 1075n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.add(Nat.div(av0_, 2n), 3020n), 1075n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4095n)), NA.add_assoc(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3020n), 1075n), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(Nat.add(Nat.div(av0_, 2n), 3020n), 1075n), Nat.add(Nat.div(av0_, 2n), 4095n), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 3020n), 1075n), Nat.add(Nat.div(av0_, 2n), Nat.add(3020n, 1075n)), Nat.add(Nat.div(av0_, 2n), 4095n), NA.add_assoc(Nat.div(av0_, 2n), 3020n, 1075n), {==})))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n), 4095n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4095n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n), 4095n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), 4095n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4095n)), Equal.cong(Nat, Nat, z => Nat.add(z, 4095n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), 0n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, 0n), Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), Equal.trans(Nat, Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), Nat.add(Nat.div(av0_, 2n), 0n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), Equal.trans(Nat, Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), Nat.add(Nat.div(av0_, 2n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.div(av0_, 2n)), Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.sym(Nat, Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n), N.add_zero(Nat.div(av0_, 2n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), z), Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.sym(Nat, Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n), N.add_zero(Nat.div(av0_, 2n))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), Nat.add(Nat.div(av0_, 2n), 0n)), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, Nat.add(Nat.div(av0_, 2n), 0n))), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), NA.add_assoc(Nat.div(av0_, 2n), 0n, Nat.add(Nat.div(av0_, 2n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(0n, Nat.add(Nat.div(av0_, 2n), 0n)), Nat.add(Nat.div(av0_, 2n), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.div(av0_, 2n), 0n)), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 0n)), Nat.add(Nat.div(av0_, 2n), 0n), NA.add_swap(0n, Nat.div(av0_, 2n), 0n), {==}))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), 0n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 0n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), NA.add_assoc(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), 0n), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 0n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 0n), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 0n)), Nat.add(Nat.div(av0_, 2n), 0n), NA.add_assoc(Nat.div(av0_, 2n), 0n, 0n), {==}))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), 4095n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 4095n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4095n)), NA.add_assoc(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), 4095n), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 4095n), Nat.add(Nat.div(av0_, 2n), 4095n), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 4095n), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 4095n)), Nat.add(Nat.div(av0_, 2n), 4095n), NA.add_assoc(Nat.div(av0_, 2n), 0n, 4095n), {==})))))), Equal.cong(Nat, Nat, z => Nat.add(z, 4095n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n), av0_, Equal.sym(Nat, av0_, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n), eEN))), Equal.cong(Nat, Nat, z => Nat.add(z, 4095n), av0_, Nat.add(Nat.sub(av0_, 1n), 1n), Equal.sym(Nat, Nat.add(Nat.sub(av0_, 1n), 1n), av0_, hE))), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(av0_, 1n), 1n), 4095n), Nat.add(Nat.sub(av0_, 1n), 4096n), Nat.add(Nat.sub(av0_, 1n), 4096n), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(av0_, 1n), 1n), 4095n), Nat.add(Nat.add(Nat.sub(av0_, 1n), 1n), 4095n), Nat.add(Nat.sub(av0_, 1n), 4096n), Equal.cong(Nat, Nat, z => Nat.add(z, 4095n), Nat.add(Nat.sub(av0_, 1n), 1n), Nat.add(Nat.sub(av0_, 1n), 1n), Equal.trans(Nat, Nat.add(Nat.sub(av0_, 1n), 1n), Nat.add(Nat.add(Nat.sub(av0_, 1n), 0n), 1n), Nat.add(Nat.sub(av0_, 1n), 1n), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), Nat.sub(av0_, 1n), Nat.add(Nat.sub(av0_, 1n), 0n), Equal.sym(Nat, Nat.add(Nat.sub(av0_, 1n), 0n), Nat.sub(av0_, 1n), N.add_zero(Nat.sub(av0_, 1n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(av0_, 1n), 0n), 1n), Nat.add(Nat.sub(av0_, 1n), Nat.add(0n, 1n)), Nat.add(Nat.sub(av0_, 1n), 1n), NA.add_assoc(Nat.sub(av0_, 1n), 0n, 1n), {==}))), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(av0_, 1n), 1n), 4095n), Nat.add(Nat.sub(av0_, 1n), Nat.add(1n, 4095n)), Nat.add(Nat.sub(av0_, 1n), 4096n), NA.add_assoc(Nat.sub(av0_, 1n), 1n, 4095n), {==})), Equal.sym(Nat, Nat.add(Nat.sub(av0_, 1n), 4096n), Nat.add(Nat.sub(av0_, 1n), 4096n), Equal.trans(Nat, Nat.add(Nat.sub(av0_, 1n), 4096n), Nat.add(Nat.add(Nat.sub(av0_, 1n), 0n), 4096n), Nat.add(Nat.sub(av0_, 1n), 4096n), Equal.cong(Nat, Nat, z => Nat.add(z, 4096n), Nat.sub(av0_, 1n), Nat.add(Nat.sub(av0_, 1n), 0n), Equal.sym(Nat, Nat.add(Nat.sub(av0_, 1n), 0n), Nat.sub(av0_, 1n), N.add_zero(Nat.sub(av0_, 1n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(av0_, 1n), 0n), 4096n), Nat.add(Nat.sub(av0_, 1n), Nat.add(0n, 4096n)), Nat.add(Nat.sub(av0_, 1n), 4096n), NA.add_assoc(Nat.sub(av0_, 1n), 0n, 4096n), {==})))))
156
157def sqn_c_g4(+av0_: Nat, +hp: {Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n) == Nat.add(Nat.sub(av0_, 1n), 4096n) : Nat}) -> {Nat.div(Nat.sub(Nat.add(Nat.sub(av0_, 1n), F.off()), 1075n), 2n) == Nat.add(Nat.div(av0_, 2n), 1510n) : Nat}:
158  Equal.trans(Nat, Nat.div(Nat.sub(Nat.add(Nat.sub(av0_, 1n), F.off()), 1075n), 2n), Nat.div(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 2n), Nat.add(Nat.div(av0_, 2n), 1510n), Equal.cong(Nat, Nat, z => Nat.div(z, 2n), Nat.sub(Nat.add(Nat.sub(av0_, 1n), 4096n), 1075n), Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), Equal.trans(Nat, Nat.sub(Nat.add(Nat.sub(av0_, 1n), 4096n), 1075n), Nat.sub(Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n), 1075n), Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), Equal.cong(Nat, Nat, z => Nat.sub(z, 1075n), Nat.add(Nat.sub(av0_, 1n), 4096n), Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n), Nat.add(Nat.sub(av0_, 1n), 4096n), hp)), FR.sub_add_l(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n))), div_dbl(Nat.add(Nat.div(av0_, 2n), 1510n)))
159
160# sq_n on a known parity, unfolded once over variables (the four cases of
161# sqn_c rewrite with these instead of unfolding the square root each time)
162def sqn_t(+e: Nat, +m: WU.U64) -> {F.sq_n(e, m, True{}) == F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(e, F.off()), 1075n), 2n), 1048n), X.shl(m, 8n)) : F.F64}:
163  {==}
164
165def sqn_f(+e: Nat, +m: WU.U64) -> {F.sq_n(e, m, False{}) == F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Nat.sub(e, 1n), F.off()), 1075n), 2n), 1048n), X.shl(X.add(m, m), 8n)) : F.F64}:
166  {==}
167
168def sqn_c(+xl: U32, +xh: U32, +hzx: {Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)) == False{} : Bool}, +o: Bool, +ho: {Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n) == o : Bool}, +ev: Bool, +hev: {Nat.is_eq(Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 0n) == ev : Bool}) -> {F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), o) == SF.pick(F.F64, ev, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))) : F.F64}:
169  match o ev:
170    case True{} True{}:
171      +n1x = NM.n1(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
172      +n2x = NM.n2(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
173      +a53 = NM.n3a(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
174      +a52 = NM.n3b(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
175      +hsa = EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))
176      +mEN = N.eq_from_is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n, ho)
177      +mXX = N.eq_from_is_eq(Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 0n, hev)
178      +eEN = Equal.trans(Nat, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 1n), half_eq(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), z), Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n, mEN))
179      +eXX = Equal.trans(Nat, SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n)), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), half_eq(SF.xexp(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), z), Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 0n, mXX))
180      +hj = jf10(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 1n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), 2171n), Equal.cong(Nat, Nat, z => Nat.add(z, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 1n), F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Equal.sym(Nat, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 1n), eEN)), Equal.trans(Nat, Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(SF.xexp(F.Bits{xl, xh}), 2171n), Nat.add(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), 2171n), n2x, Equal.cong(Nat, Nat, z => Nat.add(z, 2171n), SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), eXX))), hsa)
181      +sv = FL.shl_v(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n, 53n, {==}, {==}, a53)
182      +hnh = Equal.trans(Nat, SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(8n, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), SF.mant(F.Bits{xl, xh}))), sv, Equal.cong(Nat, Nat, z => C.shift(8n, z), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), SF.mant(F.Bits{xl, xh})), Equal.trans(Nat, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), SF.mant(F.Bits{xl, xh})), n1x, Equal.cong(Nat, Nat, z => C.shift(z, SF.mant(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), Equal.sym(Nat, Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), N.add_zero(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))))))
183      +h62 = L.subst(Nat, z => {C.fits(62n, z) == True{} : Bool}, C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), Equal.sym(Nat, SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv), Equal.trans(Bool, C.fits(Nat.add(8n, 54n), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.fits(54n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), True{}, RT.fits_sh(8n, 54n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SH.fits_mono(53n, 54n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), {==}, a53)))
184      +h60 = L.subst(Nat, z => {C.fits(60n, z) == False{} : Bool}, C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), Equal.sym(Nat, SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv), Equal.trans(Bool, C.fits(Nat.add(8n, 52n), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.fits(52n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), False{}, RT.fits_sh(8n, 52n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), a52))
185      +hE = N.add_zero(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))
186      +hp = sqn_c_g1(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), eEN)
187      +hpe = sqn_c_g2(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hp)
188      +hq = Equal.sym(Nat, SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), eXX)
189      +hqd = Equal.trans(Nat, Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), {==}, {==})
190      +hMq = Equal.trans(Nat, C.shift(200n, SF.mant(F.Bits{xl, xh})), C.shift(200n, SF.mant(F.Bits{xl, xh})), C.shift(Nat.add(200n, 0n), SF.mant(F.Bits{xl, xh})), {==}, {==})
191      Equal.trans(F.F64, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), True{}), F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.off()), 1075n), 2n), 1048n), X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), sqn_t(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.trans(F.F64, F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.off()), 1075n), 2n), 1048n), X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), QF.sqg(1n, {==}, X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n), h62, h60, SF.mant(F.Bits{xl, xh}), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n, 0n, hnh, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1511n), hp, hpe, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hE, SF.xexp(F.Bits{xl, xh}), n2x, SF.mant(F.Bits{xl, xh}), hMq, SF.xexp(F.Bits{xl, xh}), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), hq, hqd, Nat.sub(Nat.sub(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1021n), hj), Equal.sym(F.F64, SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), FR.pk_t(F.F64, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))))))
192    case True{} False{}:
193      +n1x = NM.n1(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
194      +n2x = NM.n2(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
195      +a53 = NM.n3a(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
196      +a52 = NM.n3b(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
197      +hsa = EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))
198      +mEN = N.eq_from_is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n, ho)
199      +mXX = m10(Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), NR.dm_lt(1n, SF.xexp(F.Bits{xl, xh})), hev)
200      +eEN = Equal.trans(Nat, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 1n), half_eq(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), z), Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n, mEN))
201      +eXX = Equal.trans(Nat, SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n)), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), half_eq(SF.xexp(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), z), Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 1n, mXX))
202      +hj = jf11(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 1n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), 2171n), Equal.cong(Nat, Nat, z => Nat.add(z, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 1n), F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Equal.sym(Nat, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 1n), eEN)), Equal.trans(Nat, Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(SF.xexp(F.Bits{xl, xh}), 2171n), Nat.add(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), 2171n), n2x, Equal.cong(Nat, Nat, z => Nat.add(z, 2171n), SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), eXX))), hsa)
203      +sv = FL.shl_v(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n, 53n, {==}, {==}, a53)
204      +hnh = Equal.trans(Nat, SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(8n, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), SF.mant(F.Bits{xl, xh}))), sv, Equal.cong(Nat, Nat, z => C.shift(8n, z), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), SF.mant(F.Bits{xl, xh})), Equal.trans(Nat, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), SF.mant(F.Bits{xl, xh})), n1x, Equal.cong(Nat, Nat, z => C.shift(z, SF.mant(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), Equal.sym(Nat, Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), N.add_zero(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))))))
205      +h62 = L.subst(Nat, z => {C.fits(62n, z) == True{} : Bool}, C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), Equal.sym(Nat, SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv), Equal.trans(Bool, C.fits(Nat.add(8n, 54n), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.fits(54n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), True{}, RT.fits_sh(8n, 54n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SH.fits_mono(53n, 54n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), {==}, a53)))
206      +h60 = L.subst(Nat, z => {C.fits(60n, z) == False{} : Bool}, C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), Equal.sym(Nat, SW.value(X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv), Equal.trans(Bool, C.fits(Nat.add(8n, 52n), C.shift(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.fits(52n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), False{}, RT.fits_sh(8n, 52n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), a52))
207      +hE = N.add_zero(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))
208      +hp = sqn_c_g1(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), eEN)
209      +hpe = sqn_c_g2(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hp)
210      +hq = Equal.sym(Nat, SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), eXX)
211      +hqd = Equal.trans(Nat, Nat.div(Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), 2n), Nat.div(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Equal.cong(Nat, Nat, z => Nat.div(z, 2n), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), Equal.trans(Nat, Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), Nat.sub(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), 1n), Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), eXX), FR.sub_add_l(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n))), div_dbl(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)))
212      +hMq = Equal.trans(Nat, C.shift(200n, Nat.mul(2n, SF.mant(F.Bits{xl, xh}))), C.shift(200n, Nat.double(SF.mant(F.Bits{xl, xh}))), C.shift(Nat.add(200n, 1n), SF.mant(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => C.shift(200n, z), Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.double(SF.mant(F.Bits{xl, xh})), Equal.sym(Nat, Nat.double(SF.mant(F.Bits{xl, xh})), Nat.mul(2n, SF.mant(F.Bits{xl, xh})), NA.double_mul(SF.mant(F.Bits{xl, xh})))), Equal.sym(Nat, C.shift(Nat.add(200n, 1n), SF.mant(F.Bits{xl, xh})), C.shift(200n, C.shift(1n, SF.mant(F.Bits{xl, xh}))), WW.shift_comp(200n, 1n, SF.mant(F.Bits{xl, xh}))))
213      Equal.trans(F.F64, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), True{}), F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.off()), 1075n), 2n), 1048n), X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), sqn_t(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.trans(F.F64, F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.off()), 1075n), 2n), 1048n), X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n)), SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), QF.sqg(1n, {==}, X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n), h62, h60, SF.mant(F.Bits{xl, xh}), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n, 1n, hnh, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1511n), hp, hpe, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hE, SF.xexp(F.Bits{xl, xh}), n2x, Nat.mul(2n, SF.mant(F.Bits{xl, xh})), hMq, Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), hq, hqd, Nat.sub(Nat.sub(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1021n), hj), Equal.sym(F.F64, SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n)), FR.pk_f(F.F64, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))))))
214    case False{} True{}:
215      +n1x = NM.n1(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
216      +n2x = NM.n2(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
217      +a53 = NM.n3a(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
218      +a52 = NM.n3b(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
219      +hsa = EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))
220      +mEN = m01(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), NR.dm_lt(1n, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), ho)
221      +mXX = N.eq_from_is_eq(Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 0n, hev)
222      +eEN = Equal.trans(Nat, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 0n), half_eq(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), z), Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 0n, mEN))
223      +eXX = Equal.trans(Nat, SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n)), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), half_eq(SF.xexp(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), z), Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 0n, mXX))
224      +hj = jf00(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 0n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), 2171n), Equal.cong(Nat, Nat, z => Nat.add(z, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 0n), F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Equal.sym(Nat, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 0n), eEN)), Equal.trans(Nat, Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(SF.xexp(F.Bits{xl, xh}), 2171n), Nat.add(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), 2171n), n2x, Equal.cong(Nat, Nat, z => Nat.add(z, 2171n), SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), eXX))), hsa)
225      +vAA = Equal.trans(Nat, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.low(64n, Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), WA.add_value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), WW.low_fit(64n, Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SH.fits_mono(54n, 64n, Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), {==}, FR.fits_add1(53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), a53, a53))))
226      +f54 = L.subst(Nat, z => {C.fits(54n, z) == True{} : Bool}, Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.sym(Nat, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), vAA), FR.fits_add1(53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), a53, a53))
227      +sv0 = FL.shl_v(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n, 54n, {==}, {==}, f54)
228      +sv = Equal.trans(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(8n, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv0, Equal.trans(Nat, C.shift(8n, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(8n, Nat.double(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.cong(Nat, Nat, z => C.shift(8n, z), SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.double(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.trans(Nat, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.double(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), vAA, Equal.sym(Nat, Nat.double(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), NA.double_self(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))))), WW.shift_dbl(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))))
229      +hnh = Equal.trans(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(8n, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh}))), sv, Equal.trans(Nat, C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(8n, C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(8n, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh}))), WW.shift_comp(8n, 1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.cong(Nat, Nat, z => C.shift(8n, z), C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.trans(Nat, C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => C.shift(1n, z), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), n1x), Equal.trans(Nat, C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), C.shift(Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SF.mant(F.Bits{xl, xh})), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.sym(Nat, C.shift(Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SF.mant(F.Bits{xl, xh})), C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), WW.shift_comp(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), Equal.cong(Nat, Nat, z => C.shift(z, SF.mant(F.Bits{xl, xh})), Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), NA.add_comm(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))))))))
230      +h62 = L.subst(Nat, z => {C.fits(62n, z) == True{} : Bool}, C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), Equal.sym(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv), Equal.trans(Bool, C.fits(Nat.add(9n, 53n), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.fits(53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), True{}, RT.fits_sh(9n, 53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), a53))
231      +h60 = L.subst(Nat, z => {C.fits(60n, z) == False{} : Bool}, C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), Equal.sym(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv), Equal.trans(Bool, C.fits(Nat.add(9n, 51n), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.fits(51n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), False{}, RT.fits_sh(9n, 51n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), FL.nfit_mono(51n, 52n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), {==}, a52)))
232      +eg = EX.eg(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.xexp(F.Bits{xl, xh}), n2x, hsa, EX.xexp_ge(SF.efield(F.Bits{xl, xh})))
233      +hE = Equal.trans(Nat, Nat.add(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), 1n), Nat.add(1n, Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n)), F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NA.add_comm(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), 1n), N.sub_add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n, N.le_trans(1n, 4044n, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), {==}, eg)))
234      +hp = sqn_c_g3(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), eEN, hE)
235      +hpe = sqn_c_g4(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hp)
236      +hq = Equal.sym(Nat, SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 0n), eXX)
237      +hqd = Equal.trans(Nat, Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), {==}, {==})
238      +hMq = Equal.trans(Nat, C.shift(200n, SF.mant(F.Bits{xl, xh})), C.shift(200n, SF.mant(F.Bits{xl, xh})), C.shift(Nat.add(200n, 0n), SF.mant(F.Bits{xl, xh})), {==}, {==})
239      Equal.trans(F.F64, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), False{}), F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), F.off()), 1075n), 2n), 1048n), X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), sqn_f(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.trans(F.F64, F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), F.off()), 1075n), 2n), 1048n), X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), QF.sqg(1n, {==}, X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n), h62, h60, SF.mant(F.Bits{xl, xh}), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n, 0n, hnh, Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1510n), hp, hpe, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hE, SF.xexp(F.Bits{xl, xh}), n2x, SF.mant(F.Bits{xl, xh}), hMq, SF.xexp(F.Bits{xl, xh}), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), hq, hqd, Nat.sub(Nat.sub(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1022n), hj), Equal.sym(F.F64, SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), FR.pk_t(F.F64, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))))))
240    case False{} False{}:
241      +n1x = NM.n1(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
242      +n2x = NM.n2(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
243      +a53 = NM.n3a(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
244      +a52 = NM.n3b(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), FL.hea(xl, xh), FL.hfr(xl, xh), FC.hF(xl, xh), hzx)
245      +hsa = EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))
246      +mEN = m01(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), NR.dm_lt(1n, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), ho)
247      +mXX = m10(Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), NR.dm_lt(1n, SF.xexp(F.Bits{xl, xh})), hev)
248      +eEN = Equal.trans(Nat, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 0n), half_eq(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), z), Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 0n, mEN))
249      +eXX = Equal.trans(Nat, SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n)), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), half_eq(SF.xexp(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), z), Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 1n, mXX))
250      +hj = jf01(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 0n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), 2171n), Equal.cong(Nat, Nat, z => Nat.add(z, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 0n), F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Equal.sym(Nat, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n)), 0n), eEN)), Equal.trans(Nat, Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(SF.xexp(F.Bits{xl, xh}), 2171n), Nat.add(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), 2171n), n2x, Equal.cong(Nat, Nat, z => Nat.add(z, 2171n), SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), eXX))), hsa)
251      +vAA = Equal.trans(Nat, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.low(64n, Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), WA.add_value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), WW.low_fit(64n, Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SH.fits_mono(54n, 64n, Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), {==}, FR.fits_add1(53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), a53, a53))))
252      +f54 = L.subst(Nat, z => {C.fits(54n, z) == True{} : Bool}, Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.sym(Nat, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), vAA), FR.fits_add1(53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), a53, a53))
253      +sv0 = FL.shl_v(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n, 54n, {==}, {==}, f54)
254      +sv = Equal.trans(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(8n, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv0, Equal.trans(Nat, C.shift(8n, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(8n, Nat.double(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.cong(Nat, Nat, z => C.shift(8n, z), SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.double(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.trans(Nat, SW.value(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.double(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), vAA, Equal.sym(Nat, Nat.double(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Nat.add(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), NA.double_self(SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))))), WW.shift_dbl(8n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))))
255      +hnh = Equal.trans(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(8n, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh}))), sv, Equal.trans(Nat, C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(8n, C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(8n, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh}))), WW.shift_comp(8n, 1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.cong(Nat, Nat, z => C.shift(8n, z), C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.trans(Nat, C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => C.shift(1n, z), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), n1x), Equal.trans(Nat, C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), C.shift(Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SF.mant(F.Bits{xl, xh})), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.sym(Nat, C.shift(Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SF.mant(F.Bits{xl, xh})), C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), WW.shift_comp(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), Equal.cong(Nat, Nat, z => C.shift(z, SF.mant(F.Bits{xl, xh})), Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), NA.add_comm(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))))))))
256      +h62 = L.subst(Nat, z => {C.fits(62n, z) == True{} : Bool}, C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), Equal.sym(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv), Equal.trans(Bool, C.fits(Nat.add(9n, 53n), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.fits(53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), True{}, RT.fits_sh(9n, 53n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), a53))
257      +h60 = L.subst(Nat, z => {C.fits(60n, z) == False{} : Bool}, C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), Equal.sym(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), sv), Equal.trans(Bool, C.fits(Nat.add(9n, 51n), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.fits(51n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), False{}, RT.fits_sh(9n, 51n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), FL.nfit_mono(51n, 52n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), {==}, a52)))
258      +eg = EX.eg(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.xexp(F.Bits{xl, xh}), n2x, hsa, EX.xexp_ge(SF.efield(F.Bits{xl, xh})))
259      +hE = Equal.trans(Nat, Nat.add(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), 1n), Nat.add(1n, Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n)), F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NA.add_comm(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), 1n), N.sub_add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n, N.le_trans(1n, 4044n, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), {==}, eg)))
260      +hp = sqn_c_g3(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), eEN, hE)
261      +hpe = sqn_c_g4(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hp)
262      +hq = Equal.sym(Nat, SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), eXX)
263      +hqd = Equal.trans(Nat, Nat.div(Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), 2n), Nat.div(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Equal.cong(Nat, Nat, z => Nat.div(z, 2n), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), Equal.trans(Nat, Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), Nat.sub(Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), 1n), Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), SF.xexp(F.Bits{xl, xh}), Nat.add(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n), eXX), FR.sub_add_l(Nat.add(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1n))), div_dbl(Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)))
264      +hMq = Equal.trans(Nat, C.shift(200n, Nat.mul(2n, SF.mant(F.Bits{xl, xh}))), C.shift(200n, Nat.double(SF.mant(F.Bits{xl, xh}))), C.shift(Nat.add(200n, 1n), SF.mant(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => C.shift(200n, z), Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.double(SF.mant(F.Bits{xl, xh})), Equal.sym(Nat, Nat.double(SF.mant(F.Bits{xl, xh})), Nat.mul(2n, SF.mant(F.Bits{xl, xh})), NA.double_mul(SF.mant(F.Bits{xl, xh})))), Equal.sym(Nat, C.shift(Nat.add(200n, 1n), SF.mant(F.Bits{xl, xh})), C.shift(200n, C.shift(1n, SF.mant(F.Bits{xl, xh}))), WW.shift_comp(200n, 1n, SF.mant(F.Bits{xl, xh}))))
265      Equal.trans(F.F64, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), False{}), F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), F.off()), 1075n), 2n), 1048n), X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), sqn_f(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.trans(F.F64, F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), F.off()), 1075n), 2n), 1048n), X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n)), SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), QF.sqg(1n, {==}, X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n), h62, h60, SF.mant(F.Bits{xl, xh}), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n, 1n, hnh, Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1510n), hp, hpe, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hE, SF.xexp(F.Bits{xl, xh}), n2x, Nat.mul(2n, SF.mant(F.Bits{xl, xh})), hMq, Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), hq, hqd, Nat.sub(Nat.sub(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1022n), hj), Equal.sym(F.F64, SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n)), FR.pk_f(F.F64, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))))))
266
267def sqfin(+xl: U32, +xh: U32, +hzx: {Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)) == False{} : Bool}) -> {F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n)) == SF.sqrt_fin(F.Bits{xl, xh}) : F.F64}:
268  sqn_c(xl, xh, hzx, Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n), {==}, Nat.is_eq(Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 0n), {==})
269
270def simpl(+s: Bool, +a: Bool, +b: Bool, +c: Bool, +x: F.F64, +r: F.F64) -> F.F64:
271  SF.pick(F.F64, a, SF.pick(F.F64, Bool.or(Bool.not(b), s), F.nan(), x), SF.pick(F.F64, Bool.and(c, b), x, SF.pick(F.F64, s, F.nan(), r)))
272
273def sspec(+s: Bool, +a: Bool, +b: Bool, +c: Bool, +x: F.F64, +r: F.F64) -> F.F64:
274  SF.pick(F.F64, Bool.and(a, Bool.not(b)), SF.qnan(), SF.pick(F.F64, Bool.and(c, b), x, SF.pick(F.F64, s, SF.qnan(), SF.pick(F.F64, Bool.and(a, b), x, r))))
275
276def ssh3(+e: Nat, +f: WU.U64, +s: Bool) -> {F.sq_pos(e, f, s) == SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n))) : F.F64}:
277  match s:
278    case True{}:
279      Equal.trans(F.F64, F.sq_pos(e, f, True{}), F.nan(), SF.pick(F.F64, True{}, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n))), {==}, Equal.sym(F.F64, SF.pick(F.F64, True{}, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n))), F.nan(), FR.pk_t(F.F64, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n)))))
280    case False{}:
281      Equal.trans(F.F64, F.sq_pos(e, f, False{}), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n)), SF.pick(F.F64, False{}, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n))), {==}, Equal.sym(F.F64, SF.pick(F.F64, False{}, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n))), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n)), FR.pk_f(F.F64, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n)))))
282
283def ssh2(+x: F.F64, +s: Bool, +e: Nat, +f: WU.U64, +z: Bool) -> {F.sq_sign(x, s, e, f, z) == SF.pick(F.F64, z, x, SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n)))) : F.F64}:
284  match z:
285    case True{}:
286      Equal.trans(F.F64, F.sq_sign(x, s, e, f, True{}), x, SF.pick(F.F64, True{}, x, SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n)))), {==}, Equal.sym(F.F64, SF.pick(F.F64, True{}, x, SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n)))), x, FR.pk_t(F.F64, x, SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n))))))
287    case False{}:
288      Equal.trans(F.F64, F.sq_sign(x, s, e, f, False{}), SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n))), SF.pick(F.F64, False{}, x, SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n)))), ssh3(e, f, s), Equal.sym(F.F64, SF.pick(F.F64, False{}, x, SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n)))), SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n))), FR.pk_f(F.F64, x, SF.pick(F.F64, s, F.nan(), F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n))))))
289
290def ssh1(+x: F.F64, +s: Bool, +e: Nat, +f: WU.U64, +t: Bool) -> {F.sq_cls(x, s, e, f, t) == simpl(s, t, X.is_zero(f), Nat.is_eq(e, 0n), x, F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n))) : F.F64}:
291  match t:
292    case True{}:
293      FL.non(x, Bool.or(Bool.not(X.is_zero(f)), s))
294    case False{}:
295      ssh2(x, s, e, f, Bool.and(Nat.is_eq(e, 0n), X.is_zero(f)))
296
297def ne2047(+E: Nat) -> {Bool.and(Nat.is_eq(E, 2047n), Nat.is_eq(E, 0n)) == False{} : Bool}:
298  match E:
299    case 0n:
300      {==}
301    case 1n+ +p:
302      FR.and_f(Nat.is_eq(1n+p, 2047n))
303
304def sswap(+s1: Bool, +s2: Bool, +hs: {s1 == s2 : Bool}, +x: F.F64, +r: F.F64, +p1: Bool, +q1: Bool, +h0: {p1 == q1 : Bool}, +p2: Bool, +q2: Bool, +h1: {p2 == q2 : Bool}, +p3: Bool, +q3: Bool, +h2: {p3 == q3 : Bool}) -> {simpl(s1, p1, p2, p3, x, r) == simpl(s2, q1, q2, q3, x, r) : F.F64}:
305  Equal.trans(F.F64, simpl(s1, p1, p2, p3, x, r), simpl(s2, p1, p2, p3, x, r), simpl(s2, q1, q2, q3, x, r), Equal.cong(Bool, F.F64, w => simpl(w, p1, p2, p3, x, r), s1, s2, hs), Equal.trans(F.F64, simpl(s2, p1, p2, p3, x, r), simpl(s2, q1, p2, p3, x, r), simpl(s2, q1, q2, q3, x, r), Equal.cong(Bool, F.F64, w => simpl(s2, w, p2, p3, x, r), p1, q1, h0), Equal.trans(F.F64, simpl(s2, q1, p2, p3, x, r), simpl(s2, q1, q2, p3, x, r), simpl(s2, q1, q2, q3, x, r), Equal.cong(Bool, F.F64, w => simpl(s2, q1, w, p3, x, r), p2, q2, h1), Equal.cong(Bool, F.F64, w => simpl(s2, q1, q2, w, x, r), p3, q3, h2))))
306
307def scase(+xl: U32, +xh: U32, +r1: F.F64, +r2: F.F64, +aq: Bool, +ha: {Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n) == aq : Bool}, +bq: Bool, +cq: Bool, +hc: {Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n) == cq : Bool}, +ngv: Bool, +hR: {SF.pick(F.F64, Bool.or(Bool.or(aq, Bool.and(cq, bq)), ngv), r2, r1) == r2 : F.F64}) -> {simpl(ngv, aq, bq, cq, F.Bits{xl, xh}, r1) == sspec(ngv, aq, bq, cq, F.Bits{xl, xh}, r2) : F.F64}:
308  match aq bq cq ngv:
309    case True{} True{} True{} True{}:
310      NC.absurd_tf({simpl(True{}, True{}, True{}, True{}, F.Bits{xl, xh}, r1) == sspec(True{}, True{}, True{}, True{}, F.Bits{xl, xh}, r2) : F.F64}, Equal.trans(Bool, False{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, ne2047(SF.efield(F.Bits{xl, xh}))), Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha), hc)))
311    case True{} True{} True{} False{}:
312      NC.absurd_tf({simpl(False{}, True{}, True{}, True{}, F.Bits{xl, xh}, r1) == sspec(False{}, True{}, True{}, True{}, F.Bits{xl, xh}, r2) : F.F64}, Equal.trans(Bool, False{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, ne2047(SF.efield(F.Bits{xl, xh}))), Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha), hc)))
313    case True{} True{} False{} True{}:
314      {==}
315    case True{} True{} False{} False{}:
316      {==}
317    case True{} False{} True{} True{}:
318      NC.absurd_tf({simpl(True{}, True{}, False{}, True{}, F.Bits{xl, xh}, r1) == sspec(True{}, True{}, False{}, True{}, F.Bits{xl, xh}, r2) : F.F64}, Equal.trans(Bool, False{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, ne2047(SF.efield(F.Bits{xl, xh}))), Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha), hc)))
319    case True{} False{} True{} False{}:
320      NC.absurd_tf({simpl(False{}, True{}, False{}, True{}, F.Bits{xl, xh}, r1) == sspec(False{}, True{}, False{}, True{}, F.Bits{xl, xh}, r2) : F.F64}, Equal.trans(Bool, False{}, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.sym(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), False{}, ne2047(SF.efield(F.Bits{xl, xh}))), Equal.trans(Bool, Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Bool.and(True{}, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), True{}, Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n)), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha), hc)))
321    case True{} False{} False{} True{}:
322      {==}
323    case True{} False{} False{} False{}:
324      {==}
325    case False{} True{} True{} True{}:
326      {==}
327    case False{} True{} True{} False{}:
328      {==}
329    case False{} True{} False{} True{}:
330      {==}
331    case False{} True{} False{} False{}:
332      hR
333    case False{} False{} True{} True{}:
334      {==}
335    case False{} False{} True{} False{}:
336      hR
337    case False{} False{} False{} True{}:
338      {==}
339    case False{} False{} False{} False{}:
340      hR
341
342def sR_c(+xl: U32, +xh: U32, +g: Bool, +hg: {Bool.or(Bool.or(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n))), SF.sign(F.Bits{xl, xh})) == g : Bool}) -> {SF.pick(F.F64, g, SF.sqrt_fin(F.Bits{xl, xh}), F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n))) == SF.sqrt_fin(F.Bits{xl, xh}) : F.F64}:
343  match g:
344    case True{}:
345      Equal.trans(F.F64, SF.pick(F.F64, True{}, SF.sqrt_fin(F.Bits{xl, xh}), F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n))), SF.sqrt_fin(F.Bits{xl, xh}), SF.sqrt_fin(F.Bits{xl, xh}), FR.pk_t(F.F64, SF.sqrt_fin(F.Bits{xl, xh}), F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n))), {==})
346    case False{}:
347      +h1 = FC.or_l(Bool.or(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n))), SF.sign(F.Bits{xl, xh}), hg)
348      Equal.trans(F.F64, SF.pick(F.F64, False{}, SF.sqrt_fin(F.Bits{xl, xh}), F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n))), F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n)), SF.sqrt_fin(F.Bits{xl, xh}), FR.pk_f(F.F64, SF.sqrt_fin(F.Bits{xl, xh}), F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n))), sqfin(xl, xh, FC.or_r(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), h1)))
349
350def sqrt_value(+x: F.F64) -> SF.Sqrt.value(x):
351  match x:
352    case F.Bits{+xl, +xh}:
353      +i1 = ssh1(F.Bits{xl, xh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n))
354      +i2 = sswap(F.signbit(F.Bits{xl, xh}), SF.sign(F.Bits{xl, xh}), FB.signbit_value(F.Bits{xl, xh}), F.Bits{xl, xh}, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n)), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 2047n), F.exp_field(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), FL.hea(xl, xh)), X.is_zero(F.frac(F.Bits{xl, xh})), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), FB.fz_g(xl, xh, 1048575, {==}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), F.exp_field(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), FL.hea(xl, xh)))
355      +i3 = scase(xl, xh, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n)), SF.sqrt_fin(F.Bits{xl, xh}), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), {==}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), {==}, SF.sign(F.Bits{xl, xh}), sR_c(xl, xh, Bool.or(Bool.or(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n))), SF.sign(F.Bits{xl, xh})), {==}))
356      Equal.trans(F.F64, F.sq_cls(F.Bits{xl, xh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n)), simpl(SF.sign(F.Bits{xl, xh}), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), F.Bits{xl, xh}, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n))), sspec(SF.sign(F.Bits{xl, xh}), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), F.Bits{xl, xh}, SF.sqrt_fin(F.Bits{xl, xh})), Equal.trans(F.F64, F.sq_cls(F.Bits{xl, xh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n)), simpl(F.signbit(F.Bits{xl, xh}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n), X.is_zero(F.frac(F.Bits{xl, xh})), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 0n), F.Bits{xl, xh}, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n))), simpl(SF.sign(F.Bits{xl, xh}), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), F.Bits{xl, xh}, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n))), i1, i2), i3)