import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/f64.bend as SF
import ../../../spec/math/w64.bend as SW
import ../../../src/math/f64.bend as F
import ../../../src/math/u64.bend as WU
import ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ./width.bend as WW
import ./f64round.bend as FR
import ./f64sqv.bend as QV
import ./f64sqr.bend as QR
import ./f64sqs.bend as QS
import ./f64sqx.bend as QX

# SoftFloat's even-exponent square root (sq_even with its 128-bit root) is
# the spec's sqrt_even, once the significands and exponents are matched.

def p_ge(+p: Nat, +Ep: Nat, +hp: {Nat.add(Nat.add(p, p), 1075n) == Nat.add(Ep, 4096n) : Nat}, +c: Bool, +hc: {Nat.is_lt(p, 1132n) == c : Bool}) -> {c == False{} : Bool}:
  match c:
    case True{}:
      +l1 = N.lt_trans(Nat.add(p, p), Nat.add(1132n, p), 2264n, Equal.trans(Bool, Nat.is_lt(Nat.add(p, p), Nat.add(1132n, p)), Nat.is_lt(p, 1132n), True{}, WW.lt_cancel_r(p, 1132n, p), hc), N.lt_le_trans(Nat.add(1132n, p), Nat.add(1132n, 1132n), 2264n, Equal.trans(Bool, Nat.is_lt(Nat.add(1132n, p), Nat.add(1132n, 1132n)), Nat.is_lt(p, 1132n), True{}, WW.lt_cancel_l(1132n, p, 1132n), hc), {==}))
      +l2 = L.subst(Nat, z => {Nat.is_le(Nat.add(3021n, 1075n), z) == True{} : Bool}, Nat.add(Ep, 4096n), Nat.add(Nat.add(p, p), 1075n), Equal.sym(Nat, Nat.add(Nat.add(p, p), 1075n), Nat.add(Ep, 4096n), hp), N.le_trans(4096n, 4096n, Nat.add(Ep, 4096n), {==}, L.subst(Nat, z => {Nat.is_le(4096n, z) == True{} : Bool}, Nat.add(4096n, Ep), Nat.add(Ep, 4096n), NA.add_comm(4096n, Ep), N.le_add_right(4096n, Ep))))
      +l3 = Equal.trans(Bool, Nat.is_le(3021n, Nat.add(p, p)), Nat.is_le(Nat.add(3021n, 1075n), Nat.add(Nat.add(p, p), 1075n)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(3021n, 1075n), Nat.add(Nat.add(p, p), 1075n)), Nat.is_le(3021n, Nat.add(p, p)), FR.le_cancel_r(3021n, Nat.add(p, p), 1075n)), l2)
      Equal.trans(Bool, True{}, Nat.is_lt(Nat.add(p, p), 3021n), False{}, Equal.sym(Bool, Nat.is_lt(Nat.add(p, p), 3021n), True{}, N.lt_le_trans(Nat.add(p, p), 2264n, 3021n, l1, {==})), N.le_not_lt(Nat.add(p, p), 3021n, l3))
    case False{}:
      {==}

