proofs/math/typed/f64adde.bend checks

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

18 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/w64.bend as X
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 ./w64sh.bend as SH
import ./f64round.bend as FR
import ./f64rtools.bend as RT
import ./f64bl.bend as BL
import ./f64norm.bend as NM
import ./f64nrp.bend as NP
import ./f64addc.bend as AC

Definitions

def lt_add_sub source · line 23 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+h:{Nat.is_lt(a, Nat.sub(c, b)) == True{} : Bool} -> @+hb:{Nat.is_le(b, c) == True{} : Bool} -> {Nat.is_le(1n+Nat.add(a, b), c) == True{} : Bool}

def smx_c source · line 29 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+e1:Nat -> @+d:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+D:Nat -> @+hd:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(d) == D : Nat} -> @+hD:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, D) == True{} : Bool} -> @+hz:{Nat.is_eq(D, 0n) == False{} : Bool} -> @+hov:{Nat.is_lt(Nat.add(e1, 1n), 2047n) == True{} : Bool} -> @+u:Bool -> @+hu:{Nat.is_lt(e1, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(d), 11n)) == u : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sm_exact3(s, e1, d, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.clz(d), 11n), u) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, D, Nat.add(1926n, e1)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def smx source · line 78 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+e1:Nat -> @+d:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+D:Nat -> @+hd:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(d) == D : Nat} -> @+hD:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, D) == True{} : Bool} -> @+hz:{Nat.is_eq(D, 0n) == False{} : Bool} -> @+hov:{Nat.is_lt(Nat.add(e1, 1n), 2047n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sm_exact(s, e1, d) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, D, Nat.add(1926n, e1)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

SoftFloat's exact equal-exponent difference is the rounded difference