~/bend-docscommunity

proofs/math/typed/f64sqr.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqr.bend as F64sqr

32 imports
import Base
import ./f64light.bend as FL
import ./natlight.bend as NL
import ../../../spec/lib/common.bend as C
import ../../../spec/math/f64.bend as SF
import ../../../spec/math/w64.bend as SW
import ../../../src/math/f64.bend as F
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/word.bend as WD
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ../natural/sqrtn.bend as SQ2
import ./width.bend as WW
import ./natcmp.bend as NC
import ./u32laws.bend as LW
import ./w64add.bend as WA
import ./w64mul.bend as W64M
import ./w64sqrt.bend as W64S
import ./w64div.bend as W64D
import ./w64est.bend as W64E
import ./w64dm.bend as DM
import ./f64round.bend as FR
import ./f64rtools.bend as RT
import ./w64m128.bend as M128
import ./f64sqa.bend as AQ
import ./f64sqw.bend as QW
import ./f64sqk.bend as SK
import ./f64sqv.bend as QV

Definitions

def v source · line 42 · raw

@+x:U32 -> Nat

def eqsh source · line 46 · raw

@+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}

x + b == y + a gives (a == b) == (x == y)

def rearr source · line 53 · raw

@+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}

((a + b) + d) + c == (a + (b + c)) + d

def ident source · line 62 · raw

@+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) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, rr) : Nat} -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, n)), Nat.mul(Q, Q)) == Nat.add(Nat.mul(Nat.add(Q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s)), Nat.add(Q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, U)) : Nat}

N + q^2 == S0^2 + u 2^32

def nn source · line 76 · raw

@+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, n) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, n)) : Nat}

def identN source · line 80 · raw

@+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) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, rr) : Nat} -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, n), Nat.mul(Q, Q)) == Nat.add(Nat.mul(Nat.add(Q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s)), Nat.add(Q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, U)) : Nat}

N + q^2 == S0^2 + u 2^32, with N = nh 2^64

def lo_bound source · line 84 · raw

@+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) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, rr) : Nat} -> @+hU:{Nat.is_le(U, D) == True{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, n), Nat.mul(1n+Nat.add(Q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s)), 1n+Nat.add(Q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s)))) == True{} : Bool}

N < (S0 + 1)^2, so isqrt(N) <= S0

def hi_bound source · line 95 · raw

@+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) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, rr) : Nat} -> @+hQ:{Nat.is_lt(Q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> @+hT:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, one), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, n))) == True{} : Bool} -> {Nat.is_le(Nat.add(Q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s)), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, n)), 2n)) == True{} : Bool}

S0 <= isqrt(N) + 2, for q < 2^32 and isqrt(N) >= 2^62

def two62 source · line 104 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, one)) == True{} : Bool}

def brA_T source · line 109 · raw

@+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) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, rr) : Nat} -> @+hU:{Nat.is_le(U, D) == True{} : Bool} -> @+hAB:{Nat.is_le(Nat.mul(Q, Q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, U)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, n)) == Nat.add(Q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s)) : Nat}

branch A: q^2 <= u 2^32 gives the root S0, exact iff q^2 == u 2^32

def brA_eq source · line 117 · raw

@+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) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, rr) : Nat} -> {Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, U), Nat.mul(Q, Q)) == Nat.is_eq(Nat.mul(Nat.add(Q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s)), Nat.add(Q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, n)) : Bool}

def brB_nd source · line 121 · raw

@+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) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, rr) : Nat} -> @+hBA:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, U), Nat.mul(Q, Q)) == True{} : Bool} -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, n), Nat.sub(Nat.mul(Q, Q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, U))) == Nat.mul(Nat.add(Q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s)), Nat.add(Q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s))) : Nat}

branch B: q^2 > u 2^32, D = q^2 - u 2^32 > 0 and N + D == S0^2

def brB_pos source · line 127 · raw

