~/bend-docscommunity

proofs/math/typed/f64sqs.bend checks

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

14 imports
import Base
import ./f64light.bend as FL
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/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 ./f64rtools.bend as RT
import ./f64sqa.bend as AQ

Definitions

def hb2n source · line 20 · raw

@+c:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(c)) == 0n : Nat}

def bb2n source · line 27 · raw

@+c:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(c)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(c) : Nat}

def eb2n source · line 34 · raw

@+c:Bool -> {Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(c)), 0n) == c : Bool}

def mform source · line 41 · raw

@+n:Nat -> @+j:Nat -> {Nat.add(Nat.mul(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.pow(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 2n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n)))))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.pow(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 2n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))))), Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))))) : Nat}

def s_high source · line 44 · raw

@+n:Nat -> @+j:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(1n+j, Nat.add(Nat.mul(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.pow(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 2n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))))))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n) : Nat}

def s_low source · line 49 · raw

@+n:Nat -> @+j:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(1n+j, Nat.add(Nat.mul(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.pow(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 2n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))))))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.pow(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 2n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))))), Nat.double(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n))))) : Nat}

def s_st source · line 58 · raw

@+n:Nat -> @+j:Nat -> {Bool.not(Nat.is_eq(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.pow(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 2n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))))), Nat.double(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n))))), 0n)) == Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n)), n)) : Bool}

def s_bl source · line 68 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> @+j:Nat -> @+h62:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, one), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n)) == True{} : Bool} -> {Nat.is_le(Nat.add(1n+j, 55n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(Nat.add(Nat.mul(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.pow(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 2n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n)))))))) == True{} : Bool}

def sq_spec source · line 79 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> @+j:Nat -> @+h62:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, one), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n)) == True{} : Bool} -> @+Es:Nat -> @+x:Nat -> @+hEx:{Nat.add(Es, 1n+j) == x : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, Nat.add(Nat.mul(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.pow(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 2n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n)))))), Es) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n)), n)))), x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

the spec's rounded root equals roundPackToF64 of the sticky floor root