proofs/math/typed/f64bl.bend checks

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

15 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
import ../../../src/math/f64.bend as F
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/u32.bend as U
import ../natural/bits.bend as BT
import ./width.bend as WW
import ./u32laws.bend as LW
import ./w64add.bend as WA
import ./w64sh.bend as SH
import ./natcmp.bend as NC

Definitions

def v source · line 19 · raw

@+x:U32 -> Nat

def lbits source · line 22 · raw

@+k:Nat -> @+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.low_bits(k, n) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, n) : Nat}

def hbits source · line 32 · raw

@+k:Nat -> @+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.high_bits(k, n) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, n) : Nat}

def wval source · line 39 · raw

@+n:Nat -> @+h64:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{U32.from_nat(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.low_bits(32n, n)), U32.from_nat(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.high_bits(32n, n))}) == n : Nat}

def bl_le_n source · line 46 · raw

@+K:Nat -> @+n:Nat -> @+hn:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(K, n) == True{} : Bool} -> @+hp:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(1n+K), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n))) == True{} : Bool} -> {False{} == True{} : Bool}

def bl_le source · line 57 · raw

@+K:Nat -> @+n:Nat -> @+hn:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(K, n) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n), K) == c : Bool} -> {c == True{} : Bool}

def bl_pos source · line 67 · raw

@+n:Nat -> @+hz:{Nat.is_eq(n, 0n) == False{} : Bool} -> @+c:Nat -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n) == c : Nat} -> {Nat.is_le(1n, c) == True{} : Bool}

def dle source · line 76 · raw

@+a:Nat -> @+c:Nat -> @+h:{Nat.is_le(Nat.double(a), Nat.double(c)) == True{} : Bool} -> {Nat.is_le(a, c) == True{} : Bool}

def lower source · line 79 · raw

@+n:Nat -> @+hz:{Nat.is_eq(n, 0n) == False{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n), 1n)), n) == True{} : Bool}