~/bend-docscommunity

proofs/math/typed/f64addh.bend checks

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

12 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 ./f64adda.bend as AA
import ./f64addb.bend as AB
import ./f64addg.bend as AG

Definitions

def bigA_c source · line 17 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+el:Nat -> @+fl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+es:Nat -> @+fs:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Fl:Nat -> @+Fs:Nat -> @+hfl:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fl) == Fl : Nat} -> @+hfs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fs) == Fs : Nat} -> @+hFl:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fl) == True{} : Bool} -> @+hFs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fs) == True{} : Bool} -> @+hlt:{Nat.is_lt(es, el) == True{} : Bool} -> @+z:Bool -> @+hz:{Nat.is_eq(es, 0n) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rp62(s, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, el), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, 536870912}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fl, 9n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr_jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.am_small(es, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fs, 9n)), Nat.sub(el, es)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(es, Fs), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(el), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(es)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(el, Fl))), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(es)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def bigA source · line 46 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+el:Nat -> @+fl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+es:Nat -> @+fs:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Fl:Nat -> @+Fs:Nat -> @+hfl:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fl) == Fl : Nat} -> @+hfs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fs) == Fs : Nat} -> @+hFl:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fl) == True{} : Bool} -> @+hFs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fs) == True{} : Bool} -> @+hlt:{Nat.is_lt(es, el) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.rp62(s, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, el), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, 536870912}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fl, 9n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr_jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.am_small(es, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fs, 9n)), Nat.sub(el, es)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(es, Fs), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(el), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(es)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(el, Fl))), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(es)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def bigS_c source · line 49 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+el:Nat -> @+fl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+es:Nat -> @+fs:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Fl:Nat -> @+Fs:Nat -> @+hfl:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fl) == Fl : Nat} -> @+hfs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fs) == Fs : Nat} -> @+hFl:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fl) == True{} : Bool} -> @+hFs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fs) == True{} : Bool} -> @+hlt:{Nat.is_lt(es, el) == True{} : Bool} -> @+z:Bool -> @+hz:{Nat.is_eq(es, 0n) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_round_pack(s, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, Nat.sub(el, 1n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fl, 10n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, 1073741824}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr_jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sm_small(es, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fs, 10n)), Nat.sub(el, es)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(el), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(es)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(el, Fl)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(es, Fs)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(es)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def bigS source · line 78 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+el:Nat -> @+fl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+es:Nat -> @+fs:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+Fl:Nat -> @+Fs:Nat -> @+hfl:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fl) == Fl : Nat} -> @+hfs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(fs) == Fs : Nat} -> @+hFl:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fl) == True{} : Bool} -> @+hFs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, Fs) == True{} : Bool} -> @+hlt:{Nat.is_lt(es, el) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_round_pack(s, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, Nat.sub(el, 1n)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fl, 10n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, 1073741824}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr_jam(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sm_small(es, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(fs, 10n)), Nat.sub(el, es)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(el), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(es)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(el, Fl)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.mt(es, Fs)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/f64addg.xe(es)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}