def shift_nest(+j: Nat, +sc: Nat, +MX: Nat) -> {C.shift(j, C.shift(j, C.shift(64n, C.shift(8n, C.shift(sc, MX))))) == C.shift(Nat.add(Nat.add(j, j), Nat.add(72n, sc)), MX) : Nat}:
  +e1 = Equal.sym(Nat, C.shift(Nat.add(8n, sc), MX), C.shift(8n, C.shift(sc, MX)), WW.shift_comp(8n, sc, MX))
  +e2 = Equal.sym(Nat, C.shift(Nat.add(64n, Nat.add(8n, sc)), MX), C.shift(64n, C.shift(Nat.add(8n, sc), MX)), WW.shift_comp(64n, Nat.add(8n, sc), MX))
  +e3 = Equal.sym(Nat, C.shift(Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), MX), C.shift(j, C.shift(Nat.add(64n, Nat.add(8n, sc)), MX)), WW.shift_comp(j, Nat.add(64n, Nat.add(8n, sc)), MX))
  +e4 = Equal.sym(Nat, C.shift(Nat.add(j, Nat.add(j, Nat.add(64n, Nat.add(8n, sc)))), MX), C.shift(j, C.shift(Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), MX)), WW.shift_comp(j, Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), MX))
  +e5 = Equal.cong(Nat, Nat, z => C.shift(z, MX), Nat.add(j, Nat.add(j, Nat.add(64n, Nat.add(8n, sc)))), Nat.add(Nat.add(j, j), Nat.add(72n, sc)), Equal.trans(Nat, Nat.add(j, Nat.add(j, Nat.add(64n, Nat.add(8n, sc)))), Nat.add(j, Nat.add(j, Nat.add(sc, 72n))), Nat.add(Nat.add(j, j), Nat.add(72n, sc)), Equal.trans(Nat, Nat.add(j, Nat.add(j, Nat.add(64n, Nat.add(8n, sc)))), Nat.add(Nat.add(j, 0n), Nat.add(j, Nat.add(sc, 72n))), Nat.add(j, Nat.add(j, Nat.add(sc, 72n))), Equal.trans(Nat, Nat.add(j, Nat.add(j, Nat.add(64n, Nat.add(8n, sc)))), Nat.add(Nat.add(j, 0n), Nat.add(j, Nat.add(64n, Nat.add(8n, sc)))), Nat.add(Nat.add(j, 0n), Nat.add(j, Nat.add(sc, 72n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(j, Nat.add(64n, Nat.add(8n, sc)))), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, 0n), z), Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), Nat.add(j, Nat.add(sc, 72n)), Equal.trans(Nat, Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), Nat.add(Nat.add(j, 0n), Nat.add(sc, 72n)), Nat.add(j, Nat.add(sc, 72n)), Equal.trans(Nat, Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), Nat.add(Nat.add(j, 0n), Nat.add(64n, Nat.add(8n, sc))), Nat.add(Nat.add(j, 0n), Nat.add(sc, 72n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(64n, Nat.add(8n, sc))), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, 0n), z), Nat.add(64n, Nat.add(8n, sc)), Nat.add(sc, 72n), Equal.trans(Nat, Nat.add(64n, Nat.add(8n, sc)), Nat.add(64n, Nat.add(sc, 8n)), Nat.add(sc, 72n), Equal.cong(Nat, Nat, z => Nat.add(64n, z), Nat.add(8n, sc), Nat.add(sc, 8n), Equal.trans(Nat, Nat.add(8n, sc), Nat.add(8n, Nat.add(sc, 0n)), Nat.add(sc, 8n), Equal.cong(Nat, Nat, z => Nat.add(8n, z), sc, Nat.add(sc, 0n), Equal.sym(Nat, Nat.add(sc, 0n), sc, N.add_zero(sc))), Equal.trans(Nat, Nat.add(8n, Nat.add(sc, 0n)), Nat.add(sc, Nat.add(8n, 0n)), Nat.add(sc, 8n), NA.add_swap(8n, sc, 0n), {==}))), Equal.trans(Nat, Nat.add(64n, Nat.add(sc, 8n)), Nat.add(sc, Nat.add(64n, 8n)), Nat.add(sc, 72n), NA.add_swap(64n, sc, 8n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(j, 0n), Nat.add(sc, 72n)), Nat.add(j, Nat.add(0n, Nat.add(sc, 72n))), Nat.add(j, Nat.add(sc, 72n)), NA.add_assoc(j, 0n, Nat.add(sc, 72n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(0n, Nat.add(sc, 72n)), Nat.add(sc, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(sc, 72n)), Nat.add(sc, Nat.add(0n, 72n)), Nat.add(sc, 72n), NA.add_swap(0n, sc, 72n), {==})))))), Equal.trans(Nat, Nat.add(Nat.add(j, 0n), Nat.add(j, Nat.add(sc, 72n))), Nat.add(j, Nat.add(0n, Nat.add(j, Nat.add(sc, 72n)))), Nat.add(j, Nat.add(j, Nat.add(sc, 72n))), NA.add_assoc(j, 0n, Nat.add(j, Nat.add(sc, 72n))), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(0n, Nat.add(j, Nat.add(sc, 72n))), Nat.add(j, Nat.add(sc, 72n)), Equal.trans(Nat, Nat.add(0n, Nat.add(j, Nat.add(sc, 72n))), Nat.add(j, Nat.add(0n, Nat.add(sc, 72n))), Nat.add(j, Nat.add(sc, 72n)), NA.add_swap(0n, j, Nat.add(sc, 72n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(0n, Nat.add(sc, 72n)), Nat.add(sc, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(sc, 72n)), Nat.add(sc, Nat.add(0n, 72n)), Nat.add(sc, 72n), NA.add_swap(0n, sc, 72n), {==})))))), Equal.sym(Nat, Nat.add(Nat.add(j, j), Nat.add(72n, sc)), Nat.add(j, Nat.add(j, Nat.add(sc, 72n))), Equal.trans(Nat, Nat.add(Nat.add(j, j), Nat.add(72n, sc)), Nat.add(Nat.add(j, Nat.add(j, 0n)), Nat.add(sc, 72n)), Nat.add(j, Nat.add(j, Nat.add(sc, 72n))), Equal.trans(Nat, Nat.add(Nat.add(j, j), Nat.add(72n, sc)), Nat.add(Nat.add(j, Nat.add(j, 0n)), Nat.add(72n, sc)), Nat.add(Nat.add(j, Nat.add(j, 0n)), Nat.add(sc, 72n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(72n, sc)), Nat.add(j, j), Nat.add(j, Nat.add(j, 0n)), Equal.trans(Nat, Nat.add(j, j), Nat.add(Nat.add(j, 0n), Nat.add(j, 0n)), Nat.add(j, Nat.add(j, 0n)), Equal.trans(Nat, Nat.add(j, j), Nat.add(Nat.add(j, 0n), j), Nat.add(Nat.add(j, 0n), Nat.add(j, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, j), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, 0n), z), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)))), Equal.trans(Nat, Nat.add(Nat.add(j, 0n), Nat.add(j, 0n)), Nat.add(j, Nat.add(0n, Nat.add(j, 0n))), Nat.add(j, Nat.add(j, 0n)), NA.add_assoc(j, 0n, Nat.add(j, 0n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(0n, Nat.add(j, 0n)), Nat.add(j, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(j, 0n)), Nat.add(j, Nat.add(0n, 0n)), Nat.add(j, 0n), NA.add_swap(0n, j, 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(j, Nat.add(j, 0n)), z), Nat.add(72n, sc), Nat.add(sc, 72n), Equal.trans(Nat, Nat.add(72n, sc), Nat.add(72n, Nat.add(sc, 0n)), Nat.add(sc, 72n), Equal.cong(Nat, Nat, z => Nat.add(72n, z), sc, Nat.add(sc, 0n), Equal.sym(Nat, Nat.add(sc, 0n), sc, N.add_zero(sc))), Equal.trans(Nat, Nat.add(72n, Nat.add(sc, 0n)), Nat.add(sc, Nat.add(72n, 0n)), Nat.add(sc, 72n), NA.add_swap(72n, sc, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(j, Nat.add(j, 0n)), Nat.add(sc, 72n)), Nat.add(j, Nat.add(Nat.add(j, 0n), Nat.add(sc, 72n))), Nat.add(j, Nat.add(j, Nat.add(sc, 72n))), NA.add_assoc(j, Nat.add(j, 0n), Nat.add(sc, 72n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(Nat.add(j, 0n), Nat.add(sc, 72n)), Nat.add(j, Nat.add(sc, 72n)), Equal.trans(Nat, Nat.add(Nat.add(j, 0n), Nat.add(sc, 72n)), Nat.add(j, Nat.add(0n, Nat.add(sc, 72n))), Nat.add(j, Nat.add(sc, 72n)), NA.add_assoc(j, 0n, Nat.add(sc, 72n)), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(0n, Nat.add(sc, 72n)), Nat.add(sc, 72n), Equal.trans(Nat, Nat.add(0n, Nat.add(sc, 72n)), Nat.add(sc, Nat.add(0n, 72n)), Nat.add(sc, 72n), NA.add_swap(0n, sc, 72n), {==})))))))))
  +c1 = Equal.cong(Nat, Nat, z => C.shift(j, C.shift(j, C.shift(64n, z))), C.shift(8n, C.shift(sc, MX)), C.shift(Nat.add(8n, sc), MX), e1)
  +c2 = Equal.cong(Nat, Nat, z => C.shift(j, C.shift(j, z)), C.shift(64n, C.shift(Nat.add(8n, sc), MX)), C.shift(Nat.add(64n, Nat.add(8n, sc)), MX), e2)
  +c3 = Equal.cong(Nat, Nat, z => C.shift(j, z), C.shift(j, C.shift(Nat.add(64n, Nat.add(8n, sc)), MX)), C.shift(Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), MX), e3)
  Equal.trans(Nat, C.shift(j, C.shift(j, C.shift(64n, C.shift(8n, C.shift(sc, MX))))), C.shift(j, C.shift(j, C.shift(64n, C.shift(Nat.add(8n, sc), MX)))), C.shift(Nat.add(Nat.add(j, j), Nat.add(72n, sc)), MX), c1, Equal.trans(Nat, C.shift(j, C.shift(j, C.shift(64n, C.shift(Nat.add(8n, sc), MX)))), C.shift(j, C.shift(j, C.shift(Nat.add(64n, Nat.add(8n, sc)), MX))), C.shift(Nat.add(Nat.add(j, j), Nat.add(72n, sc)), MX), c2, Equal.trans(Nat, C.shift(j, C.shift(j, C.shift(Nat.add(64n, Nat.add(8n, sc)), MX))), C.shift(j, C.shift(Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), MX)), C.shift(Nat.add(Nat.add(j, j), Nat.add(72n, sc)), MX), c3, Equal.trans(Nat, C.shift(j, C.shift(Nat.add(j, Nat.add(64n, Nat.add(8n, sc))), MX)), C.shift(Nat.add(j, Nat.add(j, Nat.add(64n, Nat.add(8n, sc)))), MX), C.shift(Nat.add(Nat.add(j, j), Nat.add(72n, sc)), MX), e4, e5))))

