~/bend-docscommunity

proofs/math/typed/f64adds.bend checks

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

20 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 ../../lib/u32half.bend as UH
import ./width.bend as WW
import ./u32laws.bend as LW
import ./w64sh.bend as SH
import ./natcmp.bend as NC
import ./f64round.bend as FR
import ./f64rtools.bend as RT
import ./f64addp.bend as AP
import ./f64adda.bend as AA
import ./f64nrp.bend as NP

Definitions

def jam_le source · line 26 · raw

@+hh:Nat -> @+ll:Nat -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(hh, ll), 1n+hh) == True{} : Bool}

def low_sh source · line 32 · raw

@+d:Nat -> @+k:Nat -> @+m:Nat -> @+hd:{Nat.is_le(d, k) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(d, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m)) == 0n : Nat}

def d11_c source · line 36 · raw

@+d:Nat -> @+S1:Nat -> @+c:Bool -> @+hc:{Nat.is_le(d, 10n) == c : Bool} -> @+hl:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(d, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(10n, S1)), 0n) == False{} : Bool} -> {Nat.is_le(11n, d) == True{} : Bool}

def shmk source · line 43 · raw

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

def wbig source · line 48 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+t:Nat -> @+S:Nat -> @+d:Nat -> @+hd:{Nat.is_le(2n, d) == True{} : Bool} -> @+hT:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, Nat.double(t)) == False{} : Bool} -> @+hS:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, S) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(d, 61n), Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(d, Nat.double(t)), S)) == False{} : Bool}

W = 2^d T - S is at least 2^d * 2^61 when d >= 2, T >= 2^62, S < 2^63

def posz source · line 59 · raw

@+n:Nat -> @+h:{Nat.is_le(1n, n) == True{} : Bool} -> {Nat.is_eq(n, 0n) == False{} : Bool}

def sub_odd source · line 66 · raw

@+t:Nat -> @+k:Nat -> @+hk:{Nat.is_lt(k, t) == True{} : Bool} -> {Nat.is_eq(Nat.sub(Nat.double(t), 1n+Nat.double(k)), 0n) == False{} : Bool}

def hlt source · line 75 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Nat -> @+S1:Nat -> @+d:Nat -> @+x0:Nat -> @+hsig:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig) == Nat.sub(Nat.double(t), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(d, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(10n, S1)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(d, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(10n, S1)))) : Nat} -> @+he:{Nat.add(Nat.add(x0, d), 2180n) == e : Nat} -> @+hx63:{Nat.is_le(63n, Nat.add(x0, d)) == True{} : Bool} -> @+hd1:{Nat.is_le(1n, d) == True{} : Bool} -> @+hS:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(10n, S1)) == True{} : Bool} -> @+hT62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, Nat.double(t)) == False{} : Bool} -> @+hT63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, Nat.double(t)) == True{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(d, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(10n, S1)), Nat.double(t)) == True{} : Bool}

def smb_c source · line 80 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Nat -> @+S1:Nat -> @+d:Nat -> @+x0:Nat -> @+hsig:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(sig) == Nat.sub(Nat.double(t), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(d, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(10n, S1)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(d, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(10n, S1)))) : Nat} -> @+he:{Nat.add(Nat.add(x0, d), 2180n) == e : Nat} -> @+hx63:{Nat.is_le(63n, Nat.add(x0, d)) == True{} : Bool} -> @+hd1:{Nat.is_le(1n, d) == True{} : Bool} -> @+hS:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(10n, S1)) == True{} : Bool} -> @+hT62:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(62n, Nat.double(t)) == False{} : Bool} -> @+hT63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, Nat.double(t)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(d, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(10n, S1)), 0n) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_round_pack(s, e, sig) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(d, Nat.double(t)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(10n, S1)), x0) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}