proofs/math/typed/f64sqs.bend

bend-collections-laws-math@1.0.0.0 · 86 lines · 9 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
3import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
4import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
5import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
6import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
7import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
8import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
9import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
10import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
11import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqa.bend as AQ
15
16# The spec's root 2 * isqrt(N * 4^j) + [inexact], cut at bit 1 + j, is
17# SoftFloat's floor(sqrt(N)) with its sticky bit (Flocq's sqrt with a
18# sticky remainder bit, round_NE once).
19
20def hb2n(+c: Bool) -> {C.half(SF.b2n(c)) == 0n : Nat}:
21  match c:
22    case True{}:
23      {==}
24    case False{}:
25      {==}
26
27def bb2n(+c: Bool) -> {C.bit(SF.b2n(c)) == SF.b2n(c) : Nat}:
28  match c:
29    case True{}:
30      {==}
31    case False{}:
32      {==}
33
34def eb2n(+c: Bool) -> {Nat.is_eq(SF.b2n(Bool.not(c)), 0n) == c : Bool}:
35  match c:
36    case True{}:
37      {==}
38    case False{}:
39      {==}
40
41def mform(+n: Nat, +j: Nat) -> {Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))) == Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))) : Nat}:
42  Equal.trans(Nat, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Nat.add(Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), Equal.cong(Nat, Nat, z => Nat.add(z, SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), Equal.sym(Nat, Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), NA.double_mul(M.isqrt(C.shift(j, C.shift(j, n)))))), NA.add_comm(Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))
43
44def s_high(+n: Nat, +j: Nat) -> {C.high(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))) == M.isqrt(n) : Nat}:
45  +e1 = Equal.cong(Nat, Nat, z => C.high(1n+j, z), Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), mform(n, j))
46  +e2 = Equal.cong(Nat, Nat, z => C.high(j, z), C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), M.isqrt(C.shift(j, C.shift(j, n))), Equal.trans(Nat, C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), Nat.add(C.half(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), M.isqrt(C.shift(j, C.shift(j, n)))), M.isqrt(C.shift(j, C.shift(j, n))), WW.half_dbl(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), M.isqrt(C.shift(j, C.shift(j, n)))), Equal.cong(Nat, Nat, z => Nat.add(z, M.isqrt(C.shift(j, C.shift(j, n)))), C.half(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), 0n, hb2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))))
47  Equal.trans(Nat, C.high(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), C.high(j, C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))))), M.isqrt(n), Equal.trans(Nat, C.high(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), C.high(1n+j, Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), C.high(j, C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))))), e1, {==}), Equal.trans(Nat, C.high(j, C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))))), C.high(j, M.isqrt(C.shift(j, C.shift(j, n)))), M.isqrt(n), e2, AQ.sc_high(n, j)))
48
49def s_low(+n: Nat, +j: Nat) -> {C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))) == Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))) : Nat}:
50  +e1 = Equal.cong(Nat, Nat, z => C.low(1n+j, z), Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), mform(n, j))
51  +eh = Equal.trans(Nat, C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), Nat.add(C.half(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), M.isqrt(C.shift(j, C.shift(j, n)))), M.isqrt(C.shift(j, C.shift(j, n))), WW.half_dbl(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), M.isqrt(C.shift(j, C.shift(j, n)))), Equal.cong(Nat, Nat, z => Nat.add(z, M.isqrt(C.shift(j, C.shift(j, n)))), C.half(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), 0n, hb2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))
52  +eb = Equal.trans(Nat, C.bit(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), C.bit(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), WW.bit_dbl(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), M.isqrt(C.shift(j, C.shift(j, n)))), bb2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))
53  +e2 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.double(C.low(j, C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))))))), C.bit(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), eb)
54  +e3 = Equal.cong(Nat, Nat, z => Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(C.low(j, z))), C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), M.isqrt(C.shift(j, C.shift(j, n))), eh)
55  +e4 = Equal.cong(Nat, Nat, z => Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(z)), C.low(j, M.isqrt(C.shift(j, C.shift(j, n)))), Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), AQ.sc_low(n, j))
56  Equal.trans(Nat, C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), C.low(1n+j, Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), e1, Equal.trans(Nat, C.low(1n+j, Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(C.low(j, C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), e2, Equal.trans(Nat, Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(C.low(j, C.half(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(C.low(j, M.isqrt(C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), e3, e4)))
57
58def s_st(+n: Nat, +j: Nat) -> {Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)) == Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)) : Bool}:
59  +z1 = FL.add_eq0(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))))
60  +z2 = Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))), 0n)), Nat.is_eq(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), 0n), Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))), eb2n(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))
61  +z3 = Equal.cong(Bool, Bool, t => Bool.and(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))), t), Nat.is_eq(Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))), 0n), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n), WW.dbl_eq0(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))))
62  +z4 = Equal.cong(Nat, Bool, w => Bool.and(Nat.is_eq(w, C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), AQ.sqm(M.isqrt(C.shift(j, C.shift(j, n)))))
63  +zz = Equal.trans(Bool, Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n), Bool.and(Nat.is_eq(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), 0n), Nat.is_eq(Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))), 0n)), Bool.and(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), z1, Equal.trans(Bool, Bool.and(Nat.is_eq(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), 0n), Nat.is_eq(Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))), 0n)), Bool.and(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))), 0n)), Bool.and(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), z2, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))), 0n)), Bool.and(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), Bool.and(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), z3, z4)))
64  +n1 = Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n), Bool.and(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), zz)
65  +n2 = Equal.sym(Bool, Bool.or(Bool.not(Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))))), Bool.not(Bool.and(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n))), FL.dm2(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)))
66  Equal.trans(Bool, Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)), Bool.not(Bool.and(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n))), Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)), n1, Equal.trans(Bool, Bool.not(Bool.and(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))), Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n))), Bool.or(Bool.not(Nat.is_eq(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))), 0n)), Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(j, C.shift(j, n))), M.isqrt(C.shift(j, C.shift(j, n)))), C.shift(j, C.shift(j, n))))), Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)), n2, AQ.sc_x(n, j)))
67
68def s_bl(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +j: Nat, +h62: {Nat.is_le(C.shift(62n, one), M.isqrt(n)) == True{} : Bool}) -> {Nat.is_le(Nat.add(1n+j, 55n), M.bit_length(Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))) == True{} : Bool}:
69  +l1 = N.le_trans(C.shift(1n+j, M.isqrt(n)), Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), N.double_le(C.shift(j, M.isqrt(n)), M.isqrt(C.shift(j, C.shift(j, n))), AQ.sc_lo(n, j)), L.subst(Nat, z => {Nat.is_le(Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), z) == True{} : Bool}, Nat.add(Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), NA.add_comm(Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), N.le_add_right(Nat.double(M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))))
70  +l2 = L.subst(Nat, z => {Nat.is_le(C.shift(1n+j, M.isqrt(n)), z) == True{} : Bool}, Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Equal.sym(Nat, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(M.isqrt(C.shift(j, C.shift(j, n))))), mform(n, j)), l1)
71  +f62 = Equal.trans(Bool, C.fits(62n, M.isqrt(n)), Nat.is_lt(M.isqrt(n), C.shift(62n, one)), False{}, Equal.sym(Bool, Nat.is_lt(M.isqrt(n), C.shift(62n, one)), C.fits(62n, M.isqrt(n)), FR.lt_fit(62n, one, h1, M.isqrt(n))), N.le_not_lt(M.isqrt(n), C.shift(62n, one), h62))
72  +f54 = FL.nfit_mono(54n, 62n, M.isqrt(n), {==}, f62)
73  +fS = Equal.trans(Bool, C.fits(Nat.add(1n+j, 54n), C.shift(1n+j, M.isqrt(n))), C.fits(54n, M.isqrt(n)), False{}, RT.fits_sh(1n+j, 54n, M.isqrt(n)), f54)
74  +fM = FR.nfit(Nat.add(1n+j, 54n), C.shift(1n+j, M.isqrt(n)), Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), l2, fS)
75  +b1 = FL.nfit_bl(Nat.add(1n+j, 54n), Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), fM)
76  L.subst(Nat, z => {Nat.is_le(1n+z, M.bit_length(Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))) == True{} : Bool}, 1n+Nat.add(j, 54n), Nat.add(j, 55n), Equal.sym(Nat, Nat.add(j, 55n), 1n+Nat.add(j, 54n), N.add_succ(j, 54n)), b1)
77
78# the spec's rounded root equals roundPackToF64 of the sticky floor root
79def sq_spec(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +j: Nat, +h62: {Nat.is_le(C.shift(62n, one), M.isqrt(n)) == True{} : Bool}, +Es: Nat, +x: Nat, +hEx: {Nat.add(Es, 1n+j) == x : Nat}) -> {SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Es) == SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x) : F.F64}:
80  +r1 = RT.round_jam(False{}, 1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Es, s_bl(one, h1, n, j, h62))
81  +r2 = Equal.cong(Nat, F.F64, z => SF.round(False{}, SW.jam(z, C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))), Nat.add(Es, 1n+j)), C.high(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), M.isqrt(n), s_high(n, j))
82  +r3 = Equal.cong(Nat, F.F64, z => SF.round(False{}, SW.jam(M.isqrt(n), z), Nat.add(Es, 1n+j)), C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), s_low(n, j))
83  +r4 = Equal.cong(Nat, F.F64, z => SF.round(False{}, z, Nat.add(Es, 1n+j)), SW.jam(M.isqrt(n), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))))), SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)))), Equal.sym(Nat, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)))), SW.jam(M.isqrt(n), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))))), FL.jmin(M.isqrt(n), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))))))
84  +r5 = Equal.cong(Bool, F.F64, t => SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(t)), Nat.add(Es, 1n+j)), Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)), Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)), s_st(n, j))
85  +r6 = Equal.cong(Nat, F.F64, z => SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), z), Nat.add(Es, 1n+j), x, hEx)
86  Equal.trans(F.F64, SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))), Es), SF.round(False{}, SW.jam(C.high(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x), r1, Equal.trans(F.F64, SF.round(False{}, SW.jam(C.high(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))))), C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x), r2, Equal.trans(F.F64, SF.round(False{}, SW.jam(M.isqrt(n), C.low(1n+j, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, n)))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n)))))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x), r3, Equal.trans(F.F64, SF.round(False{}, SW.jam(M.isqrt(n), Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n)))))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x), r4, Equal.trans(F.F64, SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.add(SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, n))), 2n), C.shift(j, C.shift(j, n))))), Nat.double(Nat.sub(M.isqrt(C.shift(j, C.shift(j, n))), C.shift(j, M.isqrt(n))))), 0n)))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), Nat.add(Es, 1n+j)), SF.round(False{}, SW.jam(M.isqrt(n), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(n), M.isqrt(n)), n)))), x), r5, r6)))))