~/jendhub

def smb0

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addb.bend:89

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addb.bend as F64addb
import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend as AA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addp.bend as AP
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adds.bend as AS

89# subMags, the smaller operand subnormal (es = 0)
90def smb0(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +el: Nat, +fl: WU.U64, +fs: WU.U64, +Fl: Nat, +Fs: Nat, +hfl: {SW.value(fl) == Fl : Nat}, +hfs: {SW.value(fs) == Fs : Nat}, +hFl: {C.fits(52n, Fl) == True{} : Bool}, +hFs: {C.fits(52n, Fs) == True{} : Bool}, +hlt: {Nat.is_lt(0n, el) == True{} : Bool}) -> {F.norm_round_pack(s, Nat.add(F.off(), Nat.sub(el, 1n)), X.sub(X.add(X.shl(fl, 10n), WU.U64{0, 1073741824}), X.shr_jam(F.sm_small(0n, X.shl(fs, 10n)), Nat.sub(el, 0n)))) == SF.round(s, Nat.sub(C.shift(Nat.sub(el, 1n), Nat.add(Fl, C.shift(52n, one))), Fs), 1926n) : F.F64}:
91  +d = Nat.sub(el, 0n)
92  +f10 = X.shl(fs, 10n)
93  +et = top10(one, h1, fl, Fl, hfl, hFl, 1073741824, {==})
94  +hFv = L.subst(Nat, z => {C.fits(52n, z) == True{} : Bool}, Fs, SW.value(fs), Equal.sym(Nat, SW.value(fs), Fs, hfs), hFs)
95  +e10 = Equal.trans(Nat, SW.value(f10), C.shift(10n, SW.value(fs)), C.shift(10n, Fs), AA.shl_v(fs, 10n, 52n, {==}, {==}, hFv), Equal.cong(Nat, Nat, z => C.shift(10n, z), SW.value(fs), Fs, hfs))
96  +S = C.shift(10n, C.shift(1n, Fs))
97  +f53s = Equal.trans(Bool, C.fits(Nat.add(1n, 52n), C.shift(1n, Fs)), C.fits(52n, Fs), True{}, RT.fits_sh(1n, 52n, Fs), hFs)
98  +hS = SH.fits_mono(Nat.add(10n, 53n), 63n, S, {==}, Equal.trans(Bool, C.fits(Nat.add(10n, 53n), S), C.fits(53n, C.shift(1n, Fs)), True{}, RT.fits_sh(10n, 53n, C.shift(1n, Fs)), f53s))
99  a1 = WA.add_value(f10, f10)
100  +eS0 = Equal.trans(Nat, Nat.add(SW.value(f10), SW.value(f10)), Nat.add(C.shift(10n, Fs), C.shift(10n, Fs)), S, Equal.trans(Nat, Nat.add(SW.value(f10), SW.value(f10)), Nat.add(C.shift(10n, Fs), SW.value(f10)), Nat.add(C.shift(10n, Fs), C.shift(10n, Fs)), Equal.cong(Nat, Nat, z => Nat.add(z, SW.value(f10)), SW.value(f10), C.shift(10n, Fs), e10), Equal.cong(Nat, Nat, z => Nat.add(C.shift(10n, Fs), z), SW.value(f10), C.shift(10n, Fs), e10)), Equal.trans(Nat, Nat.add(C.shift(10n, Fs), C.shift(10n, Fs)), Nat.double(C.shift(10n, Fs)), S, Equal.sym(Nat, Nat.double(C.shift(10n, Fs)), Nat.add(C.shift(10n, Fs), C.shift(10n, Fs)), NA.double_self(C.shift(10n, Fs))), Equal.sym(Nat, S, Nat.double(C.shift(10n, Fs)), WW.shift_dbl(10n, Fs))))
101  +es = Equal.trans(Nat, SW.value(X.add(f10, f10)), C.low(64n, Nat.add(SW.value(f10), SW.value(f10))), S, a1, Equal.trans(Nat, C.low(64n, Nat.add(SW.value(f10), SW.value(f10))), C.low(64n, S), S, Equal.cong(Nat, Nat, z => C.low(64n, z), Nat.add(SW.value(f10), SW.value(f10)), S, eS0), WW.low_fit(64n, S, SH.fits_mono(63n, 64n, S, {==}, hS))))
102  +ed = N.sub_zero(el)
103  +eq1 = N.sub_add(el, 1n, N.lt_succ_le_succ(0n, el, hlt))
104  +hd1 = L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, el, d, Equal.sym(Nat, d, el, ed), N.lt_succ_le_succ(0n, el, hlt))
105  +hT63 = f63s(one, h1, 10n, Fl, hFl, {==})
106  +hT62 = Equal.trans(Bool, C.fits(Nat.add(10n, 52n), C.shift(10n, Nat.add(Fl, C.shift(52n, one)))), C.fits(52n, Nat.add(Fl, C.shift(52n, one))), False{}, RT.fits_sh(10n, 52n, Nat.add(Fl, C.shift(52n, one))), AA.n52(one, h1, Fl))
107  +hle = hlt2(one, h1, C.shift(9n, Nat.add(Fl, C.shift(52n, one))), C.shift(1n, Fs), d, hd1, hS, hT62)
108  +hsig = subv(X.add(X.shl(fl, 10n), WU.U64{0, 1073741824}), X.add(f10, f10), C.shift(9n, Nat.add(Fl, C.shift(52n, one))), S, d, et, es, hle)
109  +he = Equal.trans(Nat, Nat.add(Nat.add(1915n, d), 2180n), Nat.add(Nat.add(1915n, 1n+Nat.sub(el, 1n)), 2180n), Nat.add(F.off(), Nat.sub(el, 1n)), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(1915n, z), 2180n), d, 1n+Nat.sub(el, 1n), Equal.trans(Nat, d, el, 1n+Nat.sub(el, 1n), ed, Equal.sym(Nat, 1n+Nat.sub(el, 1n), el, eq1))), Equal.cong(Nat, Nat, z => 1916n+z, Nat.add(Nat.sub(el, 1n), 2180n), Nat.add(2180n, Nat.sub(el, 1n)), NA.add_comm(Nat.sub(el, 1n), 2180n)))
110  +hx63 = N.le_trans(63n, 1915n, Nat.add(1915n, d), {==}, N.le_add_right(1915n, d))
111  +r1 = AS.smb_c(one, h1, s, Nat.add(F.off(), Nat.sub(el, 1n)), X.sub(X.add(X.shl(fl, 10n), WU.U64{0, 1073741824}), X.shr_jam(F.sm_small(0n, X.shl(fs, 10n)), Nat.sub(el, 0n))), C.shift(9n, Nat.add(Fl, C.shift(52n, one))), C.shift(1n, Fs), d, 1915n, hsig, he, hx63, hd1, hS, hT62, hT63, Nat.is_eq(C.low(d, S), 0n), {==})
112  +r1b = Equal.trans(F.F64, F.norm_round_pack(s, Nat.add(F.off(), Nat.sub(el, 1n)), X.sub(X.add(X.shl(fl, 10n), WU.U64{0, 1073741824}), X.shr_jam(F.sm_small(0n, X.shl(fs, 10n)), Nat.sub(el, 0n)))), SF.round(s, Nat.sub(C.shift(d, Nat.double(C.shift(9n, Nat.add(Fl, C.shift(52n, one))))), S), 1915n), SF.round(s, Nat.sub(C.shift(d, C.shift(10n, Nat.add(Fl, C.shift(52n, one)))), S), 1915n), r1, Equal.cong(Nat, F.F64, z => SF.round(s, Nat.sub(C.shift(d, z), S), 1915n), Nat.double(C.shift(9n, Nat.add(Fl, C.shift(52n, one)))), C.shift(10n, Nat.add(Fl, C.shift(52n, one))), {==}))
113  +A = C.shift(Nat.sub(el, 1n), Nat.add(Fl, C.shift(52n, one)))
114  +hFA = N.le_trans(Fs, C.shift(52n, one), A, N.lt_le(Fs, C.shift(52n, one), WW.lt_one(52n, one, h1, Fs, hFs)), N.le_trans(C.shift(52n, one), Nat.add(Fl, C.shift(52n, one)), A, L.subst(Nat, z => {Nat.is_le(C.shift(52n, one), z) == True{} : Bool}, Nat.add(C.shift(52n, one), Fl), Nat.add(Fl, C.shift(52n, one)), NA.add_comm(C.shift(52n, one), Fl), N.le_add_right(C.shift(52n, one), Fl)), WW.shift_ge(Nat.sub(el, 1n), Nat.add(Fl, C.shift(52n, one)))))
115  +eW = Equal.trans(Nat, Nat.sub(C.shift(d, C.shift(10n, Nat.add(Fl, C.shift(52n, one)))), S), Nat.sub(Nat.double(C.shift(Nat.sub(el, 1n), C.shift(10n, Nat.add(Fl, C.shift(52n, one))))), S), C.shift(11n, Nat.sub(A, Fs)), Equal.cong(Nat, Nat, z => Nat.sub(C.shift(z, C.shift(10n, Nat.add(Fl, C.shift(52n, one)))), S), d, 1n+Nat.sub(el, 1n), Equal.trans(Nat, d, el, 1n+Nat.sub(el, 1n), ed, Equal.sym(Nat, 1n+Nat.sub(el, 1n), el, eq1))), Equal.trans(Nat, Nat.sub(Nat.double(C.shift(Nat.sub(el, 1n), C.shift(10n, Nat.add(Fl, C.shift(52n, one))))), S), Nat.sub(Nat.double(C.shift(10n, A)), S), C.shift(11n, Nat.sub(A, Fs)), Equal.cong(Nat, Nat, z => Nat.sub(Nat.double(z), S), C.shift(Nat.sub(el, 1n), C.shift(10n, Nat.add(Fl, C.shift(52n, one)))), C.shift(10n, A), AA.shc(Nat.sub(el, 1n), 10n, Nat.add(Fl, C.shift(52n, one)))), Equal.trans(Nat, Nat.sub(Nat.double(C.shift(10n, A)), S), Nat.sub(C.shift(10n, C.shift(1n, A)), S), C.shift(11n, Nat.sub(A, Fs)), Equal.cong(Nat, Nat, z => Nat.sub(z, S), Nat.double(C.shift(10n, A)), C.shift(10n, C.shift(1n, A)), Equal.sym(Nat, C.shift(10n, C.shift(1n, A)), Nat.double(C.shift(10n, A)), WW.shift_dbl(10n, A))), Equal.trans(Nat, Nat.sub(C.shift(10n, C.shift(1n, A)), S), C.shift(10n, Nat.sub(C.shift(1n, A), C.shift(1n, Fs))), C.shift(11n, Nat.sub(A, Fs)), AP.sub_shift(10n, C.shift(1n, A), C.shift(1n, Fs), WW.shift_mono(1n, Fs, A, hFA)), Equal.trans(Nat, C.shift(10n, Nat.sub(C.shift(1n, A), C.shift(1n, Fs))), C.shift(10n, C.shift(1n, Nat.sub(A, Fs))), C.shift(11n, Nat.sub(A, Fs)), Equal.cong(Nat, Nat, z => C.shift(10n, z), Nat.sub(C.shift(1n, A), C.shift(1n, Fs)), C.shift(1n, Nat.sub(A, Fs)), AP.sub_shift(1n, A, Fs, hFA)), Equal.sym(Nat, C.shift(Nat.add(10n, 1n), Nat.sub(A, Fs)), C.shift(10n, C.shift(1n, Nat.sub(A, Fs))), WW.shift_comp(10n, 1n, Nat.sub(A, Fs))))))))
116  +r2 = Equal.cong(Nat, F.F64, z => SF.round(s, z, 1915n), Nat.sub(C.shift(d, C.shift(10n, Nat.add(Fl, C.shift(52n, one)))), S), C.shift(11n, Nat.sub(A, Fs)), eW)
117  +r3 = RT.round_shift_to(s, 11n, Nat.sub(A, Fs), 1915n, 1926n, {==})
118  Equal.trans(F.F64, F.norm_round_pack(s, Nat.add(F.off(), Nat.sub(el, 1n)), X.sub(X.add(X.shl(fl, 10n), WU.U64{0, 1073741824}), X.shr_jam(F.sm_small(0n, X.shl(fs, 10n)), Nat.sub(el, 0n)))), SF.round(s, Nat.sub(C.shift(d, C.shift(10n, Nat.add(Fl, C.shift(52n, one)))), S), 1915n), SF.round(s, Nat.sub(A, Fs), 1926n), r1b, Equal.trans(F.F64, SF.round(s, Nat.sub(C.shift(d, C.shift(10n, Nat.add(Fl, C.shift(52n, one)))), S), 1915n), SF.round(s, C.shift(11n, Nat.sub(A, Fs)), 1915n), SF.round(s, Nat.sub(A, Fs), 1926n), r2, r3))

Uses (53)

Used by (1)