~/jendhub

def amb0

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64adda.bend:130

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend as F64adda
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

130# addMags, larger exponent el, the smaller operand subnormal (es = 0)
131def amb0(+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.rp62(s, Nat.add(F.off(), el), X.add(X.add(WU.U64{0, 536870912}, X.shl(fl, 9n)), X.shr_jam(F.am_small(0n, X.shl(fs, 9n)), Nat.sub(el, 0n)))) == SF.round(s, Nat.add(Fs, C.shift(Nat.sub(el, 1n), Nat.add(Fl, C.shift(52n, one)))), 1926n) : F.F64}:
132  +d = Nat.sub(el, 0n)
133  +T = C.shift(9n, Nat.add(Fl, C.shift(52n, one)))
134  +S = C.shift(10n, Fs)
135  +f9 = X.shl(fs, 9n)
136  +et = top9(one, h1, fl, Fl, hfl, hFl, 536870912, {==})
137  +hFv = L.subst(Nat, z => {C.fits(52n, z) == True{} : Bool}, Fs, SW.value(fs), Equal.sym(Nat, SW.value(fs), Fs, hfs), hFs)
138  +e9 = Equal.trans(Nat, SW.value(f9), C.shift(9n, SW.value(fs)), C.shift(9n, Fs), shl_v(fs, 9n, 52n, {==}, {==}, hFv), Equal.cong(Nat, Nat, z => C.shift(9n, z), SW.value(fs), Fs, hfs))
139  +hS62 = SH.fits_mono(Nat.add(10n, 52n), 62n, S, {==}, Equal.trans(Bool, C.fits(Nat.add(10n, 52n), S), C.fits(52n, Fs), True{}, RT.fits_sh(10n, 52n, Fs), hFs))
140  a1 = WA.add_value(f9, f9)
141  +es = Equal.trans(Nat, SW.value(X.add(f9, f9)), C.low(64n, Nat.add(SW.value(f9), SW.value(f9))), S, a1, Equal.trans(Nat, C.low(64n, Nat.add(SW.value(f9), SW.value(f9))), C.low(64n, S), S, Equal.cong(Nat, Nat, z => C.low(64n, z), Nat.add(SW.value(f9), SW.value(f9)), S, Equal.trans(Nat, Nat.add(SW.value(f9), SW.value(f9)), Nat.add(C.shift(9n, Fs), C.shift(9n, Fs)), S, Equal.trans(Nat, Nat.add(SW.value(f9), SW.value(f9)), Nat.add(C.shift(9n, Fs), SW.value(f9)), Nat.add(C.shift(9n, Fs), C.shift(9n, Fs)), Equal.cong(Nat, Nat, z => Nat.add(z, SW.value(f9)), SW.value(f9), C.shift(9n, Fs), e9), Equal.cong(Nat, Nat, z => Nat.add(C.shift(9n, Fs), z), SW.value(f9), C.shift(9n, Fs), e9)), Equal.sym(Nat, Nat.double(C.shift(9n, Fs)), Nat.add(C.shift(9n, Fs), C.shift(9n, Fs)), NA.double_self(C.shift(9n, Fs))))), WW.low_fit(64n, S, SH.fits_mono(62n, 64n, S, {==}, hS62))))
142  +hT62 = SH.fits_mono(Nat.add(9n, 53n), 62n, T, {==}, sh9(53n, Nat.add(Fl, C.shift(52n, one)), f53(one, h1, Fl, hFl)))
143  +hT61 = Equal.trans(Bool, C.fits(Nat.add(9n, 52n), T), C.fits(52n, Nat.add(Fl, C.shift(52n, one))), False{}, RT.fits_sh(9n, 52n, Nat.add(Fl, C.shift(52n, one))), n52(one, h1, Fl))
144  +hsig = sigv(X.add(WU.U64{0, 536870912}, X.shl(fl, 9n)), X.add(f9, f9), T, S, d, et, es, hT62, hS62)
145  +ed = N.sub_zero(el)
146  +he = Equal.trans(Nat, Nat.add(Nat.add(1916n, d), 2180n), Nat.add(Nat.add(1916n, el), 2180n), Nat.add(F.off(), el), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(1916n, z), 2180n), d, el, ed), Equal.trans(Nat, Nat.add(Nat.add(1916n, el), 2180n), Nat.add(1916n, Nat.add(el, 2180n)), Nat.add(F.off(), el), NA.add_assoc(1916n, el, 2180n), Equal.cong(Nat, Nat, z => Nat.add(1916n, z), Nat.add(el, 2180n), Nat.add(2180n, el), NA.add_comm(el, 2180n))))
147  +r1 = amb_core(s, Nat.add(F.off(), el), X.add(X.add(WU.U64{0, 536870912}, X.shl(fl, 9n)), X.shr_jam(F.am_small(0n, X.shl(fs, 9n)), Nat.sub(el, 0n))), C.shift(8n, Nat.add(Fl, C.shift(52n, one))), S, d, 1916n, hsig, he, N.le_trans(1n, 1916n, Nat.add(1916n, d), {==}, N.le_add_right(1916n, d)), hS62, hT62, hT61)
148  +r1b = Equal.trans(F.F64, F.rp62(s, Nat.add(F.off(), el), X.add(X.add(WU.U64{0, 536870912}, X.shl(fl, 9n)), X.shr_jam(F.am_small(0n, X.shl(fs, 9n)), Nat.sub(el, 0n)))), SF.round(s, Nat.add(S, C.shift(d, Nat.double(C.shift(8n, Nat.add(Fl, C.shift(52n, one)))))), 1916n), SF.round(s, Nat.add(S, C.shift(d, C.shift(9n, Nat.add(Fl, C.shift(52n, one))))), 1916n), r1, Equal.cong(Nat, F.F64, zz_ => SF.round(s, Nat.add(S, C.shift(d, zz_)), 1916n), Nat.double(C.shift(8n, Nat.add(Fl, C.shift(52n, one)))), C.shift(9n, Nat.add(Fl, C.shift(52n, one))), {==}))
149  +eq = N.sub_add(el, 1n, N.lt_succ_le_succ(0n, el, hlt))
150  +eV = Equal.trans(Nat, Nat.add(S, C.shift(d, T)), Nat.add(S, Nat.double(C.shift(Nat.sub(el, 1n), T))), C.shift(10n, Nat.add(Fs, C.shift(Nat.sub(el, 1n), Nat.add(Fl, C.shift(52n, one))))), Equal.cong(Nat, Nat, z => Nat.add(S, C.shift(z, T)), 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, eq))), Equal.trans(Nat, Nat.add(S, Nat.double(C.shift(Nat.sub(el, 1n), T))), Nat.add(S, C.shift(10n, C.shift(Nat.sub(el, 1n), Nat.add(Fl, C.shift(52n, one))))), C.shift(10n, Nat.add(Fs, C.shift(Nat.sub(el, 1n), Nat.add(Fl, C.shift(52n, one))))), Equal.cong(Nat, Nat, z => Nat.add(S, Nat.double(z)), C.shift(Nat.sub(el, 1n), T), C.shift(9n, C.shift(Nat.sub(el, 1n), Nat.add(Fl, C.shift(52n, one)))), shc(Nat.sub(el, 1n), 9n, Nat.add(Fl, C.shift(52n, one)))), Equal.sym(Nat, C.shift(10n, Nat.add(Fs, C.shift(Nat.sub(el, 1n), Nat.add(Fl, C.shift(52n, one))))), Nat.add(S, C.shift(10n, C.shift(Nat.sub(el, 1n), Nat.add(Fl, C.shift(52n, one))))), WW.shift_add(10n, Fs, C.shift(Nat.sub(el, 1n), Nat.add(Fl, C.shift(52n, one)))))))
151  +r2 = Equal.cong(Nat, F.F64, z => SF.round(s, z, 1916n), Nat.add(S, C.shift(d, T)), C.shift(10n, Nat.add(Fs, C.shift(Nat.sub(el, 1n), Nat.add(Fl, C.shift(52n, one))))), eV)
152  +r3 = RT.round_shift_to(s, 10n, Nat.add(Fs, C.shift(Nat.sub(el, 1n), Nat.add(Fl, C.shift(52n, one)))), 1916n, 1926n, {==})
153  Equal.trans(F.F64, F.rp62(s, Nat.add(F.off(), el), X.add(X.add(WU.U64{0, 536870912}, X.shl(fl, 9n)), X.shr_jam(F.am_small(0n, X.shl(fs, 9n)), Nat.sub(el, 0n)))), SF.round(s, Nat.add(S, C.shift(d, T)), 1916n), SF.round(s, Nat.add(Fs, C.shift(Nat.sub(el, 1n), Nat.add(Fl, C.shift(52n, one)))), 1926n), r1b, Equal.trans(F.F64, SF.round(s, Nat.add(S, C.shift(d, T)), 1916n), SF.round(s, C.shift(10n, Nat.add(Fs, C.shift(Nat.sub(el, 1n), Nat.add(Fl, C.shift(52n, one))))), 1916n), SF.round(s, Nat.add(Fs, C.shift(Nat.sub(el, 1n), Nat.add(Fl, C.shift(52n, one)))), 1926n), r2, r3))

Uses (45)

Used by (1)