proofs/math/typed/f64fmod.bend checks
raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend as F64fmod
27 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 ../../lib/lemmas/proofs/natural_division.bend as ND import ../natural/misc.bend as MS import ./width.bend as WW import ./w64add.bend as WA import ./w64sh.bend as SH import ./w64dmrem.bend as DR import ./w64dmtop.bend as DQ import ./f64bits.bend as FB import ./f64light.bend as FL import ./f64round.bend as FR import ./f64rtools.bend as RT import ./f64adda.bend as AA import ./f64cmp.bend as FC import ./f64bl.bend as BL import ./f64tools.bend as T import ./f64exp.bend as EX
Definitions
def mod_mul_add source · line 40 · raw
@+q:Nat -> @+bp:Nat -> @+y:Nat -> {Nat.mod(Nat.add(Nat.mul(q, 1n+bp), y), 1n+bp) == Nat.mod(y, 1n+bp) : Nat}
def div_mul_add source · line 51 · raw
@+q:Nat -> @+bp:Nat -> @+y:Nat -> {Nat.div(Nat.add(Nat.mul(q, 1n+bp), y), 1n+bp) == Nat.add(q, Nat.div(y, 1n+bp)) : Nat}
def shq source · line 63 · raw
@+N0:Nat -> @+bp:Nat -> @+t:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(t, N0) == Nat.add(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(t, Nat.div(N0, 1n+bp)), 1n+bp), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(t, Nat.mod(N0, 1n+bp))) : Nat}N 2^t = (Q 2^t) B + r 2^t for N = Q B + r
def mod_shift source · line 72 · raw
@+N0:Nat -> @+bp:Nat -> @+t:Nat -> {Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(t, Nat.mod(N0, 1n+bp)), 1n+bp) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(t, N0), 1n+bp) : Nat}
def par_shift source · line 78 · raw
@+N0:Nat -> @+bp:Nat -> @+p:Nat -> {Nat.mod(Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+p, Nat.mod(N0, 1n+bp)), 1n+bp), 2n) == Nat.mod(Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+p, N0), 1n+bp), 2n) : Nat}the quotient's parity after at least one more bit
def min_le_r source · line 90 · raw
@+a:Nat -> @+b:Nat -> {Nat.is_le(Nat.min(a, b), b) == True{} : Bool}
def min_le_l source · line 99 · raw
@+a:Nat -> @+b:Nat -> {Nat.is_le(Nat.min(a, b), a) == True{} : Bool}
def rfit source · line 110 · raw
@+bp:Nat -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 1n+bp) == True{} : Bool} -> @+rw:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+N0:Nat -> @+hr:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(rw) == Nat.mod(N0, 1n+bp) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(rw)) == True{} : Bool}
def shl_t source · line 114 · raw
@+rw:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Nat -> @+ht:{Nat.is_le(t, 10n) == True{} : Bool} -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(rw)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(rw, t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(t, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(rw)) : Nat}
def step_r source · line 119 · raw
@+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+bp:Nat -> @+eB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b) == 1n+bp : Nat} -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 1n+bp) == True{} : Bool} -> @+hbz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(b) == False{} : Bool} -> @+rw:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+N0:Nat -> @+t:Nat -> @+ht:{Nat.is_le(t, 10n) == True{} : Bool} -> @+hr:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(rw) == Nat.mod(N0, 1n+bp) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.divmod(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(rw, t), b))) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(t, N0), 1n+bp) : Nat}
def step_q source · line 132 · raw
@+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+bp:Nat -> @+eB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b) == 1n+bp : Nat} -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 1n+bp) == True{} : Bool} -> @+hbz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(b) == False{} : Bool} -> @+rw:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+N0:Nat -> @+p:Nat -> @+ht:{Nat.is_le(1n+p, 10n) == True{} : Bool} -> @+hr:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(rw) == Nat.mod(N0, 1n+bp) : Nat} -> {Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.divmod(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(rw, 1n+p), b))), 2n) == Nat.mod(Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+p, N0), 1n+bp), 2n) : Nat}
def shc source · line 147 · raw
@+e:Nat -> @+t:Nat -> @+N0:Nat -> @+h:{Nat.is_le(t, 1n+e) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(1n+e, t), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(t, N0)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+e, N0) : Nat}
def eta source · line 151 · raw
@p:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64) -> {p == (0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(p), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(p)) : Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64)}
def loop_r source · line 156 · raw
@fuel:Nat -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+bp:Nat -> @+eB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b) == 1n+bp : Nat} -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 1n+bp) == True{} : Bool} -> @+hbz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(b) == False{} : Bool} -> @+d:Nat -> @+hd:{Nat.is_le(d, fuel) == True{} : Bool} -> @+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+N0:Nat -> @+hr:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r) == Nat.mod(N0, 1n+bp) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fm_go(fuel, b, d, (q, r)))) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(d, N0), 1n+bp) : Nat}
def loop_q source · line 174 · raw
@fuel:Nat -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+bp:Nat -> @+eB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b) == 1n+bp : Nat} -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 1n+bp) == True{} : Bool} -> @+hbz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(b) == False{} : Bool} -> @+d:Nat -> @+hd:{Nat.is_le(d, fuel) == True{} : Bool} -> @+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+N0:Nat -> @+hr:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r) == Nat.mod(N0, 1n+bp) : Nat} -> @+hq:{Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(q), 2n) == Nat.mod(Nat.div(N0, 1n+bp), 2n) : Nat} -> {Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fm_go(fuel, b, d, (q, r)))), 2n) == Nat.mod(Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(d, N0), 1n+bp), 2n) : Nat}
def v source · line 195 · raw
@+x:U32 -> Nat
def dec source · line 198 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {x == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(x)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def ru_self source · line 215 · raw
@+s:Bool -> @+Fr:Nat -> @+u:Nat -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fr) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round_u(s, Fr, u, u) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(s, 0n, Fr) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}a significand of at most 52 bits at its own ulp u encodes as a subnormal; u stays abstract, so pack's exponent arithmetic is never evaluated on a literal (rt_sub instantiates u = 1926)
def rt_sub source · line 229 · raw
@+s:Bool -> @+Fr:Nat -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fr) == True{} : Bool} -> @+z:Bool -> @+hz:{Nat.is_eq(Fr, 0n) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Fr, 1926n) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(s, 0n, Fr) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def rt_norm source · line 248 · raw
@+s:Bool -> @+E:Nat -> @+Fr:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+hE0:{Nat.is_eq(E, 0n) == False{} : Bool} -> @+hE:{Nat.is_lt(E, 2047n) == True{} : Bool} -> @+hF:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fr) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.add(Fr, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one)), Nat.add(1925n, E)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(s, E, Fr) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def frac52 source · line 278 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(x)) == True{} : Bool}
def rt_c source · line 283 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hfin:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x), 2047n) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+z:Bool -> @+hz:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x), 0n) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x)) == x : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def rt source · line 310 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hfin:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x), 2047n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x)) == x : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def fin source · line 315 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hn:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(x) == False{} : Bool} -> @+hi:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_inf(x) == False{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x), 2047n) == True{} : Bool}
def mod_small source · line 320 · raw
@+a:Nat -> @+n:Nat -> @+h:{Nat.is_lt(a, n) == True{} : Bool} -> {Nat.mod(a, n) == a : Nat}
def div_small source · line 327 · raw
@+a:Nat -> @+n:Nat -> @+h:{Nat.is_lt(a, n) == True{} : Bool} -> {Nat.div(a, n) == 0n : Nat}
def xge_c source · line 334 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+c:Bool -> @+hc:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x), 0n) == c : Bool} -> {Nat.is_le(1926n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, c, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 1074n), Nat.sub(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb), 1075n))) == True{} : Bool}
def xge source · line 341 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {Nat.is_le(1926n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x)) == True{} : Bool}
def yn_c source · line 345 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hlt:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(y), 0n) == c : Bool} -> {c == False{} : Bool}a scale above another double's is a normal number's
def nf52 source · line 354 · raw
@+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hz:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(y), 0n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(y)) == False{} : Bool}
def far_lt source · line 358 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hlt:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y)) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(y))) == True{} : Bool}y's significand moved up by k >= 1 is at least 2^53 > mant(x)
def FM source · line 370 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64
def fm_far source · line 374 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hlt:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y)) == True{} : Bool} -> @+hfin:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x), 2047n) == True{} : Bool} -> {FM(x, y) == x : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}the spec's operands when x has the smaller scale
def fm_zero source · line 389 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hzx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x) == True{} : Bool} -> @+hzy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(y) == False{} : Bool} -> @+hfin:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x), 2047n) == True{} : Bool} -> {FM(x, y) == x : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}a zero x
def bpv source · line 408 · raw
@+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Nat
def ynz source · line 411 · raw
@+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hzy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(y) == False{} : Bool} -> {Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(y)), 0n) == False{} : Bool}
def eBy source · line 414 · raw
@+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hzy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(y) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(y)) == 1n+bpv(y) : Nat}
def hbzy source · line 417 · raw
@+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hzy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(y) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(y)) == False{} : Bool}
def hBy source · line 420 · raw
@+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hzy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(y) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 1n+bpv(y)) == True{} : Bool}
def DD source · line 423 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Nat
def qr_r source · line 426 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hzy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(y) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fm_qr(x, y))) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(DD(x, y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(x))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(y))) : Nat}
def qr_q source · line 438 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hzy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(y) == False{} : Bool} -> {Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fm_qr(x, y))), 2n) == Nat.mod(Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(DD(x, y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(x))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(y))), 2n) : Nat}
def NRd source · line 453 · raw
@+s:Bool -> @+a:Nat -> @+b:Nat -> @+m1:Nat -> @+m2:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64
def fm_spec_near source · line 457 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hge:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y)) == False{} : Bool} -> {FM(x, y) == NRd(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(y)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}FM when y has the smaller (or equal) scale
def nrd_v source · line 467 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {NRd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.signbit(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(y))) == NRd(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(y)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def xlt source · line 480 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:Bool -> @+h:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(y)) == b : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y)) == b : Bool}
def fm_near source · line 484 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hzy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(y) == False{} : Bool} -> @+hge:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(y)) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.round_w(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.signbit(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fm_qr(x, y))) == FM(x, y) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def nn source · line 495 · raw
@+b:Bool -> {Bool.not(Bool.not(b)) == b : Bool}
def badv source · line 502 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {Bool.or(Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.unordered(x, y), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.is_inf(x)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.is_zero(y)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rbad(x, y) : Bool}
def ok_zy source · line 516 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rbad(x, y) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(y) == False{} : Bool}what a false rbad says
def ok_ix source · line 519 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rbad(x, y) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_inf(x) == False{} : Bool}
def ok_u source · line 522 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rbad(x, y) == False{} : Bool} -> {Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(y)) == False{} : Bool}
def ok_fin source · line 526 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rbad(x, y) == False{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x), 2047n) == True{} : Bool}
def ff_c source · line 529 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rbad(x, y) == False{} : Bool} -> @+far:Bool -> @+hfar:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(y)) == far : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fmod_fin(x, y, far) == FM(x, y) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def fz_c source · line 536 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rbad(x, y) == False{} : Bool} -> @+zx:Bool -> @+hzx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x) == zx : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fmod_z(x, y, zx) == FM(x, y) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def fyi_c source · line 543 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rbad(x, y) == False{} : Bool} -> @+yi:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fmod_yi(x, y, yi) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, yi, x, FM(x, y)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def fb_c source · line 550 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+bad:Bool -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rbad(x, y) == bad : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fmod_bad(x, y, bad) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, bad, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.qnan, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_inf(y), x, FM(x, y))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def fmod_value source · line 557 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Fmod.value(x, y)
def addrr source · line 563 · raw
@+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Rv:Nat -> @+er:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r) == Rv : Nat} -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, Rv) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(r, r)) == Nat.add(Rv, Rv) : Nat}
def rmp_c source · line 569 · raw
@+s:Bool -> @+u:Nat -> @+hu:{Nat.is_le(63n, u) == True{} : Bool} -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Bv:Nat -> @+Rv:Nat -> @+eb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b) == Bv : Nat} -> @+er:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r) == Rv : Nat} -> @+hRB:{Nat.is_le(Rv, Bv) == True{} : Bool} -> @+c:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rm_pick(s, u, b, r, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, c, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(Bool.not(s), Nat.sub(Bv, Rv), u), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Rv, u)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def rmfix_v source · line 579 · raw
@+s:Bool -> @+u:Nat -> @+hu:{Nat.is_le(63n, u) == True{} : Bool} -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Bv:Nat -> @+Rv:Nat -> @+Qv:Nat -> @+eb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b) == Bv : Nat} -> @+er:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(r) == Rv : Nat} -> @+hq:{Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(q), 2n) == Nat.mod(Qv, 2n) : Nat} -> @+hRB:{Nat.is_le(Rv, Bv) == True{} : Bool} -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, Rv) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rm_fix(s, u, b, r, q) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rnear(s, Rv, Bv, Qv, u) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}rm_fix on words is the spec's rnear on their values
def RNs source · line 593 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64
def RNd source · line 596 · raw
@+s:Bool -> @+a:Nat -> @+b:Nat -> @+m1:Nat -> @+m2:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64
def rn_spec_near source · line 599 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hge:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y)) == False{} : Bool} -> {RNs(x, y) == RNd(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(y)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def rnd_v source · line 610 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {RNd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.signbit(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(y))) == RNd(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(y)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def modlt source · line 623 · raw
@+n:Nat -> @+V:Nat -> @+hne:{Nat.is_eq(V, 0n) == False{} : Bool} -> {Nat.is_lt(Nat.mod(n, V), V) == True{} : Bool}
def rm_near_c source · line 630 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hzy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(y) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rm_qr(x, y, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fm_qr(x, y)) == RNd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.signbit(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(y))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def rn_spec_far source · line 641 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hlt:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y)) == True{} : Bool} -> {RNs(x, y) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rnear(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(y)), 0n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def xsub source · line 658 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x)) == Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x)) : Nat}
def rm_one source · line 662 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hlt:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y)) == True{} : Bool} -> @+hk:{Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x)) == 1n : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rm_fix(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.signbit(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(y), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(y)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, 0}) == RNs(x, y) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}exactly one scale step below y
def two_le source · line 684 · raw
@+k:Nat -> @+h1:{Nat.is_le(1n, k) == True{} : Bool} -> @+h2:{Nat.is_eq(k, 1n) == False{} : Bool} -> {Nat.is_le(2n, k) == True{} : Bool}
def big54 source · line 693 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hlt:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y)) == True{} : Bool} -> @+hk:{Nat.is_eq(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x)), 1n) == False{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(y)), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(x))) == False{} : Bool}
def or_ff source · line 706 · raw
@+a:Bool -> @+b:Bool -> @+ha:{a == False{} : Bool} -> @+hb:{b == False{} : Bool} -> {Bool.or(a, b) == False{} : Bool}
def rm_many source · line 710 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hlt:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y)) == True{} : Bool} -> @+hk:{Nat.is_eq(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x)), 1n) == False{} : Bool} -> @+hfin:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x), 2047n) == True{} : Bool} -> {RNs(x, y) == x : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}two or more scale steps below y: x itself
def rm_zero source · line 721 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hzx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x) == True{} : Bool} -> @+hzy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(y) == False{} : Bool} -> @+hfin:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x), 2047n) == True{} : Bool} -> {RNs(x, y) == x : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def rone_c source · line 744 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rbad(x, y) == False{} : Bool} -> @+hlt:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(y)) == True{} : Bool} -> @+o:Bool -> @+ho:{Nat.is_eq(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(y), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x)), 1n) == o : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rm_near(x, y, o) == RNs(x, y) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def rfar_c source · line 751 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rbad(x, y) == False{} : Bool} -> @+far:Bool -> @+hfar:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(y)) == far : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rm_far(x, y, far) == RNs(x, y) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def rz_c source · line 760 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rbad(x, y) == False{} : Bool} -> @+zx:Bool -> @+hzx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x) == zx : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rm_z(x, y, zx) == RNs(x, y) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def ryi_c source · line 767 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rbad(x, y) == False{} : Bool} -> @+yi:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rm_yi(x, y, yi) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, yi, x, RNs(x, y)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def rb_c source · line 774 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+bad:Bool -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rbad(x, y) == bad : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rm_bad(x, y, bad) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, bad, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.qnan, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_inf(y), x, RNs(x, y))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def remainder_value source · line 781 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Remainder.value(x, y)