~/bend-docscommunity

proofs/math/typed/f64sqf.bend checks

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

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

Definitions

def p_ge source · line 21 · raw

@+p:Nat -> @+Ep:Nat -> @+hp:{Nat.add(Nat.add(p, p), 1075n) == Nat.add(Ep, 4096n) : Nat} -> @+c:Bool -> @+hc:{Nat.is_lt(p, 1132n) == c : Bool} -> {c == False{} : Bool}

def shift_nest source · line 31 · raw

@+j:Nat -> @+sc:Nat -> @+MX:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(sc, MX))))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.add(Nat.add(j, j), Nat.add(72n, sc)), MX) : Nat}

def sqg source · line 43 · 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} -> @+MX:Nat -> @+sa:Nat -> @+ci:Nat -> @+cs:Nat -> @+hnh:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(nh) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.add(sa, ci), MX)) : Nat} -> @+Ep:Nat -> @+p:Nat -> @+hp:{Nat.add(Nat.add(p, p), 1075n) == Nat.add(Ep, 4096n) : Nat} -> @+hpe:{Nat.div(Nat.sub(Nat.add(Ep, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off), 1075n), 2n) == p : Nat} -> @+EN:Nat -> @+hE:{Nat.add(Ep, ci) == EN : Nat} -> @+XX:Nat -> @+hEN:{Nat.add(EN, sa) == Nat.add(XX, 2171n) : Nat} -> @+Mq:Nat -> @+hMq:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(200n, Mq) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.add(200n, cs), MX) : Nat} -> @+Xq:Nat -> @+q:Nat -> @+hq:{Nat.add(Nat.add(q, q), cs) == XX : Nat} -> @+hqd:{Nat.div(Xq, 2n) == q : Nat} -> @+j:Nat -> @+hj:{Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))) == Nat.add(200n, cs) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Ep, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off), 1075n), 2n), 1048n), nh) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sqrt_even(Mq, Xq) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

the generic even-exponent root