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