@+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) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, rr) : Nat} -> @+hBA:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, U), Nat.mul(Q, Q)) == True{} : Bool} -> {Nat.is_lt(0n, Nat.sub(Nat.mul(Q, Q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, U))) == True{} : Bool}

def c_eq source · line 135 · raw

@+S2:Nat -> {Nat.sub(Nat.add(2n+S2, 2n+S2), 1n) == 1n+Nat.add(1n+S2, 1n+S2) : Nat}

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

def c2_eq source · line 138 · raw

@+S2:Nat -> {Nat.sub(Nat.sub(Nat.add(2n+S2, 2n+S2), 1n), 2n) == 1n+Nat.add(S2, S2) : Nat}

def sq0_eq source · line 142 · raw

@+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}

def sq1_eq source · line 145 · raw

@+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}

def b_s1 source · line 150 · raw

@+n:Nat -> @+S2:Nat -> @+Dx:Nat -> @+hnd:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.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(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, n), Dx) : Nat}

S1^2 + c == N + D

def b1_T source · line 154 · raw

@+n:Nat -> @+S2:Nat -> @+Dx:Nat -> @+hnd:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.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} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, n)) == 1n+S2 : Nat}

D <= c: the root is S1, exact iff D == c

def b1_eq source · line 163 · raw

@+n:Nat -> @+S2:Nat -> @+Dx:Nat -> @+hnd:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.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), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, n)) : Bool}

def b_s2 source · line 167 · raw

@+n:Nat -> @+S2:Nat -> @+Dx:Nat -> @+hnd:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.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(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, n), Nat.sub(Dx, Nat.sub(Nat.add(2n+S2, 2n+S2), 1n))) : Nat}

S2^2 + (c - 2) == N + (D - c) for c < D

def b2_T source · line 175 · raw

@+n:Nat -> @+S2:Nat -> @+Dx:Nat -> @+hnd:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, n)), 2n)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, n)) == S2 : Nat}

c < D: the root is S2 (it is at least S0 - 2), exact iff D - c == c - 2

def b2_eq source · line 186 · raw

@+n:Nat -> @+S2:Nat -> @+Dx:Nat -> @+hnd:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.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), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, n)) : Bool}

def fin_v source · line 191 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == False{} : Bool} -> @+e:Nat -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+t:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+st:Bool -> @+ht:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(t) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))) : Nat} -> @+hst:{st == Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_fin(e, t, st) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))))), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

roundPackToF64 of the root with its sticky bit is the spec's round

def sticky_eq source · line 202 · raw

@+a:Bool -> @+b:Bool -> @+h:{a == b : Bool} -> {Bool.not(a) == Bool.not(b) : Bool}

def s0v source · line 206 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == False{} : Bool} -> @+q:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}) == Nat.add(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) : Nat}

def bv_q source · line 209 · raw

@+q:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(q, q)) == Nat.mul(v(q), v(q)) : Nat}

def s0_63 source · line 213 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == False{} : Bool} -> @+q:U32 -> @+hQ:{Nat.is_lt(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> {Nat.is_lt(Nat.add(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, one)) == True{} : Bool}

S0 < 2^63: q < 2^32 and s + 1 <= 2^31

def s0_2 source · line 222 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == False{} : Bool} -> @+q:U32 -> @+u:U32 -> @+hc:{Nat.add(Nat.mul(v(q), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), v(u)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))) : Nat} -> @+hU:{Nat.is_le(v(u), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) == True{} : Bool} -> @+hQ:{Nat.is_lt(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> {Nat.is_le(2n, Nat.add(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))) == True{} : Bool}

2 <= S0 (S0 >= isqrt(N) >= 2^62)

def hS source · line 227 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == False{} : Bool} -> @+q:U32 -> @+u:U32 -> @+hc:{Nat.add(Nat.mul(v(q), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), v(u)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))) : Nat} -> @+hU:{Nat.is_le(v(u), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) == True{} : Bool} -> @+hQ:{Nat.is_lt(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> {Nat.add(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) == 2n+Nat.sub(Nat.add(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 2n) : Nat}

def cw_v source · line 230 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == False{} : Bool} -> @+q:U32 -> @+u:U32 -> @+hc:{Nat.add(Nat.mul(v(q), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), v(u)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))) : Nat} -> @+hU:{Nat.is_le(v(u), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) == True{} : Bool} -> @+hQ:{Nat.is_lt(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{1, 0})) == Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 2n)), 1n) : Nat}

