proofs/math/typed/f64addg.bend checks

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

10 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/f64.bend as SF
import ../../../src/math/f64.bend as F
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 ./natcmp.bend as NC
import ./f64round.bend as FR

Definitions

def posz source · line 15 · raw

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

def shmk source · line 22 · 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 f53 source · line 26 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+Fr:Nat -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fr) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, Nat.add(Fr, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one))) == True{} : Bool}

def v source · line 29 · raw

@+x:U32 -> Nat

def xe source · line 33 · raw

@+e:Nat -> Nat

the scale and significand of a finite double with exponent field e

def mt source · line 36 · raw

@+e:Nat -> @+F:Nat -> Nat

def xe_z source · line 39 · raw

@+e:Nat -> @+hz:{Nat.is_eq(e, 0n) == True{} : Bool} -> {xe(e) == 1926n : Nat}

def xe_n source · line 42 · raw

@+e:Nat -> @+hz:{Nat.is_eq(e, 0n) == False{} : Bool} -> {xe(e) == Nat.add(1925n, e) : Nat}

def mt_z source · line 47 · raw

@+e:Nat -> @+F:Nat -> @+hz:{Nat.is_eq(e, 0n) == True{} : Bool} -> {mt(e, F) == F : Nat}

def mt_n source · line 50 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+e:Nat -> @+F:Nat -> @+hz:{Nat.is_eq(e, 0n) == False{} : Bool} -> {mt(e, F) == Nat.add(F, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one)) : Nat}

def min_l source · line 54 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.min(a, b) == a : Nat}

def min_r source · line 63 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(b, a) == True{} : Bool} -> {Nat.min(a, b) == b : Nat}

def sub_kk source · line 74 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> {Nat.sub(Nat.add(k, a), Nat.add(k, b)) == Nat.sub(a, b) : Nat}

def sub_le source · line 81 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}

def pred_eq source · line 92 · raw

@+n:Nat -> @+hz:{Nat.is_eq(n, 0n) == False{} : Bool} -> {1n+0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/nat.pred(n) == n : Nat}

def sgn source · line 100 · raw

@+sa:Bool -> @+sb:Bool -> @+h:{Bool.not(Bool.xor(sa, sb)) == False{} : Bool} -> {Bool.not(sa) == sb : Bool}

the sign of a difference of opposite signs

def zero_v source · line 111 · raw

@+s:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zero(s) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(s) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def rca source · line 118 · raw

@+s:Bool -> @+a:Nat -> @+a2:Nat -> @+ha:{a == a2 : Nat} -> @+k:Nat -> @+k2:Nat -> @+hk:{k == k2 : Nat} -> @+m:Nat -> @+m2:Nat -> @+hm:{m == m2 : Nat} -> @+x:Nat -> @+x2:Nat -> @+hx:{x == x2 : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.add(a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m)), x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.add(a2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k2, m2)), x2) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def rcs source · line 124 · raw

@+s:Bool -> @+a:Nat -> @+a2:Nat -> @+ha:{a == a2 : Nat} -> @+k:Nat -> @+k2:Nat -> @+hk:{k == k2 : Nat} -> @+m:Nat -> @+m2:Nat -> @+hm:{m == m2 : Nat} -> @+x:Nat -> @+x2:Nat -> @+hx:{x == x2 : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m), a), x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k2, m2), a2), x2) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def bigcmp_c source · line 130 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+el:Nat -> @+es:Nat -> @+Fl:Nat -> @+Fs:Nat -> @+hFl:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fl) == True{} : Bool} -> @+hFs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fs) == True{} : Bool} -> @+hlt:{Nat.is_lt(es, el) == True{} : Bool} -> @+z:Bool -> @+hz:{Nat.is_eq(es, 0n) == z : Bool} -> {Nat.is_lt(mt(es, Fs), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl))) == True{} : Bool}

def bigcmp source · line 158 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+el:Nat -> @+es:Nat -> @+Fl:Nat -> @+Fs:Nat -> @+hFl:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fl) == True{} : Bool} -> @+hFs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fs) == True{} : Bool} -> @+hlt:{Nat.is_lt(es, el) == True{} : Bool} -> {Nat.cmp(mt(es, Fs), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl))) == LT{} : Cmp}