proofs/math/typed/f64modf.bend checks
raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64modf.bend as F64modf
18 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 ./f64bits.bend as FB import ./f64light.bend as FL import ./f64round.bend as FR import ./f64tools.bend as T import ./f64rint.bend as RI
Definitions
def rem_v source · line 27 · raw
@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @+hb:{Nat.is_lt(k, 64n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(w, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr(w, k), k))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)) : Nat}the low k bits of a word, k < 64
def mfr_c source · line 43 · raw
@+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+u:Nat -> @+hu:{Nat.is_le(63n, u) == True{} : Bool} -> @+k:Nat -> @+b:Bool -> @+hb:{Nat.is_lt(k, 64n) == b : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mf_frac(s, w, u, k, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(w)), u) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def FRAC source · line 53 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64
def frac_v source · line 56 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mf_frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.signbit(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dmant(x), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x), Nat.sub(3000n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x)), Nat.is_lt(Nat.sub(3000n, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.dexp(x)), 64n)) == FRAC(x) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def zs source · line 67 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.signbit(x)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}
def mff_c source · line 70 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+c:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mf_fin(x, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pickt(Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64), c, (0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x)), x), (FRAC(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.to_integral(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Trunc{}, x))) : Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64)}
def mf_c source · line 80 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+t:Bool -> @+z:Bool -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(x)) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mf_cls(x, t) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pickt(Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64), Bool.and(t, Bool.not(z)), (0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.qnan, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.qnan), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pickt(Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64), Bool.or(Bool.and(t, z), Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x))), (0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(x)), x), (FRAC(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.to_integral(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Trunc{}, x)))) : Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64)}
def modf_value source · line 91 · raw
@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Modf.value(x)