def le_ba source · line 240 · raw

@+q:U32 -> @+u:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(q, q), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, u}) == Nat.is_le(Nat.mul(v(q), v(q)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(u))) : Bool}

def eq_ab source · line 243 · raw

@+q:U32 -> @+u:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.eq(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, u}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(q, q)) == Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(u)), Nat.mul(v(q), v(q))) : Bool}

def brA_w source · line 248 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), v(u)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))) : Nat} -> @+hU:{Nat.is_le(v(u), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) == True{} : Bool} -> @+hQ:{Nat.is_lt(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> @+hge:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(q, q), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, u}) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_rem(e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, u}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(q, q), True{}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))))), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

branch A: the root S0

def one_le source · line 257 · raw

@+x:Nat -> @+h:{Nat.is_le(2n, x) == True{} : Bool} -> {Nat.is_le(1n, x) == True{} : Bool}

def dw_value source · line 260 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == False{} : Bool} -> @+q:U32 -> @+u:U32 -> @+hc:{Nat.add(Nat.mul(v(q), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), v(u)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))) : Nat} -> @+hU:{Nat.is_le(v(u), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) == True{} : Bool} -> @+hQ:{Nat.is_lt(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> @+hBA:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(q, q), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, u})) == Nat.sub(Nat.mul(v(q), v(q)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(u))) : Nat}

def s0w_v source · line 264 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == False{} : Bool} -> @+q:U32 -> @+u:U32 -> @+hc:{Nat.add(Nat.mul(v(q), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), v(u)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))) : Nat} -> @+hU:{Nat.is_le(v(u), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) == True{} : Bool} -> @+hQ:{Nat.is_lt(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}) == 2n+Nat.sub(Nat.add(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 2n) : Nat}

def hnd_v source · line 267 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == False{} : Bool} -> @+q:U32 -> @+u:U32 -> @+hc:{Nat.add(Nat.mul(v(q), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), v(u)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))) : Nat} -> @+hU:{Nat.is_le(v(u), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) == True{} : Bool} -> @+hQ:{Nat.is_lt(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> @+hBA:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool} -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), Nat.sub(Nat.mul(v(q), v(q)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(u)))) == Nat.mul(2n+Nat.sub(Nat.add(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 2n)) : Nat}

def sm_v source · line 270 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == False{} : Bool} -> @+q:U32 -> @+u:U32 -> @+hc:{Nat.add(Nat.mul(v(q), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), v(u)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))) : Nat} -> @+hU:{Nat.is_le(v(u), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) == True{} : Bool} -> @+hQ:{Nat.is_lt(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> @+hBA:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(q, q), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, u}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{1, 0})) == Nat.is_le(Nat.sub(Nat.mul(v(q), v(q)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(u))), Nat.sub(Nat.add(2n+Nat.sub(Nat.add(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 2n), 2n+Nat.sub(Nat.add(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 2n)), 1n)) : Bool}

def brB1_w source · line 274 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), v(u)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))) : Nat} -> @+hU:{Nat.is_le(v(u), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) == True{} : Bool} -> @+hQ:{Nat.is_lt(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> @+hBA:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool} -> @+hs:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(q, q), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, u}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{1, 0})) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_d1(e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(q, q), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, u}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{1, 0}), True{}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))))), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

branch B, D <= c: the root S0 - 1

def brB2_w source · line 287 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), v(u)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))) : Nat} -> @+hU:{Nat.is_le(v(u), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) == True{} : Bool} -> @+hQ:{Nat.is_lt(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> @+hBA:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool} -> @+hs:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(q, q), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, u}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{1, 0})) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_d2(e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(q, q), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, u}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{1, 0})) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))))), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