# the generic even-exponent root
def sqg(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +MX: Nat, +sa: Nat, +ci: Nat, +cs: Nat, +hnh: {SW.value(nh) == C.shift(8n, C.shift(Nat.add(sa, ci), MX)) : Nat}, +Ep: Nat, +p: Nat, +hp: {Nat.add(Nat.add(p, p), 1075n) == Nat.add(Ep, 4096n) : Nat}, +hpe: {Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n) == p : Nat}, +EN: Nat, +hE: {Nat.add(Ep, ci) == EN : Nat}, +XX: Nat, +hEN: {Nat.add(EN, sa) == Nat.add(XX, 2171n) : Nat}, +Mq: Nat, +hMq: {C.shift(200n, Mq) == C.shift(Nat.add(200n, cs), MX) : Nat}, +Xq: Nat, +q: Nat, +hq: {Nat.add(Nat.add(q, q), cs) == XX : Nat}, +hqd: {Nat.div(Xq, 2n) == q : Nat}, +j: Nat, +hj: {Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))) == Nat.add(200n, cs) : Nat}) -> {F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), 1048n), nh) == SF.sqrt_even(Mq, Xq) : F.F64}:
  +hpv = Equal.cong(Nat, Nat, z => Nat.add(z, 1048n), Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), p, hpe)
  +pge = N.not_lt_le(p, 1132n, p_ge(p, Ep, hp, Nat.is_lt(p, 1132n), {==}))
  +hle = Equal.trans(Bool, Nat.is_le(Nat.add(1132n, 1048n), Nat.add(p, 1048n)), Nat.is_le(1132n, p), True{}, FR.le_cancel_r(1132n, p, 1048n), pge)
  +hxs = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(p, 1048n), 2180n), 2180n), Nat.add(2180n, Nat.sub(Nat.add(p, 1048n), 2180n)), Nat.add(p, 1048n), NA.add_comm(Nat.sub(Nat.add(p, 1048n), 2180n), 2180n), N.sub_add(Nat.add(p, 1048n), 2180n, hle))
  +hx = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(p, 1048n), 2180n), 2180n), Nat.add(p, 1048n), Nat.add(Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), 1048n), hxs, Equal.sym(Nat, Nat.add(Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), 1048n), Nat.add(p, 1048n), hpv))
  +r1 = QR.sqr_root_v(one, h1, nh, h62, h60, Nat.add(Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), 1048n), Nat.sub(Nat.add(p, 1048n), 2180n), hx)
  +hEs = Equal.trans(Nat, Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n), Nat.sub(Nat.add(q, 1500n), 101n), Nat.add(q, 1399n), Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(z, 1500n), 101n), Nat.div(Xq, 2n), q, hqd), FR.sub_add_a(q, 1500n, 101n, {==}))
  +g = QX.sqexp(q, p, j, Nat.sub(Nat.add(p, 1048n), 2180n), XX, EN, Ep, sa, ci, cs, hq, hp, hE, hEN, hj, hxs)
  +hEx = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n), 1n+j), Nat.add(Nat.add(q, 1399n), 1n+j), Nat.sub(Nat.add(p, 1048n), 2180n), Equal.cong(Nat, Nat, z => Nat.add(z, 1n+j), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n), Nat.add(q, 1399n), hEs), g)
  +r2 = QS.sq_spec(one, h1, C.shift(64n, SW.value(nh)), j, QV.s62(one, h1, nh, h62, h60), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n), Nat.sub(Nat.add(p, 1048n), 2180n), hEx)
  +e1 = Equal.cong(Nat, Nat, z => C.shift(j, C.shift(j, C.shift(64n, z))), SW.value(nh), C.shift(8n, C.shift(Nat.add(sa, ci), MX)), hnh)
  +e2 = shift_nest(j, Nat.add(sa, ci), MX)
  +e3 = Equal.cong(Nat, Nat, z => C.shift(z, MX), Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), Nat.add(200n, cs), hj)
  +eN = Equal.trans(Nat, C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))), C.shift(j, C.shift(j, C.shift(64n, C.shift(8n, C.shift(Nat.add(sa, ci), MX))))), C.shift(Nat.add(200n, cs), MX), e1, Equal.trans(Nat, C.shift(j, C.shift(j, C.shift(64n, C.shift(8n, C.shift(Nat.add(sa, ci), MX))))), C.shift(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), MX), C.shift(Nat.add(200n, cs), MX), e2, e3))
  +eNs = Equal.trans(Nat, C.shift(200n, Mq), C.shift(Nat.add(200n, cs), MX), C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))), hMq, Equal.sym(Nat, C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))), C.shift(Nat.add(200n, cs), MX), eN))
  +r3 = Equal.cong(Nat, F.F64, z => SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(z)), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(z), 2n), z)))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), C.shift(200n, Mq), C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))), eNs)
  Equal.trans(F.F64, F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), 1048n), nh), SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), Nat.sub(Nat.add(p, 1048n), 2180n)), SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(200n, Mq))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(200n, Mq)), 2n), C.shift(200n, Mq))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), r1, Equal.trans(F.F64, SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), Nat.sub(Nat.add(p, 1048n), 2180n)), SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh))))), 2n), C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(200n, Mq))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(200n, Mq)), 2n), C.shift(200n, Mq))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), Equal.sym(F.F64, SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh))))), 2n), C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), Nat.sub(Nat.add(p, 1048n), 2180n)), r2), Equal.sym(F.F64, SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(200n, Mq))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(200n, Mq)), 2n), C.shift(200n, Mq))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh))))), 2n), C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), r3)))