proofs/math/typed/f64next.bend checks
raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend as F64next
21 imports
import Base import ../../../spec/lib/common.bend as C import ../../../spec/math/f64.bend as SF import ../../../spec/math/w64.bend as SW import ../../../src/math/f64.bend as F import ../../../src/math/w64.bend as X import ../../../src/math/u64.bend as WU import ../../lib/nat.bend as N import ../../lib/logic.bend as L import ../../lib/lemmas/proofs/nat_algebra.bend as NA import ./width.bend as WW import ./w64add.bend as WA import ./w64sh.bend as SH import ./u32laws.bend as LW import ../../lib/word.bend as WD import ./f64bits.bend as FB import ./f64light.bend as FL import ./f64round.bend as FR import ./f64rtools.bend as RT import ./f64cmp.bend as FC import ./f64tools.bend as T
Definitions
def v source · line 31 · raw
@+x:U32 -> Nat
def non source · line 34 · raw
@+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan_or(y, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, b, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.qnan, y) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def fpk source · line 41 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fpick(x, y, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, b, x, y) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def ltc source · line 49 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+u:{Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(y)) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.lt(x, y) == Cmp.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.ord(x, y)) : Bool}the comparisons when neither operand is NaN
def eqc source · line 52 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+u:{Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(y)) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.eq(x, y) == Cmp.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.ord(x, y)) : Bool}
def or_ff source · line 55 · raw
@+a:Bool -> @+b:Bool -> @+ha:{a == False{} : Bool} -> @+hb:{b == False{} : Bool} -> {Bool.or(a, b) == False{} : Bool}
def zeros_v source · line 58 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zeros(x, y) == Bool.and(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(y)) : Bool}
def zsg source · line 61 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+and_:Bool -> Bool
def fmin_z_c source · line 66 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(x) == False{} : Bool} -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(y) == False{} : Bool} -> @+zz:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fmin_z(x, y, zz) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, zz, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(y))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Cmp.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.ord(x, y)), x, y)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def fmax_z_c source · line 77 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(x) == False{} : Bool} -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(y) == False{} : Bool} -> @+zz:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fmax_z(x, y, zz) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, zz, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(Bool.and(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(y))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Cmp.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.ord(y, x)), x, y)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def fmin_ny_c source · line 88 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(x) == False{} : Bool} -> @+b:Bool -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(y) == b : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fmin_ny(x, y, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, b, x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.and(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(y)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(y))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Cmp.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.ord(x, y)), x, y))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def fmax_ny_c source · line 97 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(x) == False{} : Bool} -> @+b:Bool -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(y) == b : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fmax_ny(x, y, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, b, x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.and(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(y)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(Bool.and(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(y))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Cmp.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.ord(y, x)), x, y))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def fmin_nx_c source · line 106 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+a:Bool -> @+ha:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(x) == a : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fmin_nx(x, y, a) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.qnan, y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(y), x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.and(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(y)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(y))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Cmp.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.ord(x, y)), x, y)))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def fmax_nx_c source · line 114 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+a:Bool -> @+ha:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(x) == a : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.fmax_nx(x, y, a) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.qnan, y), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(y), x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.and(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(y)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(Bool.and(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(y))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Cmp.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.ord(y, x)), x, y)))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def fmin_value source · line 122 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Fmin.value(x, y)
def fmax_value source · line 125 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Fmax.value(x, y)
def notinj source · line 130 · raw
@+a:Bool -> @+b:Bool -> @+h:{Bool.not(a) == Bool.not(b) : Bool} -> {a == b : Bool}
def iik_t source · line 141 · raw
@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @+hb:{Nat.is_lt(k, 64n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.eq(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr(w, k), k), w) == Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)), 0n) : Bool}
def iik_c source · line 146 · raw
@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @+b:Bool -> @+hb:{Nat.is_lt(k, 64n) == b : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ii_k(w, k, b) == Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)), 0n) : Bool}
def LZ source · line 155 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Bool
def iif_c source · line 158 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+c:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ii_fin(x, c) == Bool.or(c, LZ(x)) : Bool}
def is_integer_value source · line 169 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.IsInteger.value(x)
def sub_le_self source · line 181 · raw
@+a:Nat -> @+b:Nat -> {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}
def magval source · line 192 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mag(x)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pat(x) : Nat}
def patfit source · line 197 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pat(x)) == True{} : Bool}
def frac52 source · line 202 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(x)) == True{} : Bool}
def patz source · line 207 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pat(x), 0n) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x) : Bool}
def per1 source · line 211 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pat(x), 1n) == Nat.add(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(x), 1n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x))) : Nat}pat + 1 still fits 63 bits unless x is a NaN
def p1_c source · line 219 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hn:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(x) == False{} : Bool} -> @+b:Bool -> @+hb:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(x), 2047n) == b : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pat(x), 1n)) == True{} : Bool}
def ws_o source · line 253 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.with_sign(s, w) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64round.bits(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}a word of value n < 2^63 with the sign bit added is bits(s, n)
2^32 stays one shifted: the checker never builds the closed 2^32
def ws source · line 281 · raw
@+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.with_sign(s, w) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64round.bits(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def opat source · line 284 · raw
@+s:Bool -> @+P:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.of_pat(s, P) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64round.bits(s, P) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def step_fin source · line 287 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+W:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+P2:Nat -> @+ev:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(W) == P2 : Nat} -> @+h63:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(63n, P2) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.with_sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.signbit(x), W) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.of_pat(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), P2) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def st_c source · line 295 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hn:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(x) == False{} : Bool} -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x) == False{} : Bool} -> @+up:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.na_step(x, up) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.of_pat(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, up, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pat(x), 1n), Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pat(x), 1n))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def bs0 source · line 316 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+c:U32 -> @+hc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 31n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{U32.from_nat(1n), U32.from_nat(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(31n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, s, one, 0n)))} == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(U32, s, c, 0)} : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}from a zero: the smallest subnormal with y's sign
def bsg source · line 323 · raw
@+s:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64round.bits(s, 1n) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{1, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sgn(s)} : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def nz0 source · line 329 · raw
@+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{1, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sgn(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.signbit(y))} == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(y), 0n, 1n) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def STEP source · line 336 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64
def nzc source · line 339 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hu:{Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(y)) == False{} : Bool} -> @+iz:Bool -> @+hiz:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x) == iz : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.na_z(x, y, iz) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, iz, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(y), 0n, 1n), STEP(x, y)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def neq_c source · line 351 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+hu:{Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(y)) == False{} : Bool} -> @+e:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.na_eq(x, y, e) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, e, y, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(y), 0n, 1n), STEP(x, y))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def na_c source · line 359 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+u:Bool -> @+hu:{Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_nan(y)) == u : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.na_nan(x, y, u) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.not(Bool.not(u)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.qnan, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Cmp.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.ord(x, y)), y, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_zero(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.encode(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(y), 0n, 1n), STEP(x, y)))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def nextafter_value source · line 368 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Nextafter.value(x, y)