branch B, D > c: the root S0 - 2

def d1_v source · line 305 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), v(u)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))) : Nat} -> @+hU:{Nat.is_le(v(u), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) == True{} : Bool} -> @+hQ:{Nat.is_lt(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> @+hBA:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(u)), Nat.mul(v(q), v(q))) == True{} : Bool} -> @+sm:Bool -> @+hsm:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(q, q), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, u}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{1, 0})) == sm : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_d1(e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(q, q), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, u}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{1, 0}), sm) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))))), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def rem_v source · line 312 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), v(u)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))) : Nat} -> @+hU:{Nat.is_le(v(u), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) == True{} : Bool} -> @+hQ:{Nat.is_lt(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> @+g:Bool -> @+hg:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(q, q), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, u}) == g : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_rem(e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{q, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh))}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, u}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(q, q), g) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))))), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def qu_v source · line 320 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.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(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), v(u)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))) : Nat} -> @+hU:{Nat.is_le(v(u), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) == True{} : Bool} -> @+hQ:{Nat.is_lt(v(q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_qu(e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh)), q, u) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))))), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def shl_le_c source · line 324 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, b)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_le(a, b) == c : Bool} -> {c == True{} : Bool}

def shl_le_inv source · line 333 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, b)) == True{} : Bool} -> {Nat.is_le(a, b) == True{} : Bool}

shift(k, a) <= shift(k, b) gives a <= b

def dmq source · line 337 · raw

@+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}

x / D * D + x mod D == x and x mod D < D

def dml source · line 340 · raw

@+x:Nat -> @+D:Nat -> @+hD:{Nat.is_lt(0n, D) == True{} : Bool} -> {Nat.is_lt(Nat.mod(x, D), D) == True{} : Bool}

def cl_t source · line 344 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == False{} : Bool} -> @+e:Nat -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+qq:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+uu:U32 -> @+hq:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(qq) == Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) : Nat} -> @+hu:{v(uu) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) : Nat} -> @+hz:{U32.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(qq)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_clamp(e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh)), qq, uu, True{}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))))), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

q < 2^32: the digit as it is

def cl_f_o source · line 354 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == False{} : Bool} -> @+e:Nat -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+qq:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+uu:U32 -> @+hq:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(qq) == Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) : Nat} -> @+hz:{U32.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(qq)) == False{} : Bool} -> @+o:U32 -> @+po:{o == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 32n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_qu(e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh)), o, U32.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))))), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

q = 2^32 (r = 2 s): taken as 2^32 - 1 with u = 2 s over an open all-ones word o: v(4294967295) would be expanded in unary

def cl_f source · line 372 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == False{} : Bool} -> @+e:Nat -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+qq:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+uu:U32 -> @+hq:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(qq) == Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) : Nat} -> @+hz:{U32.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(qq)) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_clamp(e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh)), qq, uu, False{}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))))), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def cl_v source · line 375 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == False{} : Bool} -> @+e:Nat -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @+qq:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+uu:U32 -> @+hq:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(qq) == Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) : Nat} -> @+hu:{v(uu) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) : Nat} -> @+sm:Bool -> @+hsm:{U32.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(qq)) == sm : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_clamp(e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh)), qq, uu, sm) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))))), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def div_v source · line 382 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == False{} : Bool} -> @+e:Nat -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> @p:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, U32) -> @+hq:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.fst_q(p)) == Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) : Nat} -> @+hu:{v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.snd_r(p)) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))))), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_div(e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.isqrt(nh)), p) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))))), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def sqr_root_v source · line 389 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == True{} : Bool} -> @+h60:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(60n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)) == False{} : Bool} -> @+e:Nat -> @+x:Nat -> @+hx:{Nat.add(x, 2180n) == e : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_root(e, nh) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh)))))), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

the F64 root: roundPackToF64 of isqrt(nh 2^64) with its sticky bit