~/bend-docscommunity

proofs/math/typed/f64mexp.bend checks

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

20 imports
import Base
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 ./w64mul.bend as W64M
import ./natfuel.bend as NF
import ./u32laws.bend as LW
import ./w64clz.bend as CLZ
import ../../lib/u32half.bend as UH
import ../../lib/u32alg.bend as A
import ./f64cmp.bend as FC
import ./f64round.bend as FR
import ./f64rtools.bend as RT
import ./f64norm.bend as NM

Definitions

def sa_le source · line 30 · raw

@+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64norm.sa(ea, fa), 53n) == True{} : Bool}

def e_ge1 source · line 38 · raw

@+E:Nat -> @+h:{Nat.is_eq(E, 0n) == False{} : Bool} -> {Nat.is_le(1926n, Nat.add(1925n, E)) == True{} : Bool}

def xg_c source · line 45 · raw

@+E:Nat -> @+c:Bool -> @+hc:{Nat.is_eq(E, 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(E, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb), 1075n))) == True{} : Bool}

def xexp_ge source · line 52 · raw

@+E:Nat -> {Nat.is_le(1926n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 1074n), Nat.sub(Nat.add(E, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb), 1075n))) == True{} : Bool}

def eg source · line 55 · raw

@+ea:Nat -> @+sa:Nat -> @+Xx:Nat -> @+n2:{Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat} -> @+hs:{Nat.is_le(sa, 53n) == True{} : Bool} -> @+hX:{Nat.is_le(1926n, Xx) == True{} : Bool} -> {Nat.is_le(4044n, ea) == True{} : Bool}

def s_ge source · line 60 · raw

@+ea:Nat -> @+eb:Nat -> @+sa:Nat -> @+sb:Nat -> @+Xx:Nat -> @+Xy:Nat -> @+n2x:{Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat} -> @+n2y:{Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat} -> @+hsa:{Nat.is_le(sa, 53n) == True{} : Bool} -> @+hsb:{Nat.is_le(sb, 53n) == True{} : Bool} -> @+hXx:{Nat.is_le(1926n, Xx) == True{} : Bool} -> @+hXy:{Nat.is_le(1926n, Xy) == True{} : Bool} -> {Nat.is_le(8088n, Nat.add(ea, eb)) == True{} : Bool}

def e0_ge source · line 65 · raw

@+ea:Nat -> @+eb:Nat -> @+sa:Nat -> @+sb:Nat -> @+Xx:Nat -> @+Xy:Nat -> @+n2x:{Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat} -> @+n2y:{Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat} -> @+hsa:{Nat.is_le(sa, 53n) == True{} : Bool} -> @+hsb:{Nat.is_le(sb, 53n) == True{} : Bool} -> @+hXx:{Nat.is_le(1926n, Xx) == True{} : Bool} -> @+hXy:{Nat.is_le(1926n, Xy) == True{} : Bool} -> {Nat.is_le(2244n, Nat.sub(Nat.add(ea, eb), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, 1023n))) == True{} : Bool}

def x_eq source · line 68 · raw

@+ea:Nat -> @+eb:Nat -> @+sa:Nat -> @+sb:Nat -> @+Xx:Nat -> @+Xy:Nat -> @+n2x:{Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat} -> @+n2y:{Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat} -> @+hsa:{Nat.is_le(sa, 53n) == True{} : Bool} -> @+hsb:{Nat.is_le(sb, 53n) == True{} : Bool} -> @+hXx:{Nat.is_le(1926n, Xx) == True{} : Bool} -> @+hXy:{Nat.is_le(1926n, Xy) == True{} : Bool} -> {Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, 1023n)), 2180n), 2180n) == Nat.sub(Nat.add(ea, eb), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, 1023n)) : Nat}

def x_ge source · line 72 · raw

@+ea:Nat -> @+eb:Nat -> @+sa:Nat -> @+sb:Nat -> @+Xx:Nat -> @+Xy:Nat -> @+n2x:{Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat} -> @+n2y:{Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat} -> @+hsa:{Nat.is_le(sa, 53n) == True{} : Bool} -> @+hsb:{Nat.is_le(sb, 53n) == True{} : Bool} -> @+hXx:{Nat.is_le(1926n, Xx) == True{} : Bool} -> @+hXy:{Nat.is_le(1926n, Xy) == True{} : Bool} -> {Nat.is_le(64n, Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, 1023n)), 2180n)) == True{} : Bool}

def x0_eq source · line 75 · raw

@+ea:Nat -> @+eb:Nat -> @+sa:Nat -> @+sb:Nat -> @+Xx:Nat -> @+Xy:Nat -> @+n2x:{Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat} -> @+n2y:{Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat} -> @+hsa:{Nat.is_le(sa, 53n) == True{} : Bool} -> @+hsb:{Nat.is_le(sb, 53n) == True{} : Bool} -> @+hXx:{Nat.is_le(1926n, Xx) == True{} : Bool} -> @+hXy:{Nat.is_le(1926n, Xy) == True{} : Bool} -> {Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, 1023n)), 2180n), 64n), 64n) == Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, 1023n)), 2180n) : Nat}

def mexp source · line 79 · raw

@+ea:Nat -> @+eb:Nat -> @+sa:Nat -> @+sb:Nat -> @+Xx:Nat -> @+Xy:Nat -> @+n2x:{Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat} -> @+n2y:{Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat} -> @+hsa:{Nat.is_le(sa, 53n) == True{} : Bool} -> @+hsb:{Nat.is_le(sb, 53n) == True{} : Bool} -> @+hXx:{Nat.is_le(1926n, Xx) == True{} : Bool} -> @+hXy:{Nat.is_le(1926n, Xy) == True{} : Bool} -> {Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, 1023n)), 2180n), 64n), 21n), Nat.add(sa, sb)) == Nat.sub(Nat.add(Xx, Xy), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb) : Nat}

x0 + 21 + sa + sb is the spec's product exponent