~/bend-docscommunity

proofs/math/typed/f64divc.bend checks

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

19 imports
import Base
import ./f64light.bend as FL
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/word.bend as WD
import ./width.bend as WW
import ./natcmp.bend as NC
import ./f64bits.bend as FB
import ./f64cmp.bend as FC
import ./f64round.bend as FR
import ./f64norm.bend as NM
import ./f64mexp.bend as EX
import ./f64divv.bend as DV

Definitions

def v source · line 25 · raw

@+x:U32 -> Nat

def hea source · line 28 · 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 31 · 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 34 · 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 ltf source · line 37 · raw

@+xl:U32 -> @+xh:U32 -> @+h:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2047n) == False{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2047n) == True{} : Bool}

def xl_c source · line 40 · raw

@+E:Nat -> @+h:{Nat.is_lt(E, 2047n) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(E, 0n) == c : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, c, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 1074n), Nat.sub(Nat.add(E, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb), 1075n)), 3971n) == True{} : Bool}

def xexp_le source · line 47 · raw

@+E:Nat -> @+h:{Nat.is_lt(E, 2047n) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 1074n), Nat.sub(Nat.add(E, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb), 1075n)), 3971n) == True{} : Bool}

def nzle source · line 50 · raw

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

def mpos_c source · line 58 · raw

@+sy:Nat -> @+m:Nat -> @+w:Nat -> @+hw:{w == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(sy, m) : Nat} -> @+h52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, w) == False{} : Bool} -> @+z:Bool -> @+hz:{Nat.is_eq(m, 0n) == z : Bool} -> {z == False{} : Bool}

a nonzero finite significand is positive

def yp_eq source · line 67 · raw

@+yl:U32 -> @+yh:U32 -> @+hzy:{Bool.and(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n)) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}) == 1n+Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 1n) : Nat}

def dfin source · line 74 · raw

@+s:Bool -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+hzx:{Bool.and(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n)) == False{} : Bool} -> @+hzy:{Bool.and(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n)) == False{} : Bool} -> @+hax:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2047n) == True{} : Bool} -> @+hay:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 2047n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.div_n(s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.div_fin(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}, s) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

the finite nonzero quotient

def mant0 source · line 89 · raw

@+xl:U32 -> @+xh:U32 -> @+hc:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n) == True{} : Bool} -> @+hb:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) == 0n : Nat}

def zero_v source · line 93 · raw

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

def dz source · line 101 · raw

@+s:Bool -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+hc:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n) == True{} : Bool} -> @+hb:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n) == True{} : Bool} -> @+hzy:{Bool.and(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n)) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zero(s) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.div_fin(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}, s) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

zero divided by a nonzero finite double

def dimpl source · line 106 · raw

@+s:Bool -> @+a1:Bool -> @+b1:Bool -> @+c1:Bool -> @+a2:Bool -> @+b2:Bool -> @+c2:Bool -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def dspec source · line 109 · raw

@+s:Bool -> @+a1:Bool -> @+b1:Bool -> @+c1:Bool -> @+a2:Bool -> @+b2:Bool -> @+c2:Bool -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def ion source · line 112 · raw

@+s:Bool -> @+b:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.inf_or_nan(s, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, b, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.inf(s)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def non source · line 119 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan_or(x, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, b, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan, x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def dsh4 source · line 122 · raw

@+s:Bool -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+z:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.div_za(s, ea, fa, eb, fb, z) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, z, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zero(s), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.div_n(s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(ea, fa), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(ea, fa), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(eb, fb), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(eb, fb))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def dsh3 source · line 129 · raw

@+s:Bool -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+z:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.div_z(s, ea, fa, eb, fb, z) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, z, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.and(Nat.is_eq(ea, 0n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(fa)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.inf(s)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.and(Nat.is_eq(ea, 0n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(fa)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zero(s), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.div_n(s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(ea, fa), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(ea, fa), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(eb, fb), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(eb, fb)))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def dsh2 source · line 136 · raw

@+s:Bool -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.div_b(s, ea, fa, eb, fb, t) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, t, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(fb)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zero(s)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.and(Nat.is_eq(eb, 0n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(fb)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.and(Nat.is_eq(ea, 0n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(fa)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.inf(s)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.and(Nat.is_eq(ea, 0n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(fa)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zero(s), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.div_n(s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(ea, fa), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(ea, fa), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(eb, fb), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(eb, fb))))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def dsh1 source · line 143 · raw

@+s:Bool -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.div_cls(s, ea, fa, eb, fb, t) == dimpl(s, t, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(fa), Nat.is_eq(ea, 0n), Nat.is_eq(eb, 2047n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(fb), Nat.is_eq(eb, 0n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.div_n(s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(ea, fa), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(ea, fa), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(eb, fb), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(eb, fb))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def dcase source · line 150 · raw

@+s:Bool -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+r1:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+r2:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+a1:Bool -> @+b1:Bool -> @+c1:Bool -> @+a2:Bool -> @+b2:Bool -> @+c2:Bool -> @+hR:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.or(Bool.or(a1, a2), Bool.or(Bool.and(c1, b1), Bool.and(c2, b2))), r2, r1) == r2 : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64} -> @+hZ:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.or(Bool.or(a1, a2), Bool.or(Bool.not(Bool.and(c1, b1)), Bool.and(c2, b2))), r2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zero(s)) == r2 : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64} -> {dimpl(s, a1, b1, c1, a2, b2, c2, r1) == dspec(s, a1, b1, c1, a2, b2, c2, r2) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def dswap source · line 281 · raw

@+s1:Bool -> @+s2:Bool -> @+hs:{s1 == s2 : Bool} -> @+r1:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+r2:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hr:{r1 == r2 : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64} -> @+p1:Bool -> @+q1:Bool -> @+h0:{p1 == q1 : Bool} -> @+p2:Bool -> @+q2:Bool -> @+h1:{p2 == q2 : Bool} -> @+p3:Bool -> @+q3:Bool -> @+h2:{p3 == q3 : Bool} -> @+p4:Bool -> @+q4:Bool -> @+h3:{p4 == q4 : Bool} -> @+p5:Bool -> @+q5:Bool -> @+h4:{p5 == q5 : Bool} -> @+p6:Bool -> @+q6:Bool -> @+h5:{p6 == q6 : Bool} -> {dimpl(s1, p1, p2, p3, p4, p5, p6, r1) == dimpl(s2, q1, q2, q3, q4, q5, q6, r2) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def dkR_c source · line 284 · raw

@+s:Bool -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+g:Bool -> @+hg:{Bool.or(Bool.or(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2047n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 2047n)), Bool.or(Bool.and(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n)), Bool.and(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n)))) == g : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, g, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.div_fin(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}, s), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.div_n(s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh})))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.div_fin(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}, s) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def dkZ_c source · line 293 · raw

@+s:Bool -> @+xl:U32 -> @+xh:U32 -> @+yl:U32 -> @+yh:U32 -> @+g:Bool -> @+hg:{Bool.or(Bool.or(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2047n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 2047n)), Bool.or(Bool.not(Bool.and(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n))), Bool.and(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}), 0n)))) == g : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, g, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.div_fin(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}, s), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zero(s)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.div_fin(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{yl, yh}, s) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def div_value source · line 302 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Div.value(x, y)