proofs/math/typed/f64sqc.bend source

proofs/math/typed/f64sqc.bend on the hub · documented module

import Baseimport ./f64light.bend as FLimport ../../../spec/lib/common.bend as Cimport ../../../spec/math/f64.bend as SFimport ../../../spec/math/w64.bend as SWimport ../../../src/math/f64.bend as Fimport ../../../src/math/w64.bend as Ximport ../../../src/math/u64.bend as WUimport ../../../src/math/natural.bend as Mimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ../natural/arith.bend as NRimport ../natural/sqrtn.bend as SQ2import ./width.bend as WWimport ./natcmp.bend as NCimport ./w64add.bend as WAimport ./w64sh.bend as SHimport ./f64bits.bend as FBimport ./f64cmp.bend as FCimport ./f64round.bend as FRimport ./f64rtools.bend as RTimport ./f64norm.bend as NMimport ./f64mexp.bend as EXimport ./f64sqf.bend as QF# Sqrt.value of spec/math/f64.bend: SoftFloat's f64_sqrt (NaN, infinity,# zero and negative cases, then the root of the normalized significand with# its exponent made even) is the spec's sqrt, IEEE 754-2019 §5.4.1 around the# exact-then-round square root.def m01(+m: Nat, +hl: {Nat.is_lt(m, 2n) == True{} : Bool}, +h: {Nat.is_eq(m, 1n) == False{} : Bool}) -> {m == 0n : Nat}:  match m:    case 0n:      {==}    case 1n+ +mp:      match mp:        case 0n:          NC.absurd_tf({1n == 0n : Nat}, Equal.sym(Bool, True{}, False{}, h))        case 1n+ +mq:          Empty.absurd({2n+mq == 0n : Nat}, N.lt_zero_absurd(mq, hl))def m10(+m: Nat, +hl: {Nat.is_lt(m, 2n) == True{} : Bool}, +h: {Nat.is_eq(m, 0n) == False{} : Bool}) -> {m == 1n : Nat}:  match m:    case 0n:      NC.absurd_tf({0n == 1n : Nat}, Equal.sym(Bool, True{}, False{}, h))    case 1n+ +mp:      match mp:        case 0n:          {==}        case 1n+ +mq:          Empty.absurd({2n+mq == 1n : Nat}, N.lt_zero_absurd(mq, hl))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}:  match c:    case True{}:      {==}    case False{}:      +l = FL.add_lt2(y, x, N.not_le_lt(x, y, hc))      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)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}:  halve_c(x, y, h, Nat.is_le(x, y), {==})def two_add(+a: Nat) -> {Nat.add(Nat.mul(a, 2n), 0n) == Nat.add(a, a) : Nat}:  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)))))def div_dbl(+p: Nat) -> {Nat.div(Nat.add(p, p), 2n) == p : Nat}:  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, {==}))# n = 2 * (n / 2) + (n mod 2)def half_eq(+n: Nat) -> {n == Nat.add(Nat.add(Nat.div(n, 2n), Nat.div(n, 2n)), Nat.mod(n, 2n)) : Nat}:  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)))))# (b + (K + D)) twice, then p, then s, regroupeddef 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}:  +KD = Nat.add(K, D)  +e1 = NA.add_assoc(b, KD, Nat.add(b, KD))  +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))  +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)))  +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))  +f1 = NA.add_assoc(K, D, Nat.add(K, D))  +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))  +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)))  +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))  +B2 = Nat.add(b, b)  +K2 = Nat.add(K, K)  +D2 = Nat.add(D, D)  +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)))  +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))  +g2 = NA.add_assoc(B2, Nat.add(Nat.add(K2, D2), p), s)  +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))  +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)))  +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))  +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))  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)))# the exponent step of sqn_c for any parity: 2a + p + s = 2b + q + 2171 with# s <= 53, p <= 1, K <= 1022 and 2K + p = 2043 + u gives# 2 ((a - b) - K) + 72 + s + u = 200 + qdef 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}:  +aa = Nat.add(a, a)  +bb = Nat.add(b, b)  +c54 = Nat.add(1n, 53n)  +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))  +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)  +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)))  +l3 = N.le_trans(Nat.add(bb, 2171n), Nat.add(Nat.add(aa, p), sa), Nat.add(aa, c54), l1, l2)  +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, {==}))  +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)  +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)  +k3 = N.le_add_left(Nat.add(K, K), Nat.add(1022n, 1022n), bb, SQ2.le_add2(K, 1022n, K, 1022n, hK, hK))  +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, {==}))  +k6 = N.le_trans(Nat.add(bb, Nat.add(K, K)), Nat.add(bb, 2117n), aa, k5, l5)  +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)))))  +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)  +hbK = halve(Nat.add(b, K), a, k7)  +hb = N.le_trans(b, Nat.add(b, K), a, N.le_add_right(b, K), hbK)  +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))  +D = Nat.sub(Nat.sub(a, b), K)  +DD = Nat.add(D, D)  +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))))  +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)  +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)))  +h4 = NR.add_cancel(bb, Nat.add(Nat.add(Nat.add(K, K), p), Nat.add(DD, sa)), Nat.add(q, 2171n), h3)  +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)  +W = Nat.add(u, Nat.add(DD, sa))  +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)), {==})  +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)))  +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)))  +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))  +r1 = Equal.trans(Nat, Nat.add(q, 2171n), Nat.add(2171n, q), Nat.add(1971n, Nat.add(200n, q)), NA.add_comm(q, 2171n), {==})  +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))  NR.add_cancel(1971n, Nat.add(DD, Nat.add(72n, Nat.add(sa, u))), Nat.add(200n, q), fin)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}:  jfg(a, b, sa, 0n, 0n, 1022n, 1n, hEN2, hsa, {==}, {==}, {==})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}:  jfg(a, b, sa, 0n, 1n, 1022n, 1n, hEN2, hsa, {==}, {==}, {==})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}:  jfg(a, b, sa, 1n, 0n, 1021n, 0n, hEN2, hsa, {==}, {==}, {==})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}:  jfg(a, b, sa, 1n, 1n, 1021n, 0n, hEN2, hsa, {==}, {==}, {==})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}:  Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), 1075n), Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n), 4096n), Nat.add(av0_, 4096n), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), 1075n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4097n)), Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n), 4096n), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), 1075n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3022n)), 1075n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4097n)), Equal.cong(Nat, Nat, z => Nat.add(z, 1075n), Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3022n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3022n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n), Equal.trans(Nat, Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n), Equal.cong(Nat, Nat, z => Nat.add(z, 1511n), Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.sym(Nat, Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n), N.add_zero(Nat.div(av0_, 2n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1511n), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 1511n)), Nat.add(Nat.div(av0_, 2n), 1511n), NA.add_assoc(Nat.div(av0_, 2n), 0n, 1511n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), z), Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n), Equal.trans(Nat, Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n), Equal.cong(Nat, Nat, z => Nat.add(z, 1511n), Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.sym(Nat, Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n), N.add_zero(Nat.div(av0_, 2n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1511n), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 1511n)), Nat.add(Nat.div(av0_, 2n), 1511n), NA.add_assoc(Nat.div(av0_, 2n), 0n, 1511n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.div(av0_, 2n), Nat.add(1511n, Nat.add(Nat.div(av0_, 2n), 1511n))), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3022n)), NA.add_assoc(Nat.div(av0_, 2n), 1511n, Nat.add(Nat.div(av0_, 2n), 1511n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(1511n, Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.div(av0_, 2n), 3022n), Equal.trans(Nat, Nat.add(1511n, Nat.add(Nat.div(av0_, 2n), 1511n)), Nat.add(Nat.div(av0_, 2n), Nat.add(1511n, 1511n)), Nat.add(Nat.div(av0_, 2n), 3022n), NA.add_swap(1511n, Nat.div(av0_, 2n), 1511n), {==}))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3022n)), 1075n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.add(Nat.div(av0_, 2n), 3022n), 1075n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4097n)), NA.add_assoc(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3022n), 1075n), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(Nat.add(Nat.div(av0_, 2n), 3022n), 1075n), Nat.add(Nat.div(av0_, 2n), 4097n), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 3022n), 1075n), Nat.add(Nat.div(av0_, 2n), Nat.add(3022n, 1075n)), Nat.add(Nat.div(av0_, 2n), 4097n), NA.add_assoc(Nat.div(av0_, 2n), 3022n, 1075n), {==})))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n), 4096n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4097n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n), 4096n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 1n)), 4096n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4097n)), Equal.cong(Nat, Nat, z => Nat.add(z, 4096n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 1n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), 1n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), Equal.trans(Nat, Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), Nat.add(Nat.div(av0_, 2n), 0n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), Equal.trans(Nat, Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), Nat.add(Nat.div(av0_, 2n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.div(av0_, 2n)), Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.sym(Nat, Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n), N.add_zero(Nat.div(av0_, 2n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), z), Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.sym(Nat, Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n), N.add_zero(Nat.div(av0_, 2n))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), Nat.add(Nat.div(av0_, 2n), 0n)), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, Nat.add(Nat.div(av0_, 2n), 0n))), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), NA.add_assoc(Nat.div(av0_, 2n), 0n, Nat.add(Nat.div(av0_, 2n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(0n, Nat.add(Nat.div(av0_, 2n), 0n)), Nat.add(Nat.div(av0_, 2n), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.div(av0_, 2n), 0n)), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 0n)), Nat.add(Nat.div(av0_, 2n), 0n), NA.add_swap(0n, Nat.div(av0_, 2n), 0n), {==}))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), 1n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 1n)), NA.add_assoc(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), 1n), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1n), Nat.add(Nat.div(av0_, 2n), 1n), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1n), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 1n)), Nat.add(Nat.div(av0_, 2n), 1n), NA.add_assoc(Nat.div(av0_, 2n), 0n, 1n), {==}))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 1n)), 4096n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.add(Nat.div(av0_, 2n), 1n), 4096n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4097n)), NA.add_assoc(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 1n), 4096n), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(Nat.add(Nat.div(av0_, 2n), 1n), 4096n), Nat.add(Nat.div(av0_, 2n), 4097n), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 1n), 4096n), Nat.add(Nat.div(av0_, 2n), Nat.add(1n, 4096n)), Nat.add(Nat.div(av0_, 2n), 4097n), NA.add_assoc(Nat.div(av0_, 2n), 1n, 4096n), {==})))))), Equal.cong(Nat, Nat, z => Nat.add(z, 4096n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n), av0_, Equal.sym(Nat, av0_, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n), eEN)))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}:  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)))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}:  Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n), Nat.add(Nat.add(Nat.sub(av0_, 1n), 1n), 4095n), Nat.add(Nat.sub(av0_, 1n), 4096n), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n), Nat.add(av0_, 4095n), Nat.add(Nat.add(Nat.sub(av0_, 1n), 1n), 4095n), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n), Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n), 4095n), Nat.add(av0_, 4095n), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4095n)), Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n), 4095n), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3020n)), 1075n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4095n)), Equal.cong(Nat, Nat, z => Nat.add(z, 1075n), Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3020n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3020n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n), Equal.trans(Nat, Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n), Equal.cong(Nat, Nat, z => Nat.add(z, 1510n), Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.sym(Nat, Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n), N.add_zero(Nat.div(av0_, 2n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1510n), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 1510n)), Nat.add(Nat.div(av0_, 2n), 1510n), NA.add_assoc(Nat.div(av0_, 2n), 0n, 1510n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), z), Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n), Equal.trans(Nat, Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n), Equal.cong(Nat, Nat, z => Nat.add(z, 1510n), Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.sym(Nat, Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n), N.add_zero(Nat.div(av0_, 2n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 1510n), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 1510n)), Nat.add(Nat.div(av0_, 2n), 1510n), NA.add_assoc(Nat.div(av0_, 2n), 0n, 1510n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.div(av0_, 2n), Nat.add(1510n, Nat.add(Nat.div(av0_, 2n), 1510n))), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3020n)), NA.add_assoc(Nat.div(av0_, 2n), 1510n, Nat.add(Nat.div(av0_, 2n), 1510n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(1510n, Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.div(av0_, 2n), 3020n), Equal.trans(Nat, Nat.add(1510n, Nat.add(Nat.div(av0_, 2n), 1510n)), Nat.add(Nat.div(av0_, 2n), Nat.add(1510n, 1510n)), Nat.add(Nat.div(av0_, 2n), 3020n), NA.add_swap(1510n, Nat.div(av0_, 2n), 1510n), {==}))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3020n)), 1075n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.add(Nat.div(av0_, 2n), 3020n), 1075n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4095n)), NA.add_assoc(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 3020n), 1075n), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(Nat.add(Nat.div(av0_, 2n), 3020n), 1075n), Nat.add(Nat.div(av0_, 2n), 4095n), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 3020n), 1075n), Nat.add(Nat.div(av0_, 2n), Nat.add(3020n, 1075n)), Nat.add(Nat.div(av0_, 2n), 4095n), NA.add_assoc(Nat.div(av0_, 2n), 3020n, 1075n), {==})))), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n), 4095n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4095n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n), 4095n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), 4095n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4095n)), Equal.cong(Nat, Nat, z => Nat.add(z, 4095n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), 0n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, 0n), Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), Equal.trans(Nat, Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), Nat.add(Nat.div(av0_, 2n), 0n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), Equal.trans(Nat, Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n)), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), Nat.add(Nat.div(av0_, 2n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.div(av0_, 2n)), Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.sym(Nat, Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n), N.add_zero(Nat.div(av0_, 2n)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), z), Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.sym(Nat, Nat.add(Nat.div(av0_, 2n), 0n), Nat.div(av0_, 2n), N.add_zero(Nat.div(av0_, 2n))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), Nat.add(Nat.div(av0_, 2n), 0n)), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, Nat.add(Nat.div(av0_, 2n), 0n))), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), NA.add_assoc(Nat.div(av0_, 2n), 0n, Nat.add(Nat.div(av0_, 2n), 0n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(0n, Nat.add(Nat.div(av0_, 2n), 0n)), Nat.add(Nat.div(av0_, 2n), 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(Nat.div(av0_, 2n), 0n)), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 0n)), Nat.add(Nat.div(av0_, 2n), 0n), NA.add_swap(0n, Nat.div(av0_, 2n), 0n), {==}))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), 0n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 0n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), NA.add_assoc(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), 0n), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 0n), Nat.add(Nat.div(av0_, 2n), 0n), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 0n), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 0n)), Nat.add(Nat.div(av0_, 2n), 0n), NA.add_assoc(Nat.div(av0_, 2n), 0n, 0n), {==}))))), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n)), 4095n), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 4095n)), Nat.add(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 4095n)), NA.add_assoc(Nat.div(av0_, 2n), Nat.add(Nat.div(av0_, 2n), 0n), 4095n), Equal.cong(Nat, Nat, z => Nat.add(Nat.div(av0_, 2n), z), Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 4095n), Nat.add(Nat.div(av0_, 2n), 4095n), Equal.trans(Nat, Nat.add(Nat.add(Nat.div(av0_, 2n), 0n), 4095n), Nat.add(Nat.div(av0_, 2n), Nat.add(0n, 4095n)), Nat.add(Nat.div(av0_, 2n), 4095n), NA.add_assoc(Nat.div(av0_, 2n), 0n, 4095n), {==})))))), Equal.cong(Nat, Nat, z => Nat.add(z, 4095n), Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n), av0_, Equal.sym(Nat, av0_, Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n), eEN))), Equal.cong(Nat, Nat, z => Nat.add(z, 4095n), av0_, Nat.add(Nat.sub(av0_, 1n), 1n), Equal.sym(Nat, Nat.add(Nat.sub(av0_, 1n), 1n), av0_, hE))), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(av0_, 1n), 1n), 4095n), Nat.add(Nat.sub(av0_, 1n), 4096n), Nat.add(Nat.sub(av0_, 1n), 4096n), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(av0_, 1n), 1n), 4095n), Nat.add(Nat.add(Nat.sub(av0_, 1n), 1n), 4095n), Nat.add(Nat.sub(av0_, 1n), 4096n), Equal.cong(Nat, Nat, z => Nat.add(z, 4095n), Nat.add(Nat.sub(av0_, 1n), 1n), Nat.add(Nat.sub(av0_, 1n), 1n), Equal.trans(Nat, Nat.add(Nat.sub(av0_, 1n), 1n), Nat.add(Nat.add(Nat.sub(av0_, 1n), 0n), 1n), Nat.add(Nat.sub(av0_, 1n), 1n), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), Nat.sub(av0_, 1n), Nat.add(Nat.sub(av0_, 1n), 0n), Equal.sym(Nat, Nat.add(Nat.sub(av0_, 1n), 0n), Nat.sub(av0_, 1n), N.add_zero(Nat.sub(av0_, 1n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(av0_, 1n), 0n), 1n), Nat.add(Nat.sub(av0_, 1n), Nat.add(0n, 1n)), Nat.add(Nat.sub(av0_, 1n), 1n), NA.add_assoc(Nat.sub(av0_, 1n), 0n, 1n), {==}))), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(av0_, 1n), 1n), 4095n), Nat.add(Nat.sub(av0_, 1n), Nat.add(1n, 4095n)), Nat.add(Nat.sub(av0_, 1n), 4096n), NA.add_assoc(Nat.sub(av0_, 1n), 1n, 4095n), {==})), Equal.sym(Nat, Nat.add(Nat.sub(av0_, 1n), 4096n), Nat.add(Nat.sub(av0_, 1n), 4096n), Equal.trans(Nat, Nat.add(Nat.sub(av0_, 1n), 4096n), Nat.add(Nat.add(Nat.sub(av0_, 1n), 0n), 4096n), Nat.add(Nat.sub(av0_, 1n), 4096n), Equal.cong(Nat, Nat, z => Nat.add(z, 4096n), Nat.sub(av0_, 1n), Nat.add(Nat.sub(av0_, 1n), 0n), Equal.sym(Nat, Nat.add(Nat.sub(av0_, 1n), 0n), Nat.sub(av0_, 1n), N.add_zero(Nat.sub(av0_, 1n)))), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(av0_, 1n), 0n), 4096n), Nat.add(Nat.sub(av0_, 1n), Nat.add(0n, 4096n)), Nat.add(Nat.sub(av0_, 1n), 4096n), NA.add_assoc(Nat.sub(av0_, 1n), 0n, 4096n), {==})))))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}:  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)))# sq_n on a known parity, unfolded once over variables (the four cases of# sqn_c rewrite with these instead of unfolding the square root each time)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}:  {==}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}:  {==}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}:  match o ev:    case True{} True{}:      +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)      +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)      +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)      +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)      +hsa = EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))      +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)      +mXX = N.eq_from_is_eq(Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 0n, hev)      +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))      +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))      +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)      +sv = FL.shl_v(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n, 53n, {==}, {==}, a53)      +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}))))))))      +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)))      +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))      +hE = N.add_zero(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))      +hp = sqn_c_g1(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), eEN)      +hpe = sqn_c_g2(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hp)      +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)      +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), {==}, {==})      +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})), {==}, {==})      Equal.trans(F.F64, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), True{}), F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.off()), 1075n), 2n), 1048n), X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), sqn_t(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.trans(F.F64, F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.off()), 1075n), 2n), 1048n), X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), QF.sqg(1n, {==}, X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n), h62, h60, SF.mant(F.Bits{xl, xh}), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n, 0n, hnh, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1511n), hp, hpe, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hE, SF.xexp(F.Bits{xl, xh}), n2x, SF.mant(F.Bits{xl, xh}), hMq, SF.xexp(F.Bits{xl, xh}), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), hq, hqd, Nat.sub(Nat.sub(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1021n), hj), Equal.sym(F.F64, SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), FR.pk_t(F.F64, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))))))    case True{} False{}:      +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)      +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)      +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)      +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)      +hsa = EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))      +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)      +mXX = m10(Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), NR.dm_lt(1n, SF.xexp(F.Bits{xl, xh})), hev)      +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))      +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))      +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)      +sv = FL.shl_v(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n, 53n, {==}, {==}, a53)      +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}))))))))      +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)))      +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))      +hE = N.add_zero(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))      +hp = sqn_c_g1(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), eEN)      +hpe = sqn_c_g2(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hp)      +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)      +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)))      +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}))))      Equal.trans(F.F64, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), True{}), F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.off()), 1075n), 2n), 1048n), X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), sqn_t(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.trans(F.F64, F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.off()), 1075n), 2n), 1048n), X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n)), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n)), SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), QF.sqg(1n, {==}, X.shl(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 8n), h62, h60, SF.mant(F.Bits{xl, xh}), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 0n, 1n, hnh, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1511n), hp, hpe, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hE, SF.xexp(F.Bits{xl, xh}), n2x, Nat.mul(2n, SF.mant(F.Bits{xl, xh})), hMq, Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), hq, hqd, Nat.sub(Nat.sub(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1021n), hj), Equal.sym(F.F64, SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n)), FR.pk_f(F.F64, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))))))    case False{} True{}:      +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)      +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)      +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)      +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)      +hsa = EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))      +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)      +mXX = N.eq_from_is_eq(Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), 0n, hev)      +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))      +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))      +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)      +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))))      +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))      +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)      +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}))))))      +hnh = Equal.trans(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(8n, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh}))), sv, Equal.trans(Nat, C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(8n, C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(8n, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh}))), WW.shift_comp(8n, 1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.cong(Nat, Nat, z => C.shift(8n, z), C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.trans(Nat, C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => C.shift(1n, z), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), n1x), Equal.trans(Nat, C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), C.shift(Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SF.mant(F.Bits{xl, xh})), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.sym(Nat, C.shift(Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SF.mant(F.Bits{xl, xh})), C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), WW.shift_comp(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), Equal.cong(Nat, Nat, z => C.shift(z, SF.mant(F.Bits{xl, xh})), Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), NA.add_comm(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))))))))      +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))      +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)))      +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})))      +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)))      +hp = sqn_c_g3(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), eEN, hE)      +hpe = sqn_c_g4(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hp)      +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)      +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), {==}, {==})      +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})), {==}, {==})      Equal.trans(F.F64, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), False{}), F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), F.off()), 1075n), 2n), 1048n), X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), sqn_f(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.trans(F.F64, F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), F.off()), 1075n), 2n), 1048n), X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), QF.sqg(1n, {==}, X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n), h62, h60, SF.mant(F.Bits{xl, xh}), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n, 0n, hnh, Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1510n), hp, hpe, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hE, SF.xexp(F.Bits{xl, xh}), n2x, SF.mant(F.Bits{xl, xh}), hMq, SF.xexp(F.Bits{xl, xh}), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), hq, hqd, Nat.sub(Nat.sub(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1022n), hj), Equal.sym(F.F64, SF.pick(F.F64, True{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), FR.pk_t(F.F64, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))))))    case False{} False{}:      +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)      +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)      +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)      +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)      +hsa = EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))      +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)      +mXX = m10(Nat.mod(SF.xexp(F.Bits{xl, xh}), 2n), NR.dm_lt(1n, SF.xexp(F.Bits{xl, xh})), hev)      +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))      +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))      +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)      +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))))      +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))      +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)      +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}))))))      +hnh = Equal.trans(Nat, SW.value(X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(8n, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh}))), sv, Equal.trans(Nat, C.shift(9n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(8n, C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))))), C.shift(8n, C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh}))), WW.shift_comp(8n, 1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), Equal.cong(Nat, Nat, z => C.shift(8n, z), C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.trans(Nat, C.shift(1n, SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))), C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.cong(Nat, Nat, z => C.shift(1n, z), SW.value(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), n1x), Equal.trans(Nat, C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), C.shift(Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SF.mant(F.Bits{xl, xh})), C.shift(Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), SF.mant(F.Bits{xl, xh})), Equal.sym(Nat, C.shift(Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), SF.mant(F.Bits{xl, xh})), C.shift(1n, C.shift(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), WW.shift_comp(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), Equal.cong(Nat, Nat, z => C.shift(z, SF.mant(F.Bits{xl, xh})), Nat.add(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Nat.add(NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), NA.add_comm(1n, NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})))))))))      +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))      +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)))      +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})))      +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)))      +hp = sqn_c_g3(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), eEN, hE)      +hpe = sqn_c_g4(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hp)      +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)      +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)))      +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}))))      Equal.trans(F.F64, F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), False{}), F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), F.off()), 1075n), 2n), 1048n), X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), sqn_f(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), Equal.trans(F.F64, F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), F.off()), 1075n), 2n), 1048n), X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n)), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n)), SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), QF.sqg(1n, {==}, X.shl(X.add(F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}))), 8n), h62, h60, SF.mant(F.Bits{xl, xh}), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n, 1n, hnh, Nat.sub(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 1n), Nat.add(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1510n), hp, hpe, F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), hE, SF.xexp(F.Bits{xl, xh}), n2x, Nat.mul(2n, SF.mant(F.Bits{xl, xh})), hMq, Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n), hq, hqd, Nat.sub(Nat.sub(Nat.div(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), Nat.div(SF.xexp(F.Bits{xl, xh}), 2n)), 1022n), hj), Equal.sym(F.F64, SF.pick(F.F64, False{}, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n)), FR.pk_f(F.F64, SF.sqrt_even(SF.mant(F.Bits{xl, xh}), SF.xexp(F.Bits{xl, xh})), SF.sqrt_even(Nat.mul(2n, SF.mant(F.Bits{xl, xh})), Nat.sub(SF.xexp(F.Bits{xl, xh}), 1n))))))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}:  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), {==})def simpl(+s: Bool, +a: Bool, +b: Bool, +c: Bool, +x: F.F64, +r: F.F64) -> F.F64:  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)))def sspec(+s: Bool, +a: Bool, +b: Bool, +c: Bool, +x: F.F64, +r: F.F64) -> F.F64:  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))))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}:  match s:    case True{}:      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)))))    case False{}:      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)))))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}:  match z:    case True{}:      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))))))    case False{}:      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))))))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}:  match t:    case True{}:      FL.non(x, Bool.or(Bool.not(X.is_zero(f)), s))    case False{}:      ssh2(x, s, e, f, Bool.and(Nat.is_eq(e, 0n), X.is_zero(f)))def ne2047(+E: Nat) -> {Bool.and(Nat.is_eq(E, 2047n), Nat.is_eq(E, 0n)) == False{} : Bool}:  match E:    case 0n:      {==}    case 1n+ +p:      FR.and_f(Nat.is_eq(1n+p, 2047n))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}:  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))))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}:  match aq bq cq ngv:    case True{} True{} True{} True{}:      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)))    case True{} True{} True{} False{}:      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)))    case True{} True{} False{} True{}:      {==}    case True{} True{} False{} False{}:      {==}    case True{} False{} True{} True{}:      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)))    case True{} False{} True{} False{}:      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)))    case True{} False{} False{} True{}:      {==}    case True{} False{} False{} False{}:      {==}    case False{} True{} True{} True{}:      {==}    case False{} True{} True{} False{}:      {==}    case False{} True{} False{} True{}:      {==}    case False{} True{} False{} False{}:      hR    case False{} False{} True{} True{}:      {==}    case False{} False{} True{} False{}:      hR    case False{} False{} False{} True{}:      {==}    case False{} False{} False{} False{}:      hRdef 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}:  match g:    case True{}:      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))), {==})    case False{}:      +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)      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)))def sqrt_value(+x: F.F64) -> SF.Sqrt.value(x):  match x:    case F.Bits{+xl, +xh}:      +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))      +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)))      +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})), {==}))      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)