F64adda.amb1: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend as F64adda Lines 108-128 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend&start_line=108&end_line=128 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/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/w64sh.bend as SH import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT # addMags, larger exponent el, smaller exponent es = 1 + p def amb1(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +el: Nat, +fl: WU.U64, +p: Nat, +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(1n+p, 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(1n+p, X.shl(fs, 9n)), Nat.sub(el, 1n+p)))) == SF.round(s, Nat.add(Nat.add(Fs, C.shift(52n, one)), C.shift(Nat.sub(el, 1n+p), Nat.add(Fl, C.shift(52n, one)))), Nat.add(1925n, 1n+p)) : F.F64}: +d = Nat.sub(el, 1n+p) +T = C.shift(9n, Nat.add(Fl, C.shift(52n, one))) +S = C.shift(9n, Nat.add(Fs, C.shift(52n, one))) +sw = X.add(X.shl(fs, 9n), WU.U64{0, 536870912}) +et = top9(one, h1, fl, Fl, hfl, hFl, 536870912, {==}) +es = Equal.trans(Nat, SW.value(sw), SW.value(X.add(WU.U64{0, 536870912}, X.shl(fs, 9n))), S, addc(X.shl(fs, 9n), WU.U64{0, 536870912}), top9(one, h1, fs, Fs, hfs, hFs, 536870912, {==})) +hT62 = SH.fits_mono(Nat.add(9n, 53n), 62n, T, {==}, sh9(53n, Nat.add(Fl, C.shift(52n, one)), f53(one, h1, Fl, hFl))) +hS62 = SH.fits_mono(Nat.add(9n, 53n), 62n, S, {==}, sh9(53n, Nat.add(Fs, C.shift(52n, one)), f53(one, h1, Fs, hFs))) +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)) +hsig = sigv(X.add(WU.U64{0, 536870912}, X.shl(fl, 9n)), sw, T, S, d, et, es, hT62, hS62) +eld = N.sub_add(el, 1n+p, N.lt_le(1n+p, el, hlt)) +he = Equal.trans(Nat, Nat.add(Nat.add(Nat.add(1916n, 1n+p), d), 2180n), Nat.add(Nat.add(1916n, Nat.add(1n+p, d)), 2180n), Nat.add(F.off(), el), Equal.cong(Nat, Nat, z => Nat.add(z, 2180n), Nat.add(Nat.add(1916n, 1n+p), d), Nat.add(1916n, Nat.add(1n+p, d)), NA.add_assoc(1916n, 1n+p, d)), Equal.trans(Nat, Nat.add(Nat.add(1916n, Nat.add(1n+p, 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), Nat.add(1n+p, d), el, eld), 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))))) +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(1n+p, X.shl(fs, 9n)), Nat.sub(el, 1n+p))), C.shift(8n, Nat.add(Fl, C.shift(52n, one))), S, d, Nat.add(1916n, 1n+p), hsig, he, N.le_trans(1n, Nat.add(1916n, 1n+p), Nat.add(Nat.add(1916n, 1n+p), d), {==}, N.le_add_right(Nat.add(1916n, 1n+p), d)), hS62, hT62, hT61) +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(1n+p, X.shl(fs, 9n)), Nat.sub(el, 1n+p)))), SF.round(s, Nat.add(S, C.shift(d, Nat.double(C.shift(8n, Nat.add(Fl, C.shift(52n, one)))))), Nat.add(1916n, 1n+p)), SF.round(s, Nat.add(S, C.shift(d, C.shift(9n, Nat.add(Fl, C.shift(52n, one))))), Nat.add(1916n, 1n+p)), r1, Equal.cong(Nat, F.F64, zz_ => SF.round(s, Nat.add(S, C.shift(d, zz_)), Nat.add(1916n, 1n+p)), Nat.double(C.shift(8n, Nat.add(Fl, C.shift(52n, one)))), C.shift(9n, Nat.add(Fl, C.shift(52n, one))), {==})) +eV = Equal.trans(Nat, Nat.add(S, C.shift(d, T)), Nat.add(S, C.shift(9n, C.shift(d, Nat.add(Fl, C.shift(52n, one))))), C.shift(9n, Nat.add(Nat.add(Fs, C.shift(52n, one)), C.shift(d, Nat.add(Fl, C.shift(52n, one))))), Equal.cong(Nat, Nat, z => Nat.add(S, z), C.shift(d, T), C.shift(9n, C.shift(d, Nat.add(Fl, C.shift(52n, one)))), shc(d, 9n, Nat.add(Fl, C.shift(52n, one)))), Equal.sym(Nat, C.shift(9n, Nat.add(Nat.add(Fs, C.shift(52n, one)), C.shift(d, Nat.add(Fl, C.shift(52n, one))))), Nat.add(S, C.shift(9n, C.shift(d, Nat.add(Fl, C.shift(52n, one))))), WW.shift_add(9n, Nat.add(Fs, C.shift(52n, one)), C.shift(d, Nat.add(Fl, C.shift(52n, one)))))) +r2 = Equal.cong(Nat, F.F64, z => SF.round(s, z, Nat.add(1916n, 1n+p)), Nat.add(S, C.shift(d, T)), C.shift(9n, Nat.add(Nat.add(Fs, C.shift(52n, one)), C.shift(d, Nat.add(Fl, C.shift(52n, one))))), eV) +r3 = RT.round_shift(s, 9n, Nat.add(Nat.add(Fs, C.shift(52n, one)), C.shift(d, Nat.add(Fl, C.shift(52n, one)))), Nat.add(1916n, 1n+p)) +r4 = Equal.cong(Nat, F.F64, z => SF.round(s, Nat.add(Nat.add(Fs, C.shift(52n, one)), C.shift(d, Nat.add(Fl, C.shift(52n, one)))), z), Nat.add(Nat.add(1916n, 1n+p), 9n), Nat.add(1925n, 1n+p), Equal.cong(Nat, Nat, z => 1917n+z, Nat.add(p, 9n), Nat.add(9n, p), NA.add_comm(p, 9n))) 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(1n+p, X.shl(fs, 9n)), Nat.sub(el, 1n+p)))), SF.round(s, Nat.add(S, C.shift(d, T)), Nat.add(1916n, 1n+p)), SF.round(s, Nat.add(Nat.add(Fs, C.shift(52n, one)), C.shift(d, Nat.add(Fl, C.shift(52n, one)))), Nat.add(1925n, 1n+p)), r1b, Equal.trans(F.F64, SF.round(s, Nat.add(S, C.shift(d, T)), Nat.add(1916n, 1n+p)), SF.round(s, C.shift(9n, Nat.add(Nat.add(Fs, C.shift(52n, one)), C.shift(d, Nat.add(Fl, C.shift(52n, one))))), Nat.add(1916n, 1n+p)), SF.round(s, Nat.add(Nat.add(Fs, C.shift(52n, one)), C.shift(d, Nat.add(Fl, C.shift(52n, one)))), Nat.add(1925n, 1n+p)), r2, Equal.trans(F.F64, SF.round(s, C.shift(9n, Nat.add(Nat.add(Fs, C.shift(52n, one)), C.shift(d, Nat.add(Fl, C.shift(52n, one))))), Nat.add(1916n, 1n+p)), SF.round(s, Nat.add(Nat.add(Fs, C.shift(52n, one)), C.shift(d, Nat.add(Fl, C.shift(52n, one)))), Nat.add(Nat.add(1916n, 1n+p), 9n)), SF.round(s, Nat.add(Nat.add(Fs, C.shift(52n, one)), C.shift(d, Nat.add(Fl, C.shift(52n, one)))), Nat.add(1925n, 1n+p)), r3, r4))) Uses (39): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_add_right https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=sub_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend&name=addc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend&name=amb_core https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend&name=f53 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend&name=n52 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend&name=sh9 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend&name=shc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend&name=sigv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adda.bend&name=top9 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend&name=fits_sh https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend&name=round_shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=fits_mono https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=round https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=am_small https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=off https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=rp62 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=shl https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=shr_jam