proofs/math/typed/f64sqr.bend

bend-collections-laws-math@1.0.0.0 · 391 lines · 54 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
3import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natlight.bend as NL
4import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
5import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
6import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
7import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
8import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
9import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
10import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
11import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
12import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
13import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
14import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
15import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
16import bend-collections-laws-math@1.0.0.0/proofs/math/natural/sqrtn.bend as SQ2
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
20import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
21import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
22import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64S
23import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div.bend as W64D
24import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64est.bend as W64E
25import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dm.bend as DM
26import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
27import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
28import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64m128.bend as M128
29import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqa.bend as AQ
30import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqw.bend as QW
31import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqk.bend as SK
32import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqv.bend as QV
33
34# The F64 square root by one step of Zimmermann's SqrtRem (Karatsuba square
35# root; Bertot, Magaud and Zimmermann, "A proof of GMP square root", 2002)
36# with the exact remainder: for s = isqrt(nh), r = nh - s^2 and
37# q 2 s + u = r 2^32 (q < 2^32, u <= 2 s), S0 = s 2^32 + q satisfies
38# N + q^2 == S0^2 + u 2^32 for N = nh 2^64, so S0 - 2 <= isqrt(N) <= S0 and
39# the sign of u 2^32 - q^2 (then of the next remainders) picks the root and
40# its sticky bit.
41
42def v(+x: U32) -> Nat:
43  U32.to_nat(x)
44
45# x + b == y + a gives (a == b) == (x == y)
46def eqsh(+x: Nat, +b: Nat, +y: Nat, +a: Nat, +h: {Nat.add(x, b) == Nat.add(y, a) : Nat}) -> {Nat.is_eq(a, b) == Nat.is_eq(x, y) : Bool}:
47  +e1 = Equal.sym(Cmp, Nat.cmp(Nat.add(y, a), Nat.add(y, b)), Nat.cmp(a, b), NC.cmp_add(y, a, b))
48  +e2 = Equal.cong(Nat, Cmp, z => Nat.cmp(z, Nat.add(y, b)), Nat.add(y, a), Nat.add(x, b), Equal.sym(Nat, Nat.add(x, b), Nat.add(y, a), h))
49  +e3 = NC.cmp_addr(x, y, b)
50  Equal.cong(Cmp, Bool, z => Cmp.is_eq(z), Nat.cmp(a, b), Nat.cmp(x, y), Equal.trans(Cmp, Nat.cmp(a, b), Nat.cmp(Nat.add(y, a), Nat.add(y, b)), Nat.cmp(x, y), e1, Equal.trans(Cmp, Nat.cmp(Nat.add(y, a), Nat.add(y, b)), Nat.cmp(Nat.add(x, b), Nat.add(y, b)), Nat.cmp(x, y), e2, e3)))
51
52# ((a + b) + d) + c == (a + (b + c)) + d
53def rearr(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {Nat.add(Nat.add(Nat.add(a, b), d), c) == Nat.add(Nat.add(a, Nat.add(b, c)), d) : Nat}:
54  +e1 = NA.add_assoc(Nat.add(a, b), d, c)
55  +e2 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(a, b), z), Nat.add(d, c), Nat.add(c, d), NA.add_comm(d, c))
56  +e3 = Equal.sym(Nat, Nat.add(Nat.add(Nat.add(a, b), c), d), Nat.add(Nat.add(a, b), Nat.add(c, d)), NA.add_assoc(Nat.add(a, b), c, d))
57  +e4 = Equal.cong(Nat, Nat, z => Nat.add(z, d), Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c)), NA.add_assoc(a, b, c))
58  Equal.trans(Nat, Nat.add(Nat.add(Nat.add(a, b), d), c), Nat.add(Nat.add(a, b), Nat.add(d, c)), Nat.add(Nat.add(a, Nat.add(b, c)), d), e1, Equal.trans(Nat, Nat.add(Nat.add(a, b), Nat.add(d, c)), Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(Nat.add(a, Nat.add(b, c)), d), e2, Equal.trans(Nat, Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(Nat.add(Nat.add(a, b), c), d), Nat.add(Nat.add(a, Nat.add(b, c)), d), e3, e4)))
59
60
61# N + q^2 == S0^2 + u 2^32
62def ident(+s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}) -> {Nat.add(C.shift(32n, C.shift(32n, n)), Nat.mul(Q, Q)) == Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)) : Nat}:
63  +e0 = Equal.cong(Nat, Nat, z => Nat.mul(z, z), Nat.add(Q, C.shift(32n, s)), Nat.add(C.shift(32n, s), Q), NA.add_comm(Q, C.shift(32n, s)))
64  +e1 = SK.sqa(C.shift(32n, s), Q)
65  +e2 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), z), Nat.mul(Q, Q)), Nat.add(Nat.mul(C.shift(32n, s), Q), Nat.mul(C.shift(32n, s), Q)), C.shift(32n, Nat.mul(Q, D)), SK.uw2(s, Q, D, hD))
66  +eS = Equal.trans(Nat, Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(C.shift(32n, s), Q), Nat.add(C.shift(32n, s), Q)), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), e0, Equal.trans(Nat, Nat.mul(Nat.add(C.shift(32n, s), Q), Nat.add(C.shift(32n, s), Q)), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(Nat.mul(C.shift(32n, s), Q), Nat.mul(C.shift(32n, s), Q))), Nat.mul(Q, Q)), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), e1, e2))
67  +f1 = Equal.sym(Nat, Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, C.shift(32n, rr))), C.shift(32n, C.shift(32n, n)), SK.usq(s, rr, n, hn))
68  +f2 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, z)), C.shift(32n, rr), Nat.add(Nat.mul(Q, D), U), Equal.sym(Nat, Nat.add(Nat.mul(Q, D), U), C.shift(32n, rr), hc))
69  +f3 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), z), C.shift(32n, Nat.add(Nat.mul(Q, D), U)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U)), WW.shift_add(32n, Nat.mul(Q, D), U))
70  +eN = Equal.trans(Nat, C.shift(32n, C.shift(32n, n)), Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, C.shift(32n, rr))), Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), f1, Equal.trans(Nat, Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, C.shift(32n, rr))), Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.add(Nat.mul(Q, D), U))), Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), f2, f3))
71  +g1 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(Q, Q)), C.shift(32n, C.shift(32n, n)), Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), eN)
72  +g2 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, U)), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), eS)
73  Equal.trans(Nat, Nat.add(C.shift(32n, C.shift(32n, n)), Nat.mul(Q, Q)), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), Nat.mul(Q, Q)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), g1, Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), Nat.mul(Q, Q)), Nat.add(Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), C.shift(32n, U)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), C.shift(32n, U)), Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), Nat.add(C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U))), Nat.mul(Q, Q)), rearr(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D)), C.shift(32n, U), Nat.mul(Q, Q))), Equal.sym(Nat, Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Nat.add(Nat.add(Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.mul(Q, D))), Nat.mul(Q, Q)), C.shift(32n, U)), g2)))
74
75
76def nn(+n: Nat) -> {C.shift(64n, n) == C.shift(32n, C.shift(32n, n)) : Nat}:
77  WW.shift_comp(32n, 32n, n)
78
79# N + q^2 == S0^2 + u 2^32, with N = nh 2^64
80def identN(+s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}) -> {Nat.add(C.shift(64n, n), Nat.mul(Q, Q)) == Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)) : Nat}:
81  Equal.trans(Nat, Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Nat.add(C.shift(32n, C.shift(32n, n)), Nat.mul(Q, Q)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(Q, Q)), C.shift(64n, n), C.shift(32n, C.shift(32n, n)), nn(n)), ident(s, rr, n, Q, U, D, hn, hD, hc))
82
83# N < (S0 + 1)^2, so isqrt(N) <= S0
84def lo_bound(+s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}, +hU: {Nat.is_le(U, D) == True{} : Bool}) -> {Nat.is_lt(C.shift(64n, n), Nat.mul(1n+Nat.add(Q, C.shift(32n, s)), 1n+Nat.add(Q, C.shift(32n, s)))) == True{} : Bool}:
85  +a1 = N.le_add_right(C.shift(64n, n), Nat.mul(Q, Q))
86  +a2 = L.subst(Nat, z => {Nat.is_le(C.shift(64n, n), z) == True{} : Bool}, Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), identN(s, rr, n, Q, U, D, hn, hD, hc), a1)
87  +hPs = L.subst(Nat, z => {Nat.is_le(C.shift(32n, s), z) == True{} : Bool}, Nat.add(C.shift(32n, s), Q), Nat.add(Q, C.shift(32n, s)), NA.add_comm(C.shift(32n, s), Q), N.le_add_right(C.shift(32n, s), Q))
88  +a3 = N.le_trans(C.shift(32n, U), C.shift(32n, D), Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), WW.shift_mono(32n, U, D, hU), L.subst(Nat, z => {Nat.is_le(C.shift(32n, z), Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))) == True{} : Bool}, Nat.add(s, s), D, hD, L.subst(Nat, z => {Nat.is_le(z, Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))) == True{} : Bool}, Nat.add(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, Nat.add(s, s)), Equal.sym(Nat, C.shift(32n, Nat.add(s, s)), Nat.add(C.shift(32n, s), C.shift(32n, s)), WW.shift_add(32n, s, s)), SQ2.le_add2(C.shift(32n, s), Nat.add(Q, C.shift(32n, s)), C.shift(32n, s), Nat.add(Q, C.shift(32n, s)), hPs, hPs))))
89  +a4 = N.le_trans(C.shift(64n, n), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), a2, N.le_add_left(C.shift(32n, U), Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), a3))
90  +a5 = L.subst(Nat, z => {Nat.is_le(C.shift(64n, n), z) == True{} : Bool}, Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), Nat.add(Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), NA.add_comm(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), a4)
91  L.subst(Nat, z => {Nat.is_lt(C.shift(64n, n), z) == True{} : Bool}, 1n+Nat.add(Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), Nat.mul(1n+Nat.add(Q, C.shift(32n, s)), 1n+Nat.add(Q, C.shift(32n, s))), Equal.sym(Nat, Nat.mul(1n+Nat.add(Q, C.shift(32n, s)), 1n+Nat.add(Q, C.shift(32n, s))), 1n+Nat.add(Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), SQ2.succ_mul_succ(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), N.le_lt_trans(C.shift(64n, n), Nat.add(Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), 1n+Nat.add(Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), a5, N.lt_succ(Nat.add(Nat.add(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))))))
92
93
94# S0 <= isqrt(N) + 2, for q < 2^32 and isqrt(N) >= 2^62
95def hi_bound(+one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}, +hQ: {Nat.is_lt(Q, C.shift(32n, one)) == True{} : Bool}, +hT: {Nat.is_le(C.shift(62n, one), M.isqrt(C.shift(64n, n))) == True{} : Bool}) -> {Nat.is_le(Nat.add(Q, C.shift(32n, s)), Nat.add(M.isqrt(C.shift(64n, n)), 2n)) == True{} : Bool}:
96  +e64 = Equal.trans(Nat, Nat.mul(C.shift(32n, one), C.shift(32n, one)), C.shift(32n, C.shift(32n, Nat.mul(one, one))), C.shift(2n, C.shift(62n, one)), AQ.sh_sq(32n, one), Equal.trans(Nat, C.shift(32n, C.shift(32n, Nat.mul(one, one))), C.shift(32n, C.shift(32n, one)), C.shift(2n, C.shift(62n, one)), Equal.cong(Nat, Nat, z => C.shift(32n, C.shift(32n, z)), Nat.mul(one, one), one, L.subst(Nat, o => {Nat.mul(o, o) == o : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==})), Equal.trans(Nat, C.shift(32n, C.shift(32n, one)), C.shift(64n, one), C.shift(2n, C.shift(62n, one)), Equal.sym(Nat, C.shift(64n, one), C.shift(32n, C.shift(32n, one)), WW.shift_comp(32n, 32n, one)), WW.shift_comp(2n, 62n, one))))
97  +hq2 = N.le_trans(Nat.mul(Q, Q), Nat.mul(C.shift(32n, one), C.shift(32n, one)), Nat.add(Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))), Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n)))), AQ.sqmono(Q, C.shift(32n, one), N.lt_le(Q, C.shift(32n, one), hQ)), L.subst(Nat, z => {Nat.is_le(Nat.mul(C.shift(32n, one), C.shift(32n, one)), z) == True{} : Bool}, C.shift(2n, M.isqrt(C.shift(64n, n))), Nat.add(Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))), Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n)))), SK.four(M.isqrt(C.shift(64n, n))), L.subst(Nat, z => {Nat.is_le(z, C.shift(2n, M.isqrt(C.shift(64n, n)))) == True{} : Bool}, C.shift(2n, C.shift(62n, one)), Nat.mul(C.shift(32n, one), C.shift(32n, one)), Equal.sym(Nat, Nat.mul(C.shift(32n, one), C.shift(32n, one)), C.shift(2n, C.shift(62n, one)), e64), WW.shift_mono(2n, C.shift(62n, one), M.isqrt(C.shift(64n, n)), hT))))
98  +a1 = N.le_add_right(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U))
99  +a2 = L.subst(Nat, z => {Nat.is_le(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), z) == True{} : Bool}, Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Equal.sym(Nat, Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), identN(s, rr, n, Q, U, D, hn, hD, hc)), a1)
100  +a3 = N.le_lt_trans(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Nat.add(Nat.mul(1n+M.isqrt(C.shift(64n, n)), 1n+M.isqrt(C.shift(64n, n))), Nat.add(Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))), Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))))), a2, N.lt_le_trans(Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Nat.add(Nat.mul(1n+M.isqrt(C.shift(64n, n)), 1n+M.isqrt(C.shift(64n, n))), Nat.mul(Q, Q)), Nat.add(Nat.mul(1n+M.isqrt(C.shift(64n, n)), 1n+M.isqrt(C.shift(64n, n))), Nat.add(Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))), Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))))), N.lt_add_r2(C.shift(64n, n), Nat.mul(1n+M.isqrt(C.shift(64n, n)), 1n+M.isqrt(C.shift(64n, n))), Nat.mul(Q, Q), AQ.ilt(C.shift(64n, n))), N.le_add_left(Nat.mul(Q, Q), Nat.add(Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n))), Nat.add(M.isqrt(C.shift(64n, n)), M.isqrt(C.shift(64n, n)))), Nat.mul(1n+M.isqrt(C.shift(64n, n)), 1n+M.isqrt(C.shift(64n, n))), hq2)))
101  SK.k_hi_c(C.shift(64n, n), M.isqrt(C.shift(64n, n)), Nat.add(Q, C.shift(32n, s)), a3, Nat.is_le(Nat.add(Q, C.shift(32n, s)), Nat.add(M.isqrt(C.shift(64n, n)), 2n)), {==})
102
103
104def two62(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(2n, C.shift(62n, one)) == True{} : Bool}:
105  +h = L.subst(Nat, o => {Nat.is_le(o, C.shift(61n, one)) == True{} : Bool}, one, 1n, h1, WW.shift_ge(61n, one))
106  L.subst(Nat, z => {Nat.is_le(2n, z) == True{} : Bool}, Nat.add(C.shift(61n, one), C.shift(61n, one)), C.shift(62n, one), Equal.sym(Nat, C.shift(62n, one), Nat.add(C.shift(61n, one), C.shift(61n, one)), NA.double_self(C.shift(61n, one))), SQ2.le_add2(1n, C.shift(61n, one), 1n, C.shift(61n, one), h, h))
107
108# branch A: q^2 <= u 2^32 gives the root S0, exact iff q^2 == u 2^32
109def brA_T(+s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}, +hU: {Nat.is_le(U, D) == True{} : Bool}, +hAB: {Nat.is_le(Nat.mul(Q, Q), C.shift(32n, U)) == True{} : Bool}) -> {M.isqrt(C.shift(64n, n)) == Nat.add(Q, C.shift(32n, s)) : Nat}:
110  +a1 = N.le_add_left(Nat.mul(Q, Q), C.shift(32n, U), C.shift(64n, n), hAB)
111  +a2 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(C.shift(64n, n), C.shift(32n, U))) == True{} : Bool}, Nat.add(C.shift(64n, n), Nat.mul(Q, Q)), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), identN(s, rr, n, Q, U, D, hn, hD, hc), a1)
112  +a3 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(C.shift(64n, n), C.shift(32n, U))) == True{} : Bool}, Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Nat.add(C.shift(32n, U), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), NA.add_comm(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), a2)
113  +a4 = L.subst(Nat, z => {Nat.is_le(Nat.add(C.shift(32n, U), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), z) == True{} : Bool}, Nat.add(C.shift(64n, n), C.shift(32n, U)), Nat.add(C.shift(32n, U), C.shift(64n, n)), NA.add_comm(C.shift(64n, n), C.shift(32n, U)), a3)
114  +hle = Equal.trans(Bool, Nat.is_le(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(64n, n)), Nat.is_le(Nat.add(C.shift(32n, U), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), Nat.add(C.shift(32n, U), C.shift(64n, n))), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(C.shift(32n, U), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), Nat.add(C.shift(32n, U), C.shift(64n, n))), Nat.is_le(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(64n, n)), NR.le_add_cancel(C.shift(32n, U), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(64n, n))), a4)
115  AQ.isqrt_char(C.shift(64n, n), Nat.add(Q, C.shift(32n, s)), hle, lo_bound(s, rr, n, Q, U, D, hn, hD, hc, hU))
116
117def brA_eq(+s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}) -> {Nat.is_eq(C.shift(32n, U), Nat.mul(Q, Q)) == Nat.is_eq(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(64n, n)) : Bool}:
118  Equal.trans(Bool, Nat.is_eq(C.shift(32n, U), Nat.mul(Q, Q)), Nat.is_eq(C.shift(64n, n), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), Nat.is_eq(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(64n, n)), eqsh(C.shift(64n, n), Nat.mul(Q, Q), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U), identN(s, rr, n, Q, U, D, hn, hD, hc)), QW.eq_comm(C.shift(64n, n), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))))
119
120# branch B: q^2 > u 2^32, D = q^2 - u 2^32 > 0 and N + D == S0^2
121def brB_nd(+s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}, +hBA: {Nat.is_lt(C.shift(32n, U), Nat.mul(Q, Q)) == True{} : Bool}) -> {Nat.add(C.shift(64n, n), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))) == Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))) : Nat}:
122  +eD = N.sub_add(Nat.mul(Q, Q), C.shift(32n, U), N.lt_le(C.shift(32n, U), Nat.mul(Q, Q), hBA))
123  +e1 = L.subst(Nat, z => {Nat.add(C.shift(64n, n), z) == Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)) : Nat}, Nat.mul(Q, Q), Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))), Equal.sym(Nat, Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))), Nat.mul(Q, Q), eD), identN(s, rr, n, Q, U, D, hn, hD, hc))
124  +e2 = Equal.trans(Nat, Nat.add(C.shift(32n, U), Nat.add(C.shift(64n, n), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U)))), Nat.add(C.shift(64n, n), Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U)))), Nat.add(C.shift(32n, U), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), NA.add_swap(C.shift(32n, U), C.shift(64n, n), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))), Equal.trans(Nat, Nat.add(C.shift(64n, n), Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U)))), Nat.add(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U)), Nat.add(C.shift(32n, U), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s)))), e1, NA.add_comm(Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), C.shift(32n, U))))
125  NR.add_cancel(C.shift(32n, U), Nat.add(C.shift(64n, n), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))), Nat.mul(Nat.add(Q, C.shift(32n, s)), Nat.add(Q, C.shift(32n, s))), e2)
126
127def brB_pos(+s: Nat, +rr: Nat, +n: Nat, +Q: Nat, +U: Nat, +D: Nat, +hn: {Nat.add(Nat.mul(s, s), rr) == n : Nat}, +hD: {Nat.add(s, s) == D : Nat}, +hc: {Nat.add(Nat.mul(Q, D), U) == C.shift(32n, rr) : Nat}, +hBA: {Nat.is_lt(C.shift(32n, U), Nat.mul(Q, Q)) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))) == True{} : Bool}:
128  +eD = N.sub_add(Nat.mul(Q, Q), C.shift(32n, U), N.lt_le(C.shift(32n, U), Nat.mul(Q, Q), hBA))
129  +h = L.subst(Nat, z => {Nat.is_lt(C.shift(32n, U), z) == True{} : Bool}, Nat.mul(Q, Q), Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))), Equal.sym(Nat, Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))), Nat.mul(Q, Q), eD), hBA)
130  +h2 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U)))) == True{} : Bool}, C.shift(32n, U), Nat.add(C.shift(32n, U), 0n), Equal.sym(Nat, Nat.add(C.shift(32n, U), 0n), C.shift(32n, U), N.add_zero(C.shift(32n, U))), h)
131  Equal.trans(Bool, Nat.is_lt(0n, Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))), Nat.is_lt(Nat.add(C.shift(32n, U), 0n), Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U)))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(C.shift(32n, U), 0n), Nat.add(C.shift(32n, U), Nat.sub(Nat.mul(Q, Q), C.shift(32n, U)))), Nat.is_lt(0n, Nat.sub(Nat.mul(Q, Q), C.shift(32n, U))), WW.lt_cancel_l(C.shift(32n, U), 0n, Nat.sub(Nat.mul(Q, Q), C.shift(32n, U)))), h2)
132
133
134# with S0 = 2 + S2 and S1 = 1 + S2: c = 2 S0 - 1 == 1 + 2 S1, S0^2 == c + S1^2, S1^2 == (c - 2) + S2^2
135def c_eq(+S2: Nat) -> {Nat.sub(Nat.add(2n+S2, 2n+S2), 1n) == 1n+Nat.add(1n+S2, 1n+S2) : Nat}:
136  Equal.cong(Nat, Nat, z => 1n+z, Nat.add(S2, 2n+S2), 1n+Nat.add(S2, 1n+S2), N.add_succ(S2, 1n+S2))
137
138def c2_eq(+S2: Nat) -> {Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n) == 1n+Nat.add(S2, S2) : Nat}:
139  +e1 = Equal.trans(Nat, Nat.add(S2, 2n+S2), 1n+Nat.add(S2, 1n+S2), 1n+1n+Nat.add(S2, S2), N.add_succ(S2, 1n+S2), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(S2, 1n+S2), 1n+Nat.add(S2, S2), N.add_succ(S2, S2)))
140  Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), Nat.add(S2, 2n+S2), 1n+1n+Nat.add(S2, S2), e1)
141
142def sq0_eq(+S2: Nat) -> {Nat.mul(2n+S2, 2n+S2) == Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)) : Nat}:
143  Equal.trans(Nat, Nat.mul(2n+S2, 2n+S2), 1n+Nat.add(Nat.add(1n+S2, 1n+S2), Nat.mul(1n+S2, 1n+S2)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), SQ2.succ_mul_succ(1n+S2, 1n+S2), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(1n+S2, 1n+S2)), 1n+Nat.add(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Equal.sym(Nat, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 1n+Nat.add(1n+S2, 1n+S2), c_eq(S2))))
144
145def sq1_eq(+S2: Nat) -> {Nat.mul(1n+S2, 1n+S2) == Nat.add(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.mul(S2, S2)) : Nat}:
146  Equal.trans(Nat, Nat.mul(1n+S2, 1n+S2), 1n+Nat.add(Nat.add(S2, S2), Nat.mul(S2, S2)), Nat.add(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.mul(S2, S2)), SQ2.succ_mul_succ(S2, S2), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(S2, S2)), 1n+Nat.add(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Equal.sym(Nat, Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), 1n+Nat.add(S2, S2), c2_eq(S2))))
147
148
149# S1^2 + c == N + D
150def b_s1(+n: Nat, +S2: Nat, +Dx: Nat, +hnd: {Nat.add(C.shift(64n, n), Dx) == Nat.mul(2n+S2, 2n+S2) : Nat}) -> {Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)) == Nat.add(C.shift(64n, n), Dx) : Nat}:
151  Equal.trans(Nat, Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Nat.add(C.shift(64n, n), Dx), NA.add_comm(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Nat.mul(2n+S2, 2n+S2), Nat.add(C.shift(64n, n), Dx), Equal.sym(Nat, Nat.mul(2n+S2, 2n+S2), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), sq0_eq(S2)), Equal.sym(Nat, Nat.add(C.shift(64n, n), Dx), Nat.mul(2n+S2, 2n+S2), hnd)))
152
153# D <= c: the root is S1, exact iff D == c
154def b1_T(+n: Nat, +S2: Nat, +Dx: Nat, +hnd: {Nat.add(C.shift(64n, n), Dx) == Nat.mul(2n+S2, 2n+S2) : Nat}, +hpos: {Nat.is_lt(0n, Dx) == True{} : Bool}, +hs: {Nat.is_le(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)) == True{} : Bool}) -> {M.isqrt(C.shift(64n, n)) == 1n+S2 : Nat}:
155  +e1 = b_s1(n, S2, Dx, hnd)
156  +a1 = N.le_add_left(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), C.shift(64n, n), hs)
157  +a2 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))) == True{} : Bool}, Nat.add(C.shift(64n, n), Dx), Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Equal.sym(Nat, Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(C.shift(64n, n), Dx), e1), a1)
158  +a3 = L.subst(Nat, z => {Nat.is_le(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), z) == True{} : Bool}, Nat.add(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), C.shift(64n, n)), NA.add_comm(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), L.subst(Nat, z => {Nat.is_le(z, Nat.add(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))) == True{} : Bool}, Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), NA.add_comm(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), a2))
159  +hle = Equal.trans(Bool, Nat.is_le(Nat.mul(1n+S2, 1n+S2), C.shift(64n, n)), Nat.is_le(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), C.shift(64n, n))), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), C.shift(64n, n))), Nat.is_le(Nat.mul(1n+S2, 1n+S2), C.shift(64n, n)), NR.le_add_cancel(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2), C.shift(64n, n))), a3)
160  +hlt = L.subst(Nat, z => {Nat.is_lt(C.shift(64n, n), z) == True{} : Bool}, Nat.add(C.shift(64n, n), Dx), Nat.mul(2n+S2, 2n+S2), hnd, DM.lt_add_pos(C.shift(64n, n), Dx, hpos))
161  AQ.isqrt_char(C.shift(64n, n), 1n+S2, hle, hlt)
162
163def b1_eq(+n: Nat, +S2: Nat, +Dx: Nat, +hnd: {Nat.add(C.shift(64n, n), Dx) == Nat.mul(2n+S2, 2n+S2) : Nat}) -> {Nat.is_eq(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx) == Nat.is_eq(Nat.mul(1n+S2, 1n+S2), C.shift(64n, n)) : Bool}:
164  Equal.trans(Bool, Nat.is_eq(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx), Nat.is_eq(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.is_eq(Nat.mul(1n+S2, 1n+S2), C.shift(64n, n)), QW.eq_comm(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx), eqsh(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), C.shift(64n, n), Dx, b_s1(n, S2, Dx, hnd)))
165
166# S2^2 + (c - 2) == N + (D - c) for c < D
167def b_s2(+n: Nat, +S2: Nat, +Dx: Nat, +hnd: {Nat.add(C.shift(64n, n), Dx) == Nat.mul(2n+S2, 2n+S2) : Nat}, +hb: {Nat.is_lt(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx) == True{} : Bool}) -> {Nat.add(Nat.mul(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n)) == Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))) : Nat}:
168  +eD = N.sub_add(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), N.lt_le(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx, hb))
169  +e1 = L.subst(Nat, z => {Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)) == Nat.add(C.shift(64n, n), z) : Nat}, Dx, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Dx, eD), b_s1(n, S2, Dx, hnd))
170  +e2 = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), NA.add_comm(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Equal.trans(Nat, Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(C.shift(64n, n), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), e1, NA.add_swap(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))))
171  +e3 = NR.add_cancel(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), e2)
172  Equal.trans(Nat, Nat.add(Nat.mul(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n)), Nat.mul(1n+S2, 1n+S2), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Equal.trans(Nat, Nat.add(Nat.mul(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n)), Nat.add(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.mul(S2, S2)), Nat.mul(1n+S2, 1n+S2), NA.add_comm(Nat.mul(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n)), Equal.sym(Nat, Nat.mul(1n+S2, 1n+S2), Nat.add(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.mul(S2, S2)), sq1_eq(S2))), e3)
173
174# c < D: the root is S2 (it is at least S0 - 2), exact iff D - c == c - 2
175def b2_T(+n: Nat, +S2: Nat, +Dx: Nat, +hnd: {Nat.add(C.shift(64n, n), Dx) == Nat.mul(2n+S2, 2n+S2) : Nat}, +hb: {Nat.is_lt(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx) == True{} : Bool}, +hge: {Nat.is_le(2n+S2, Nat.add(M.isqrt(C.shift(64n, n)), 2n)) == True{} : Bool}) -> {M.isqrt(C.shift(64n, n)) == S2 : Nat}:
176  +eD = N.sub_add(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), N.lt_le(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx, hb))
177  +e1 = L.subst(Nat, z => {Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)) == Nat.add(C.shift(64n, n), z) : Nat}, Dx, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Dx, eD), b_s1(n, S2, Dx, hnd))
178  +e2 = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), NA.add_comm(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2)), Equal.trans(Nat, Nat.add(Nat.mul(1n+S2, 1n+S2), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.add(C.shift(64n, n), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), e1, NA.add_swap(C.shift(64n, n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))))
179  +e3 = NR.add_cancel(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.mul(1n+S2, 1n+S2), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), e2)
180  +hp = Equal.trans(Bool, Nat.is_lt(0n, Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Nat.is_lt(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), Nat.is_lt(0n, Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), WW.lt_cancel_l(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n, Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)))), L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n), z) == True{} : Bool}, Dx, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Dx, eD), L.subst(Nat, z => {Nat.is_lt(z, Dx) == True{} : Bool}, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 0n), Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), N.add_zero(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), hb)))
181  +hlt = L.subst(Nat, z => {Nat.is_lt(C.shift(64n, n), z) == True{} : Bool}, Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Nat.mul(1n+S2, 1n+S2), Equal.sym(Nat, Nat.mul(1n+S2, 1n+S2), Nat.add(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), e3), DM.lt_add_pos(C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), hp))
182  +hup = N.lt_succ_le(M.isqrt(C.shift(64n, n)), S2, AQ.isqrt_lt(C.shift(64n, n), 1n+S2, hlt))
183  +hdn = L.subst(Nat, z => {Nat.is_le(2n+S2, z) == True{} : Bool}, Nat.add(M.isqrt(C.shift(64n, n)), 2n), 2n+M.isqrt(C.shift(64n, n)), NA.add_comm(M.isqrt(C.shift(64n, n)), 2n), hge)
184  N.le_antisym(M.isqrt(C.shift(64n, n)), S2, hup, hdn)
185
186def b2_eq(+n: Nat, +S2: Nat, +Dx: Nat, +hnd: {Nat.add(C.shift(64n, n), Dx) == Nat.mul(2n+S2, 2n+S2) : Nat}, +hb: {Nat.is_lt(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), Dx) == True{} : Bool}) -> {Nat.is_eq(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))) == Nat.is_eq(Nat.mul(S2, S2), C.shift(64n, n)) : Bool}:
187  Equal.trans(Bool, Nat.is_eq(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), Nat.is_eq(Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n)), Nat.is_eq(Nat.mul(S2, S2), C.shift(64n, n)), QW.eq_comm(Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))), eqsh(Nat.mul(S2, S2), Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n), C.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n)), b_s2(n, S2, Dx, hnd, hb)))
188
189
190# roundPackToF64 of the root with its sticky bit is the spec's round
191def fin_v(+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}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +t: WU.U64, +st: Bool, +ht: {SW.value(t) == M.isqrt(C.shift(64n, SW.value(nh))) : Nat}, +hst: {st == 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)))) : Bool}) -> {F.sq_fin(e, t, st) == 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)))))), x) : F.F64}:
192  +ev = Equal.trans(Nat, SW.value(X.or_bit(t, st)), SW.jam(SW.value(t), SF.b2n(st)), 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)))))), FL.orv(t, st), Equal.trans(Nat, SW.jam(SW.value(t), SF.b2n(st)), SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(st)), 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)))))), Equal.cong(Nat, Nat, z => SW.jam(z, SF.b2n(st)), SW.value(t), M.isqrt(C.shift(64n, SW.value(nh))), ht), Equal.cong(Bool, Nat, z => SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(z)), st, 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)))), hst)))
193  +s63 = Equal.trans(Bool, C.fits(63n, M.isqrt(C.shift(64n, SW.value(nh)))), Nat.is_lt(M.isqrt(C.shift(64n, SW.value(nh))), C.shift(63n, one)), True{}, Equal.sym(Bool, Nat.is_lt(M.isqrt(C.shift(64n, SW.value(nh))), C.shift(63n, one)), C.fits(63n, M.isqrt(C.shift(64n, SW.value(nh)))), FR.lt_fit(63n, one, h1, M.isqrt(C.shift(64n, SW.value(nh))))), N.lt_le_trans(M.isqrt(C.shift(64n, SW.value(nh))), SW.value(WU.U64{0, U32.add(X.lo(X.isqrt(nh)), 1)}), C.shift(63n, one), QV.s_hi(one, h1, nh, h62, h60, WU.U64{0, U32.add(X.lo(X.isqrt(nh)), 1)}, QV.r0_v(one, h1, nh, h62, h60), QV.r0_hi(one, h1, nh, h62, h60)), QV.r0_63(one, h1, nh, h62, h60, WU.U64{0, U32.add(X.lo(X.isqrt(nh)), 1)}, QV.r0_v(one, h1, nh, h62, h60), QV.r0_hi(one, h1, nh, h62, h60))))
194  +s62 = Equal.trans(Bool, C.fits(62n, M.isqrt(C.shift(64n, SW.value(nh)))), Nat.is_lt(M.isqrt(C.shift(64n, SW.value(nh))), C.shift(62n, one)), False{}, Equal.sym(Bool, Nat.is_lt(M.isqrt(C.shift(64n, SW.value(nh))), C.shift(62n, one)), C.fits(62n, M.isqrt(C.shift(64n, SW.value(nh)))), FR.lt_fit(62n, one, h1, M.isqrt(C.shift(64n, SW.value(nh))))), N.le_not_lt(M.isqrt(C.shift(64n, SW.value(nh))), C.shift(62n, one), QV.s62(one, h1, nh, h62, h60)))
195  +j63 = Equal.trans(Bool, C.fits(63n, 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))))))), C.fits(63n, M.isqrt(C.shift(64n, SW.value(nh)))), True{}, RT.jam_fits(62n, 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)))))), s63)
196  +j62 = Equal.trans(Bool, C.fits(62n, 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))))))), C.fits(62n, M.isqrt(C.shift(64n, SW.value(nh)))), False{}, RT.jam_fits(61n, 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)))))), s62)
197  +h63 = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, 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)))))), SW.value(X.or_bit(t, st)), Equal.sym(Nat, SW.value(X.or_bit(t, st)), 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)))))), ev), j63)
198  +h62b = L.subst(Nat, z => {C.fits(62n, z) == False{} : Bool}, 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)))))), SW.value(X.or_bit(t, st)), Equal.sym(Nat, SW.value(X.or_bit(t, st)), 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)))))), ev), j62)
199  +r1 = FR.round_pack(False{}, e, X.or_bit(t, st), x, hx, h62b, h63)
200  Equal.trans(F.F64, F.sq_fin(e, t, st), SF.round(False{}, SW.value(X.or_bit(t, st)), x), 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)))))), x), r1, Equal.cong(Nat, F.F64, z => SF.round(False{}, z, x), SW.value(X.or_bit(t, st)), 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)))))), ev))
201
202def sticky_eq(+a: Bool, +b: Bool, +h: {a == b : Bool}) -> {Bool.not(a) == Bool.not(b) : Bool}:
203  Equal.cong(Bool, Bool, z => Bool.not(z), a, b, h)
204
205
206def s0v(+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}, +q: U32) -> {SW.value(WU.U64{q, X.lo(X.isqrt(nh))}) == Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))) : Nat}:
207  Equal.cong(Nat, Nat, z => Nat.add(v(q), C.shift(32n, z)), v(X.lo(X.isqrt(nh))), M.isqrt(SW.value(nh)), QV.s_v(one, h1, nh, h62, h60))
208
209def bv_q(+q: U32) -> {SW.value(X.mul32(q, q)) == Nat.mul(v(q), v(q)) : Nat}:
210  W64M.mul32_value(q, q)
211
212# S0 < 2^63: q < 2^32 and s + 1 <= 2^31
213def s0_63(+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}, +q: U32, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), C.shift(63n, one)) == True{} : Bool}:
214  +l1 = N.lt_le_trans(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(C.shift(32n, one), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(C.shift(32n, one), C.shift(32n, M.isqrt(SW.value(nh)))), N.lt_add_r2(v(q), C.shift(32n, one), C.shift(32n, M.isqrt(SW.value(nh))), hQ), N.le_refl(Nat.add(C.shift(32n, one), C.shift(32n, M.isqrt(SW.value(nh))))))
215  +e1 = Equal.sym(Nat, C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), Nat.add(C.shift(32n, one), C.shift(32n, M.isqrt(SW.value(nh)))), WW.shift_add(32n, one, M.isqrt(SW.value(nh))))
216  +l0 = L.subst(Nat, o => {Nat.is_le(Nat.add(o, M.isqrt(SW.value(nh))), C.shift(31n, one)) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), N.lt_succ_le_succ(M.isqrt(SW.value(nh)), C.shift(31n, one), QV.iv31(one, h1, nh, h62, h60)))
217  +l2 = WW.shift_mono(32n, Nat.add(one, M.isqrt(SW.value(nh))), C.shift(31n, one), l0)
218  +l3 = L.subst(Nat, z => {Nat.is_le(C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), z) == True{} : Bool}, C.shift(32n, C.shift(31n, one)), C.shift(63n, one), Equal.sym(Nat, C.shift(63n, one), C.shift(32n, C.shift(31n, one)), WW.shift_comp(32n, 31n, one)), l2)
219  N.lt_le_trans(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(C.shift(32n, one), C.shift(32n, M.isqrt(SW.value(nh)))), C.shift(63n, one), l1, L.subst(Nat, z => {Nat.is_le(z, C.shift(63n, one)) == True{} : Bool}, C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), Nat.add(C.shift(32n, one), C.shift(32n, M.isqrt(SW.value(nh)))), Equal.sym(Nat, Nat.add(C.shift(32n, one), C.shift(32n, M.isqrt(SW.value(nh)))), C.shift(32n, Nat.add(one, M.isqrt(SW.value(nh)))), e1), l3))
220
221# 2 <= S0 (S0 >= isqrt(N) >= 2^62)
222def s0_2(+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}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}) -> {Nat.is_le(2n, Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))) == True{} : Bool}:
223  +hT = N.lt_succ_le(M.isqrt(C.shift(64n, SW.value(nh))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), AQ.isqrt_lt(C.shift(64n, SW.value(nh)), 1n+Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), lo_bound(M.isqrt(SW.value(nh)), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(nh), v(q), v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.hn_v(one, h1, nh, h62, h60), {==}, hc, hU)))
224  N.le_trans(2n, C.shift(62n, one), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), two62(one, h1), N.le_trans(C.shift(62n, one), M.isqrt(C.shift(64n, SW.value(nh))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), QV.s62(one, h1, nh, h62, h60), hT))
225
226
227def hS(+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}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}) -> {Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))) == 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n) : Nat}:
228  Equal.sym(Nat, 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), N.sub_add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n, s0_2(one, h1, nh, h62, h60, q, u, hc, hU, hQ)))
229
230def cw_v(+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}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}) -> {SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})) == Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n) : Nat}:
231  +l63 = s0_63(one, h1, nh, h62, h60, q, hQ)
232  +f = WW.fits_one(64n, one, h1, Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), z) == True{} : Bool}, Nat.add(C.shift(63n, one), C.shift(63n, one)), C.shift(64n, one), Equal.sym(Nat, C.shift(64n, one), Nat.add(C.shift(63n, one), C.shift(63n, one)), NA.double_self(C.shift(63n, one))), N.lt_le_trans(Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), Nat.add(C.shift(63n, one), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), Nat.add(C.shift(63n, one), C.shift(63n, one)), N.lt_add_r2(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), C.shift(63n, one), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), l63), L.subst(Nat, z => {Nat.is_le(Nat.add(C.shift(63n, one), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), z) == True{} : Bool}, Nat.add(C.shift(63n, one), C.shift(63n, one)), Nat.add(C.shift(63n, one), C.shift(63n, one)), {==}, N.le_add_left(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), C.shift(63n, one), C.shift(63n, one), N.lt_le(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), C.shift(63n, one), l63))))))
233  +fs = L.subst(Nat, z => {C.fits(64n, z) == True{} : Bool}, Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), Nat.add(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), SW.value(WU.U64{q, X.lo(X.isqrt(nh))})), Equal.trans(Nat, Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), Nat.add(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), Nat.add(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), SW.value(WU.U64{q, X.lo(X.isqrt(nh))})), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Equal.sym(Nat, SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), s0v(one, h1, nh, h62, h60, q))), Equal.cong(Nat, Nat, z => Nat.add(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), z), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Equal.sym(Nat, SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), s0v(one, h1, nh, h62, h60, q)))), f)
234  +ea = Equal.trans(Nat, SW.value(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))})), Nat.add(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), SW.value(WU.U64{q, X.lo(X.isqrt(nh))})), Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), M128.add64_exact(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}, fs), Equal.trans(Nat, Nat.add(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), SW.value(WU.U64{q, X.lo(X.isqrt(nh))})), Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), SW.value(WU.U64{q, X.lo(X.isqrt(nh))})), Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), Equal.cong(Nat, Nat, z => Nat.add(z, SW.value(WU.U64{q, X.lo(X.isqrt(nh))})), SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), s0v(one, h1, nh, h62, h60, q)), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), z), SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), s0v(one, h1, nh, h62, h60, q))))
235  +h1l = L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), SW.value(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))})), Equal.sym(Nat, SW.value(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))})), Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), ea), N.le_trans(1n, 2n, Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), {==}, N.le_trans(2n, Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), s0_2(one, h1, nh, h62, h60, q, u, hc, hU, hQ), N.le_add_right(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))))))
236  +es = Equal.trans(Nat, SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.sub(SW.value(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))})), 1n), Nat.sub(Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), 1n), WA.sub_value(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}, h1l), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), SW.value(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))})), Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), ea))
237  Equal.trans(Nat, SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.sub(Nat.add(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), 1n), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), es, Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(z, z), 1n), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), hS(one, h1, nh, h62, h60, q, u, hc, hU, hQ)))
238
239
240def le_ba(+q: U32, +u: U32) -> {X.le(X.mul32(q, q), WU.U64{0, u}) == Nat.is_le(Nat.mul(v(q), v(q)), C.shift(32n, v(u))) : Bool}:
241  Equal.trans(Bool, X.le(X.mul32(q, q), WU.U64{0, u}), Nat.is_le(SW.value(X.mul32(q, q)), SW.value(WU.U64{0, u})), Nat.is_le(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), WA.le_value(X.mul32(q, q), WU.U64{0, u}), Equal.cong(Nat, Bool, z => Nat.is_le(z, C.shift(32n, v(u))), SW.value(X.mul32(q, q)), Nat.mul(v(q), v(q)), bv_q(q)))
242
243def eq_ab(+q: U32, +u: U32) -> {X.eq(WU.U64{0, u}, X.mul32(q, q)) == Nat.is_eq(C.shift(32n, v(u)), Nat.mul(v(q), v(q))) : Bool}:
244  Equal.trans(Bool, X.eq(WU.U64{0, u}, X.mul32(q, q)), Nat.is_eq(SW.value(WU.U64{0, u}), SW.value(X.mul32(q, q))), Nat.is_eq(C.shift(32n, v(u)), Nat.mul(v(q), v(q))), WA.eq_value(WU.U64{0, u}, X.mul32(q, q)), Equal.cong(Nat, Bool, z => Nat.is_eq(C.shift(32n, v(u)), z), SW.value(X.mul32(q, q)), Nat.mul(v(q), v(q)), bv_q(q)))
245
246
247# branch A: the root S0
248def brA_w(+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}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}, +hge: {X.le(X.mul32(q, q), WU.U64{0, u}) == True{} : Bool}) -> {F.sq_rem(e, WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{0, u}, X.mul32(q, q), True{}) == 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)))))), x) : F.F64}:
249  +hAB = Equal.trans(Bool, Nat.is_le(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), X.le(X.mul32(q, q), WU.U64{0, u}), True{}, Equal.sym(Bool, X.le(X.mul32(q, q), WU.U64{0, u}), Nat.is_le(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), le_ba(q, u)), hge)
250  +eT = brA_T(M.isqrt(SW.value(nh)), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(nh), v(q), v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.hn_v(one, h1, nh, h62, h60), {==}, hc, hU, hAB)
251  +ht = Equal.trans(Nat, SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), M.isqrt(C.shift(64n, SW.value(nh))), s0v(one, h1, nh, h62, h60, q), Equal.sym(Nat, M.isqrt(C.shift(64n, SW.value(nh))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), eT))
252  +e1 = Equal.trans(Bool, X.eq(WU.U64{0, u}, X.mul32(q, q)), Nat.is_eq(C.shift(32n, v(u)), Nat.mul(v(q), v(q))), Nat.is_eq(Nat.mul(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), C.shift(64n, SW.value(nh))), eq_ab(q, u), brA_eq(M.isqrt(SW.value(nh)), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(nh), v(q), v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.hn_v(one, h1, nh, h62, h60), {==}, hc))
253  +e2 = Equal.trans(Bool, X.eq(WU.U64{0, u}, X.mul32(q, q)), Nat.is_eq(Nat.mul(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), C.shift(64n, SW.value(nh))), 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))), e1, Equal.cong(Nat, Bool, z => Nat.is_eq(Nat.mul(z, z), C.shift(64n, SW.value(nh))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), M.isqrt(C.shift(64n, SW.value(nh))), Equal.sym(Nat, M.isqrt(C.shift(64n, SW.value(nh))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), eT)))
254  fin_v(one, h1, nh, h62, h60, e, x, hx, WU.U64{q, X.lo(X.isqrt(nh))}, Bool.not(X.eq(WU.U64{0, u}, X.mul32(q, q))), ht, sticky_eq(X.eq(WU.U64{0, u}, X.mul32(q, q)), 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))), e2))
255
256
257def one_le(+x: Nat, +h: {Nat.is_le(2n, x) == True{} : Bool}) -> {Nat.is_le(1n, x) == True{} : Bool}:
258  N.le_trans(1n, 2n, x, {==}, h)
259
260def dw_value(+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}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}, +hBA: {Nat.is_lt(C.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool}) -> {SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})) == Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))) : Nat}:
261  +h = L.subst(Nat, z => {Nat.is_le(C.shift(32n, v(u)), z) == True{} : Bool}, Nat.mul(v(q), v(q)), SW.value(X.mul32(q, q)), Equal.sym(Nat, SW.value(X.mul32(q, q)), Nat.mul(v(q), v(q)), bv_q(q)), N.lt_le(C.shift(32n, v(u)), Nat.mul(v(q), v(q)), hBA))
262  Equal.trans(Nat, SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.sub(SW.value(X.mul32(q, q)), SW.value(WU.U64{0, u})), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), WA.sub_value(X.mul32(q, q), WU.U64{0, u}, h), Equal.cong(Nat, Nat, z => Nat.sub(z, C.shift(32n, v(u))), SW.value(X.mul32(q, q)), Nat.mul(v(q), v(q)), bv_q(q)))
263
264def s0w_v(+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}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}) -> {SW.value(WU.U64{q, X.lo(X.isqrt(nh))}) == 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n) : Nat}:
265  Equal.trans(Nat, SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), s0v(one, h1, nh, h62, h60, q), hS(one, h1, nh, h62, h60, q, u, hc, hU, hQ))
266
267def hnd_v(+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}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}, +hBA: {Nat.is_lt(C.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool}) -> {Nat.add(C.shift(64n, SW.value(nh)), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u)))) == Nat.mul(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)) : Nat}:
268  Equal.trans(Nat, Nat.add(C.shift(64n, SW.value(nh)), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u)))), Nat.mul(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh))))), Nat.mul(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), brB_nd(M.isqrt(SW.value(nh)), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(nh), v(q), v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.hn_v(one, h1, nh, h62, h60), {==}, hc, hBA), Equal.cong(Nat, Nat, z => Nat.mul(z, z), Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), hS(one, h1, nh, h62, h60, q, u, hc, hU, hQ)))
269
270def sm_v(+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}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}, +hBA: {Nat.is_lt(C.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool}) -> {X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})) == Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)) : Bool}:
271  Equal.trans(Bool, X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.is_le(SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), WA.le_value(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Equal.trans(Bool, Nat.is_le(SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), Equal.cong(Nat, Bool, z => Nat.is_le(z, SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), dw_value(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA)), Equal.cong(Nat, Bool, z => Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), z), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), cw_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ))))
272
273# branch B, D <= c: the root S0 - 1
274def brB1_w(+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}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}, +hBA: {Nat.is_lt(C.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool}, +hs: {X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})) == True{} : Bool}) -> {F.sq_d1(e, WU.U64{q, X.lo(X.isqrt(nh))}, X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), True{}) == 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)))))), x) : F.F64}:
275  +hs2 = Equal.trans(Bool, Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), True{}, Equal.sym(Bool, X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), sm_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA)), hs)
276  +eT = b1_T(SW.value(nh), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), hnd_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA), brB_pos(M.isqrt(SW.value(nh)), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(nh), v(q), v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.hn_v(one, h1, nh, h62, h60), {==}, hc, hBA), hs2)
277  +h1l = L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Equal.sym(Nat, SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), s0w_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ)), N.le_trans(1n, 2n, 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), {==}, N.le_add_right(2n, Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n))))
278  +ev = Equal.trans(Nat, SW.value(X.sub(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{1, 0})), Nat.sub(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), 1n), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), WA.sub_value(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{1, 0}, h1l), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), s0w_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ)))
279  +ht = Equal.trans(Nat, SW.value(X.sub(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{1, 0})), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), M.isqrt(C.shift(64n, SW.value(nh))), ev, Equal.sym(Nat, M.isqrt(C.shift(64n, SW.value(nh))), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), eT))
280  +e1 = Equal.trans(Bool, X.eq(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.is_eq(SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), SW.value(X.sub(X.mul32(q, q), WU.U64{0, u}))), Nat.is_eq(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u)))), WA.eq_value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), X.sub(X.mul32(q, q), WU.U64{0, u})), Equal.trans(Bool, Nat.is_eq(SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), SW.value(X.sub(X.mul32(q, q), WU.U64{0, u}))), Nat.is_eq(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), SW.value(X.sub(X.mul32(q, q), WU.U64{0, u}))), Nat.is_eq(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u)))), Equal.cong(Nat, Bool, z => Nat.is_eq(z, SW.value(X.sub(X.mul32(q, q), WU.U64{0, u}))), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), cw_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ)), Equal.cong(Nat, Bool, z => Nat.is_eq(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), z), SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), dw_value(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA))))
281  +e2 = Equal.trans(Bool, X.eq(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.is_eq(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u)))), Nat.is_eq(Nat.mul(1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), C.shift(64n, SW.value(nh))), e1, b1_eq(SW.value(nh), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), hnd_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA)))
282  +e3 = Equal.trans(Bool, X.eq(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.is_eq(Nat.mul(1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), C.shift(64n, SW.value(nh))), 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))), e2, Equal.cong(Nat, Bool, z => Nat.is_eq(Nat.mul(z, z), C.shift(64n, SW.value(nh))), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), M.isqrt(C.shift(64n, SW.value(nh))), Equal.sym(Nat, M.isqrt(C.shift(64n, SW.value(nh))), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), eT)))
283  fin_v(one, h1, nh, h62, h60, e, x, hx, X.sub(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{1, 0}), Bool.not(X.eq(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), X.sub(X.mul32(q, q), WU.U64{0, u}))), ht, sticky_eq(X.eq(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), X.sub(X.mul32(q, q), WU.U64{0, u})), 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))), e3))
284
285
286# branch B, D > c: the root S0 - 2
287def brB2_w(+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}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}, +hBA: {Nat.is_lt(C.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool}, +hs: {X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})) == False{} : Bool}) -> {F.sq_d2(e, WU.U64{q, X.lo(X.isqrt(nh))}, X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})) == 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)))))), x) : F.F64}:
288  +hs2 = Equal.trans(Bool, Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), False{}, Equal.sym(Bool, X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), sm_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA)), hs)
289  +hb = N.not_le_lt(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), hs2)
290  +hge = L.subst(Nat, z => {Nat.is_le(z, Nat.add(M.isqrt(C.shift(64n, SW.value(nh))), 2n)) == True{} : Bool}, Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), hS(one, h1, nh, h62, h60, q, u, hc, hU, hQ), hi_bound(one, h1, M.isqrt(SW.value(nh)), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(nh), v(q), v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.hn_v(one, h1, nh, h62, h60), {==}, hc, hQ, QV.s62(one, h1, nh, h62, h60)))
291  +eT = b2_T(SW.value(nh), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), hnd_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA), hb, hge)
292  +h2l = L.subst(Nat, z => {Nat.is_le(2n, z) == True{} : Bool}, 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), Equal.sym(Nat, SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), s0w_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ)), N.le_add_right(2n, Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)))
293  +ev = Equal.trans(Nat, SW.value(X.sub(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{2, 0})), Nat.sub(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), 2n), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), WA.sub_value(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{2, 0}, h2l), Equal.trans(Nat, Nat.sub(SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), 2n), Nat.sub(Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 0n), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), Equal.cong(Nat, Nat, z => Nat.sub(z, 2n), SW.value(WU.U64{q, X.lo(X.isqrt(nh))}), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), s0w_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ)), N.sub_zero(Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n))))
294  +ht = Equal.trans(Nat, SW.value(X.sub(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{2, 0})), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), M.isqrt(C.shift(64n, SW.value(nh))), ev, Equal.sym(Nat, M.isqrt(C.shift(64n, SW.value(nh))), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), eT))
295  +c2l0 = L.subst(Nat, z => {Nat.is_le(2n, z) == True{} : Bool}, 1n+Nat.add(1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), Equal.sym(Nat, Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), 1n+Nat.add(1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), c_eq(Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n))), N.le_add_right(2n, Nat.add(Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 1n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n))))
296  +c2l = L.subst(Nat, z => {Nat.is_le(2n, z) == True{} : Bool}, Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Equal.sym(Nat, SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), cw_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ)), c2l0)
297  +e21 = Equal.trans(Nat, SW.value(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0})), Nat.sub(SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), 2n), Nat.sub(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), 2n), WA.sub_value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0}, c2l), Equal.cong(Nat, Nat, z => Nat.sub(z, 2n), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), cw_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ)))
298  +hcd = L.subst(Nat, z => {Nat.is_le(z, SW.value(X.sub(X.mul32(q, q), WU.U64{0, u}))) == True{} : Bool}, Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Equal.sym(Nat, SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), cw_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ)), L.subst(Nat, z => {Nat.is_le(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), z) == True{} : Bool}, Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), Equal.sym(Nat, SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), dw_value(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA)), N.lt_le(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), hb)))
299  +e22 = Equal.trans(Nat, SW.value(X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.sub(SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.sub(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), WA.sub_value(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), hcd), Equal.trans(Nat, Nat.sub(SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.sub(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.sub(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), Equal.cong(Nat, Nat, z => Nat.sub(z, SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), SW.value(X.sub(X.mul32(q, q), WU.U64{0, u})), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), dw_value(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA)), Equal.cong(Nat, Nat, z => Nat.sub(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), z), SW.value(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), cw_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ))))
300  +e1 = Equal.trans(Bool, X.eq(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0}), X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.is_eq(SW.value(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0})), SW.value(X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})))), Nat.is_eq(Nat.sub(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), 2n), Nat.sub(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n))), WA.eq_value(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0}), X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Equal.trans(Bool, Nat.is_eq(SW.value(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0})), SW.value(X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})))), Nat.is_eq(Nat.sub(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), 2n), SW.value(X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})))), Nat.is_eq(Nat.sub(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), 2n), Nat.sub(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n))), Equal.cong(Nat, Bool, z => Nat.is_eq(z, SW.value(X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})))), SW.value(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0})), Nat.sub(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), 2n), e21), Equal.cong(Nat, Bool, z => Nat.is_eq(Nat.sub(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), 2n), z), SW.value(X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.sub(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n)), e22)))
301  +e2 = Equal.trans(Bool, X.eq(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0}), X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.is_eq(Nat.sub(Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n), 2n), Nat.sub(Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), 1n))), Nat.is_eq(Nat.mul(Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), C.shift(64n, SW.value(nh))), e1, b2_eq(SW.value(nh), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), Nat.sub(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), hnd_v(one, h1, nh, h62, h60, q, u, hc, hU, hQ, hBA), hb))
302  +e3 = Equal.trans(Bool, X.eq(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0}), X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), Nat.is_eq(Nat.mul(Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n)), C.shift(64n, SW.value(nh))), 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))), e2, Equal.cong(Nat, Bool, z => Nat.is_eq(Nat.mul(z, z), C.shift(64n, SW.value(nh))), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), M.isqrt(C.shift(64n, SW.value(nh))), Equal.sym(Nat, M.isqrt(C.shift(64n, SW.value(nh))), Nat.sub(Nat.add(v(q), C.shift(32n, M.isqrt(SW.value(nh)))), 2n), eT)))
303  fin_v(one, h1, nh, h62, h60, e, x, hx, X.sub(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{2, 0}), Bool.not(X.eq(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0}), X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})))), ht, sticky_eq(X.eq(X.sub(X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), WU.U64{2, 0}), X.sub(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}))), 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))), e3))
304
305def d1_v(+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}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}, +hBA: {Nat.is_lt(C.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool}, +sm: Bool, +hsm: {X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})) == sm : Bool}) -> {F.sq_d1(e, WU.U64{q, X.lo(X.isqrt(nh))}, X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0}), sm) == 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)))))), x) : F.F64}:
306  match sm:
307    case True{}:
308      brB1_w(one, h1, nh, h62, h60, e, x, hx, q, u, hc, hU, hQ, hBA, hsm)
309    case False{}:
310      brB2_w(one, h1, nh, h62, h60, e, x, hx, q, u, hc, hU, hQ, hBA, hsm)
311
312def rem_v(+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}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}, +g: Bool, +hg: {X.le(X.mul32(q, q), WU.U64{0, u}) == g : Bool}) -> {F.sq_rem(e, WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{0, u}, X.mul32(q, q), g) == 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)))))), x) : F.F64}:
313  match g:
314    case True{}:
315      brA_w(one, h1, nh, h62, h60, e, x, hx, q, u, hc, hU, hQ, hg)
316    case False{}:
317      +h0 = Equal.trans(Bool, Nat.is_le(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), X.le(X.mul32(q, q), WU.U64{0, u}), False{}, Equal.sym(Bool, X.le(X.mul32(q, q), WU.U64{0, u}), Nat.is_le(Nat.mul(v(q), v(q)), C.shift(32n, v(u))), le_ba(q, u)), hg)
318      d1_v(one, h1, nh, h62, h60, e, x, hx, q, u, hc, hU, hQ, N.not_le_lt(Nat.mul(v(q), v(q)), C.shift(32n, v(u)), h0), X.le(X.sub(X.mul32(q, q), WU.U64{0, u}), X.sub(X.add(WU.U64{q, X.lo(X.isqrt(nh))}, WU.U64{q, X.lo(X.isqrt(nh))}), WU.U64{1, 0})), {==})
319
320def qu_v(+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}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +q: U32, +u: U32, +hc: {Nat.add(Nat.mul(v(q), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(u)) == C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))) : Nat}, +hU: {Nat.is_le(v(u), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, +hQ: {Nat.is_lt(v(q), C.shift(32n, one)) == True{} : Bool}) -> {F.sq_qu(e, X.lo(X.isqrt(nh)), q, u) == 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)))))), x) : F.F64}:
321  rem_v(one, h1, nh, h62, h60, e, x, hx, q, u, hc, hU, hQ, X.le(X.mul32(q, q), WU.U64{0, u}), {==})
322
323
324def shl_le_c(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_le(C.shift(k, a), C.shift(k, b)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_le(a, b) == c : Bool}) -> {c == True{} : Bool}:
325  match c:
326    case True{}:
327      {==}
328    case False{}:
329      +h2 = WW.shift_lt(k, b, a, N.not_le_lt(a, b, hc))
330      Empty.absurd({False{} == True{} : Bool}, LW.true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(C.shift(k, b), C.shift(k, a)), False{}, Equal.sym(Bool, Nat.is_lt(C.shift(k, b), C.shift(k, a)), True{}, h2), N.le_not_lt(C.shift(k, b), C.shift(k, a), h))))
331
332# shift(k, a) <= shift(k, b) gives a <= b
333def shl_le_inv(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_le(C.shift(k, a), C.shift(k, b)) == True{} : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}:
334  shl_le_c(k, a, b, h, Nat.is_le(a, b), {==})
335
336# x / D * D + x mod D == x and x mod D < D
337def dmq(+x: Nat, +D: Nat, +hD: {Nat.is_lt(0n, D) == True{} : Bool}) -> {Nat.add(Nat.mul(Nat.div(x, D), D), Nat.mod(x, D)) == x : Nat}:
338  NL.dmq(x, D, hD)
339
340def dml(+x: Nat, +D: Nat, +hD: {Nat.is_lt(0n, D) == True{} : Bool}) -> {Nat.is_lt(Nat.mod(x, D), D) == True{} : Bool}:
341  NL.dml(x, D, hD)
342
343# q < 2^32: the digit as it is
344def cl_t(+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}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +qq: WU.U64, +uu: U32, +hq: {SW.value(qq) == Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}, +hu: {v(uu) == Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}, +hz: {U32.is_zero(X.hi(qq)) == True{} : Bool}) -> {F.sq_clamp(e, X.lo(X.isqrt(nh)), qq, uu, True{}) == 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)))))), x) : F.F64}:
345  +eq1 = Equal.trans(Nat, v(X.lo(qq)), SW.value(qq), Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), W64E.lo_hi0(qq, hz), hq)
346  +hc = Equal.trans(Nat, Nat.add(Nat.mul(v(X.lo(qq)), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(uu)), Nat.add(Nat.mul(Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Equal.trans(Nat, Nat.add(Nat.mul(v(X.lo(qq)), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(uu)), Nat.add(Nat.mul(Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(uu)), Nat.add(Nat.mul(Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(uu)), v(X.lo(qq)), Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), eq1), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), z), v(uu), Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), hu)), dmq(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.d_pos(one, h1, nh, h62, h60)))
347  +hU = L.subst(Nat, z => {Nat.is_le(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(uu), Equal.sym(Nat, v(uu), Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), hu), N.lt_le(Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), dml(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.d_pos(one, h1, nh, h62, h60))))
348  +hQ = WW.lt_one(32n, one, h1, v(X.lo(qq)), LW.vb(X.lo(qq)))
349  qu_v(one, h1, nh, h62, h60, e, x, hx, X.lo(qq), uu, hc, hU, hQ)
350
351
352# q = 2^32 (r = 2 s): taken as 2^32 - 1 with u = 2 s
353# over an open all-ones word o: v(4294967295) would be expanded in unary
354def cl_f_o(+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}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +qq: WU.U64, +uu: U32, +hq: {SW.value(qq) == Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}, +hz: {U32.is_zero(X.hi(qq)) == False{} : Bool}, +o: U32, +po: {o == U32{WD.mask(32n, 32n)} : U32}) -> {F.sq_qu(e, X.lo(X.isqrt(nh)), o, U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(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)))))), x) : F.F64}:
355  +e1 = Equal.trans(Nat, 1n+v(o), WD.sc(32n, one), C.shift(32n, one), W64S.mask_v(32n, {==}, one, h1, o, po), Equal.sym(Nat, C.shift(32n, one), WD.sc(32n, one), W64M.shift_sc(32n, one)))
356  +hQ = L.subst(Nat, z => {Nat.is_lt(v(o), z) == True{} : Bool}, 1n+v(o), C.shift(32n, one), e1, N.lt_succ(v(o)))
357  +eU = QV.dw_v(one, h1, nh, h62, h60)
358  +hhi = WA.pos_ne(v(X.hi(qq)), Equal.trans(Bool, Nat.is_eq(v(X.hi(qq)), 0n), U32.is_zero(X.hi(qq)), False{}, Equal.sym(Bool, U32.is_zero(X.hi(qq)), Nat.is_eq(v(X.hi(qq)), 0n), LW.zero_nat(X.hi(qq))), hz))
359  +g1 = N.le_trans(C.shift(32n, one), C.shift(32n, v(X.hi(qq))), SW.value(qq), WW.shift_mono(32n, one, v(X.hi(qq)), L.subst(Nat, z => {Nat.is_le(z, v(X.hi(qq))) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), hhi)), L.subst(Nat, z => {Nat.is_le(C.shift(32n, v(X.hi(qq))), z) == True{} : Bool}, Nat.add(C.shift(32n, v(X.hi(qq))), v(X.lo(qq))), SW.value(qq), Equal.trans(Nat, Nat.add(C.shift(32n, v(X.hi(qq))), v(X.lo(qq))), Nat.add(v(X.lo(qq)), C.shift(32n, v(X.hi(qq)))), SW.value(qq), NA.add_comm(C.shift(32n, v(X.hi(qq))), v(X.lo(qq))), Equal.sym(Nat, SW.value(qq), Nat.add(v(X.lo(qq)), C.shift(32n, v(X.hi(qq)))), WA.val_eta(qq))), N.le_add_right(C.shift(32n, v(X.hi(qq))), v(X.lo(qq)))))
360  +hqD = L.subst(Nat, z => {Nat.is_le(Nat.mul(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))))) == True{} : Bool}, Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(qq), Equal.sym(Nat, SW.value(qq), Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), hq), QV.dq_le(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.d_pos(one, h1, nh, h62, h60)))
361  +g2 = SK.qb(one, h1, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), SW.value(qq), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), hqD, QV.r_le(one, h1, nh, h62, h60), QV.d_pos(one, h1, nh, h62, h60))
362  +eq1 = N.le_antisym(SW.value(qq), C.shift(32n, one), g2, g1)
363  +g3 = L.subst(Nat, z => {Nat.is_le(Nat.mul(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))))) == True{} : Bool}, SW.value(qq), C.shift(32n, one), eq1, hqD)
364  +eP = Equal.trans(Nat, Nat.mul(C.shift(32n, one), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mul(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), C.shift(32n, one)), C.shift(32n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), NA.mul_comm(C.shift(32n, one), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Equal.sym(Nat, C.shift(32n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.mul(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), C.shift(32n, one)), WW.shift_mul_one(32n, one, h1, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))))
365  +g4 = L.subst(Nat, z => {Nat.is_le(z, C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))))) == True{} : Bool}, Nat.mul(C.shift(32n, one), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), eP, g3)
366  +g5 = N.le_antisym(Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.r_le(one, h1, nh, h62, h60), shl_le_inv(32n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), g4))
367  +hc0 = Equal.trans(Nat, Nat.add(Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), NA.add_comm(Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Equal.trans(Nat, Nat.add(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.mul(C.shift(32n, one), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Equal.cong(Nat, Nat, z => Nat.mul(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), 1n+v(o), C.shift(32n, one), e1), Equal.trans(Nat, Nat.mul(C.shift(32n, one), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), eP, Equal.cong(Nat, Nat, z => C.shift(32n, z), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Equal.sym(Nat, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), g5)))))
368  +hc = Equal.trans(Nat, Nat.add(Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Nat.add(Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(v(o), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), z), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), eU), hc0)
369  +hU = L.subst(Nat, z => {Nat.is_le(z, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) == True{} : Bool}, Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Equal.sym(Nat, v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), eU), N.le_refl(Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))))
370  qu_v(one, h1, nh, h62, h60, e, x, hx, o, U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))), hc, hU, hQ)
371
372def cl_f(+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}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +qq: WU.U64, +uu: U32, +hq: {SW.value(qq) == Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}, +hz: {U32.is_zero(X.hi(qq)) == False{} : Bool}) -> {F.sq_clamp(e, X.lo(X.isqrt(nh)), qq, uu, False{}) == 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)))))), x) : F.F64}:
373  cl_f_o(one, h1, nh, h62, h60, e, x, hx, qq, uu, hq, hz, 4294967295, {==})
374
375def cl_v(+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}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +qq: WU.U64, +uu: U32, +hq: {SW.value(qq) == Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}, +hu: {v(uu) == Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}, +sm: Bool, +hsm: {U32.is_zero(X.hi(qq)) == sm : Bool}) -> {F.sq_clamp(e, X.lo(X.isqrt(nh)), qq, uu, sm) == 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)))))), x) : F.F64}:
376  match sm:
377    case True{}:
378      cl_t(one, h1, nh, h62, h60, e, x, hx, qq, uu, hq, hu, hsm)
379    case False{}:
380      cl_f(one, h1, nh, h62, h60, e, x, hx, qq, uu, hq, hsm)
381
382def div_v(+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}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, p: WU.U64 & U32, +hq: {SW.value(X.fst_q(p)) == Nat.div(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}, +hu: {v(X.snd_r(p)) == Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))) : Nat}) -> {F.sq_div(e, X.lo(X.isqrt(nh)), p) == 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)))))), x) : F.F64}:
383  match p:
384    case Tuple{+qq, +uu}:
385      cl_v(one, h1, nh, h62, h60, e, x, hx, qq, uu, hq, hu, U32.is_zero(X.hi(qq)), {==})
386
387
388# the F64 root: roundPackToF64 of isqrt(nh 2^64) with its sticky bit
389def sqr_root_v(+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}, +e: Nat, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}) -> {F.sq_root(e, 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)))))), x) : F.F64}:
390  +hu = Equal.trans(Nat, v(X.snd_r(X.div32(WU.U64{0, X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))}, U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))), Nat.mod(SW.value(WU.U64{0, X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))}), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), W64D.div32_rem(WU.U64{0, X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))}, U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))), QV.dw_nz(one, h1, nh, h62, h60)), Equal.trans(Nat, Nat.mod(SW.value(WU.U64{0, X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))}), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, z), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh))))), v(X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))), Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh)))), QV.lo_w(one, h1, nh, h62, h60)), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, Nat.sub(SW.value(nh), Nat.mul(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))))), z), v(U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), Nat.add(M.isqrt(SW.value(nh)), M.isqrt(SW.value(nh))), QV.dw_v(one, h1, nh, h62, h60))))
391  div_v(one, h1, nh, h62, h60, e, x, hx, X.div32(WU.U64{0, X.lo(X.sub(nh, X.mul32(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))))}, U32.add(X.lo(X.isqrt(nh)), X.lo(X.isqrt(nh)))), QV.q_v(one, h1, nh, h62, h60), hu)