~/bend-docscommunity

proofs/math/typed/f64addf.bend checks

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

22 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 ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../lib/word.bend as WD
import ./width.bend as WW
import ./u32laws.bend as LW
import ./w64add.bend as WA
import ./natcmp.bend as NC
import ./f64bits.bend as FB
import ./f64light.bend as FL
import ./f64round.bend as FR
import ./f64addc.bend as AC
import ./f64adde.bend as AE
import ./f64addg.bend as AG
import ./f64addh.bend as AH

Definitions

def v source · line 29 · raw

@+x:U32 -> Nat

def hea source · line 32 · raw

@+xl:U32 -> @+xh:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) : Nat}

def fval_g source · line 35 · raw

@+xl:U32 -> @+xh:U32 -> @+m:U32 -> @+hm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 20n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{xl, U32.and(xh, m)}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) : Nat}

def hfr source · line 38 · raw

@+xl:U32 -> @+xh:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) : Nat}

def hF source · line 41 · raw

@+xl:U32 -> @+xh:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})) == True{} : Bool}

def ap source · line 44 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+same:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.add_pick(x, y, same) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, same, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.add_mags(x, y, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.signbit(x)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sub_mags(x, y, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.signbit(x))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def le_rw source · line 51 · raw

@+a:Nat -> @+a2:Nat -> @+ha:{a == a2 : Nat} -> @+b:Nat -> @+b2:Nat -> @+hb:{b == b2 : Nat} -> @+h:{Nat.is_le(a2, b2) == True{} : Bool} -> {Nat.is_le(a, b) == True{} : Bool}

def nz_le source · line 55 · raw

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

def xe_le_c source · line 58 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> @+z:Bool -> @+hz:{Nat.is_eq(a, 0n) == z : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(a), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(b)) == True{} : Bool}

def xe_le source · line 69 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(a), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(b)) == True{} : Bool}

def xem_c source · line 72 · raw

@+e:Nat -> @+z:Bool -> @+hz:{Nat.is_eq(e, 0n) == z : Bool} -> {Nat.add(1926n, Nat.sub(e, 1n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(e) : Nat}

def xem source · line 81 · raw

@+e:Nat -> {Nat.add(1926n, Nat.sub(e, 1n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(e) : Nat}

def hovm source · line 84 · raw

@+e:Nat -> @+h:{Nat.is_lt(e, 2047n) == True{} : Bool} -> {Nat.is_lt(Nat.add(Nat.sub(e, 1n), 1n), 2047n) == True{} : Bool}

def rc2 source · line 92 · raw

@+s:Bool -> @+s2:Bool -> @+hs:{s == s2 : Bool} -> @+m:Nat -> @+m2:Nat -> @+hm:{m == m2 : Nat} -> @+x:Nat -> @+x2:Nat -> @+hx:{x == x2 : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, m, x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s2, m2, x2) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def spec_lt source · line 97 · raw

@+sa:Bool -> @+sb:Bool -> @+ea:Nat -> @+eb:Nat -> @+Fa:Nat -> @+Fb:Nat -> @+h:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.add_mag(sa, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), Nat.min(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb))), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fa)), sb, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb), Nat.min(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb))), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(eb, Fb)), Nat.min(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.add_mag(sa, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fa), sb, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(eb, Fb)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def spec_gt source · line 103 · raw

@+sa:Bool -> @+sb:Bool -> @+ea:Nat -> @+eb:Nat -> @+Fa:Nat -> @+Fb:Nat -> @+h:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.add_mag(sa, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), Nat.min(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb))), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fa)), sb, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb), Nat.min(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb))), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(eb, Fb)), Nat.min(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.add_mag(sa, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fa)), sb, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(eb, Fb), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def spec_eq source · line 109 · raw

