1 import Base 2 import ./f64light.bend as FL 3 import ../../../spec/lib/common.bend as C 4 import ../../../spec/math/f64.bend as SF 5 import ../../../spec/math/w64.bend as SW 6 import ../../../src/math/f64.bend as F 7 import ../../../src/math/w64.bend as X 8 import ../../../src/math/u64.bend as WU 9 import ../../../src/math/natural.bend as M 10 import ../../lib/nat.bend as N 11 import ../../lib/logic.bend as L 12 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 13 import ../natural/arith.bend as NR 14 import ../natural/sqrtn.bend as SQ2 15 import ./width.bend as WW 16 import ./natcmp.bend as NC 17 import ./w64add.bend as WA 18 import ./w64sh.bend as SH 19 import ./f64bits.bend as FB 20 import ./f64cmp.bend as FC 21 import ./f64round.bend as FR 22 import ./f64rtools.bend as RT 23 import ./f64norm.bend as NM 24 import ./f64mexp.bend as EX 25 import ./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 32 def 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 43 def 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 54 def 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 62 def 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 65 def 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 68 def 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) 72 def 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 76 def 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 101 def 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 136 def 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 139 def 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 142 def 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 145 def 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 148 def 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(av 150 151 def 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 154 def 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 156 157 def 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) 162 def 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 165 def 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 168 def 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.m 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}), 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 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.n 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 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.Bi 266 267 def 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 270 def 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 273 def 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 276 def 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 283 def 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 290 def 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 297 def 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 304 def 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 307 def 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 342 def 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 350 def 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)