~/bend-docscommunity

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)