@+sa:Bool -> @+sb:Bool -> @+ea:Nat -> @+Fa:Nat -> @+Fb:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.add_mag(sa, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), Nat.min(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea))), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fa)), sb, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), Nat.min(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea))), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fb)), Nat.min(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.add_mag(sa, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fa), sb, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fb), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def caseLT source · line 115 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+sa:Bool -> @+sb:Bool -> @+ea:Nat -> @+eb:Nat -> @+Fa:Nat -> @+Fb:Nat -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(x)) == Fa : Nat} -> @+hfb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(y)) == Fb : Nat} -> @+hFa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fa) == True{} : Bool} -> @+hFb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fb) == True{} : Bool} -> @+hb:{Nat.is_eq(eb, 2047n) == False{} : Bool} -> @+hlt:{Nat.is_lt(ea, eb) == True{} : Bool} -> @+sg:Bool -> @+hsg:{Bool.not(Bool.xor(sa, sb)) == sg : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, sg, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.am_case(x, y, sa, ea, eb, LT{}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sm_case(x, y, sa, ea, eb, LT{})) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.add_mag(sa, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fa), sb, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(eb, Fb)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def caseGT source · line 132 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+sa:Bool -> @+sb:Bool -> @+ea:Nat -> @+eb:Nat -> @+Fa:Nat -> @+Fb:Nat -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(x)) == Fa : Nat} -> @+hfb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(y)) == Fb : Nat} -> @+hFa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fa) == True{} : Bool} -> @+hFb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fb) == True{} : Bool} -> @+ha:{Nat.is_eq(ea, 2047n) == False{} : Bool} -> @+hgt:{Nat.is_lt(eb, ea) == True{} : Bool} -> @+sg:Bool -> @+hsg:{Bool.not(Bool.xor(sa, sb)) == sg : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, sg, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.am_case(x, y, sa, ea, eb, GT{}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sm_case(x, y, sa, ea, eb, GT{})) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.add_mag(sa, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fa)), sb, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(eb, Fb), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def aeq_c source · line 152 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+sa:Bool -> @+ea:Nat -> @+Fa:Nat -> @+Fb:Nat -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(x)) == Fa : Nat} -> @+hfb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(y)) == Fb : Nat} -> @+hFa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fa) == True{} : Bool} -> @+hFb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fb) == True{} : Bool} -> @+ha:{Nat.is_eq(ea, 2047n) == False{} : Bool} -> @+z:Bool -> @+hz:{Nat.is_eq(ea, 0n) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.am_eq(x, sa, ea, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(y)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(sa, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fa), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fb)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def seq source · line 173 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+sa:Bool -> @+sb:Bool -> @+hsg:{Bool.not(Bool.xor(sa, sb)) == False{} : Bool} -> @+ea:Nat -> @+Fa:Nat -> @+Fb:Nat -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(x)) == Fa : Nat} -> @+hfb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(y)) == Fb : Nat} -> @+hFa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fa) == True{} : Bool} -> @+hFb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fb) == True{} : Bool} -> @+hlta:{Nat.is_lt(ea, 2047n) == True{} : Bool} -> @+d:Cmp -> @+hd:{Nat.cmp(Fa, Fb) == d : Cmp} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sm_eq2(sa, ea, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(y), d) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sub_mag(sa, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fa), sb, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fb), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), d) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def caseEQ source · line 196 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+sa:Bool -> @+sb:Bool -> @+ea:Nat -> @+Fa:Nat -> @+Fb:Nat -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(x)) == Fa : Nat} -> @+hfb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(y)) == Fb : Nat} -> @+hFa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fa) == True{} : Bool} -> @+hFb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fb) == True{} : Bool} -> @+hlta:{Nat.is_lt(ea, 2047n) == True{} : Bool} -> @+sg:Bool -> @+hsg:{Bool.not(Bool.xor(sa, sb)) == sg : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, sg, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.am_case(x, y, sa, ea, ea, EQ{}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sm_case(x, y, sa, ea, ea, EQ{})) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.add_mag(sa, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fa), sb, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fb), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def core_c source · line 215 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+sa:Bool -> @+sb:Bool -> @+ea:Nat -> @+eb:Nat -> @+Fa:Nat -> @+Fb:Nat -> @+hfa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(x)) == Fa : Nat} -> @+hfb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(y)) == Fb : Nat} -> @+hFa:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fa) == True{} : Bool} -> @+hFb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fb) == True{} : Bool} -> @+hlta:{Nat.is_lt(ea, 2047n) == True{} : Bool} -> @+hltb:{Nat.is_lt(eb, 2047n) == True{} : Bool} -> @+sg:Bool -> @+hsg:{Bool.not(Bool.xor(sa, sb)) == sg : Bool} -> @+c:Cmp -> @+hc:{Nat.cmp(ea, eb) == c : Cmp} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, sg, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.am_case(x, y, sa, ea, eb, c), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sm_case(x, y, sa, ea, eb, c)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.add_mag(sa, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), Nat.min(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb))), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(ea, Fa)), sb, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb), Nat.min(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb))), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(eb, Fb)), Nat.min(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(ea), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(eb))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def afin source · line 232 · raw

@+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+ha:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2047n) == True{} : Bool} -> @+hb:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 2047n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.add_fin(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

F.add on finite operands is the spec's add_fin