proofs/math/typed/f64addp.bend checks

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

13 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ./width.bend as WW
import ../../lib/u32alg.bend as A
import ./u32laws.bend as LW
import ./w64sh.bend as SH
import ./natcmp.bend as NC
import ./f64round.bend as FR

Definitions

def jam_add source · line 20 · raw

@+t:Nat -> @+h:Nat -> @+l:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(Nat.add(h, Nat.double(t)), l) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(h, l), Nat.double(t)) : Nat}

def jam_z source · line 25 · raw

@+h:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(h, 0n) == h : Nat}

def jam_nz source · line 28 · raw

@+h:Nat -> @+l:Nat -> @+hl:{Nat.is_eq(l, 0n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(h, l) == 1n+Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(h)) : Nat}

def sub_shift source · line 35 · raw

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

def half_lt source · line 39 · raw

@+k:Nat -> @+t:Nat -> @+h:{Nat.is_lt(Nat.double(k), Nat.double(t)) == True{} : Bool} -> {Nat.is_lt(k, t) == True{} : Bool}

def lt_add_l source · line 42 · raw

@+l:Nat -> @+r:Nat -> @+hl:{Nat.is_eq(l, 0n) == False{} : Bool} -> {Nat.is_lt(r, Nat.add(l, r)) == True{} : Bool}

def rnz_c source · line 49 · raw

@+l:Nat -> @+R:Nat -> @+S:Nat -> @+e:{Nat.add(l, R) == S : Nat} -> @+hl:{Nat.is_lt(l, S) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(R, 0n) == c : Bool} -> {c == False{} : Bool}

def hg_c source · line 58 · raw

@+u:Nat -> @+g:Nat -> @+b:Nat -> @+e:{Nat.add(b, 1n+g) == 2n+Nat.double(u) : Nat} -> @+hb:{Nat.is_le(b, 1n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(g) == u : Nat}

def jsub source · line 70 · raw

@+t:Nat -> @+d:Nat -> @+h:Nat -> @+l:Nat -> @+hl0:{Nat.is_eq(l, 0n) == False{} : Bool} -> @+hld:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(d, l) == True{} : Bool} -> @+hh:{Nat.is_lt(h, Nat.double(t)) == True{} : Bool} -> {Nat.sub(Nat.double(t), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(h, l)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(d, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(d, Nat.double(t)), Nat.add(l, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(d, h)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(d, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(d, Nat.double(t)), Nat.add(l, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(d, h))))) : Nat}

T - jam(h, l) is the jam of T * 2^d - (l + h * 2^d) when 0 < l < 2^d, h < T, T even