F64addc.amen: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addc.bend as F64addc Lines 116-136 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addc.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addc.bend&start_line=116&end_line=136 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/lib/word.bend as WD 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/f64round.bend as FR import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT # addMags, equal normal exponents e: the 54-bit sum at bit 62 def amen(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +fa: WU.U64, +fb: WU.U64, +Fa: Nat, +Fb: Nat, +hfa: {SW.value(fa) == Fa : Nat}, +hfb: {SW.value(fb) == Fb : Nat}, +hFa: {C.fits(52n, Fa) == True{} : Bool}, +hFb: {C.fits(52n, Fb) == True{} : Bool}, +c: U32, +hc: {c == U32{WD.pw(32n, 21n)} : U32}) -> {F.round_pack(s, Nat.add(F.off(), e), X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)) == SF.round(s, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(1925n, e)) : F.F64}: +eW = Equal.trans(Nat, Nat.add(C.shift(53n, one), Nat.add(Fa, Fb)), Nat.add(Nat.add(C.shift(52n, one), C.shift(52n, one)), Nat.add(Fa, Fb)), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Fa, Fb)), Nat.double(C.shift(52n, one)), Nat.add(C.shift(52n, one), C.shift(52n, one)), NA.double_self(C.shift(52n, one))), Equal.trans(Nat, Nat.add(Nat.add(C.shift(52n, one), C.shift(52n, one)), Nat.add(Fa, Fb)), Nat.add(Nat.add(C.shift(52n, one), Fa), Nat.add(C.shift(52n, one), Fb)), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), swap4(C.shift(52n, one), C.shift(52n, one), Fa, Fb), Equal.trans(Nat, Nat.add(Nat.add(C.shift(52n, one), Fa), Nat.add(C.shift(52n, one), Fb)), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(C.shift(52n, one), Fb)), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(C.shift(52n, one), Fb)), Nat.add(C.shift(52n, one), Fa), Nat.add(Fa, C.shift(52n, one)), NA.add_comm(C.shift(52n, one), Fa)), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Fa, C.shift(52n, one)), z), Nat.add(C.shift(52n, one), Fb), Nat.add(Fb, C.shift(52n, one)), NA.add_comm(C.shift(52n, one), Fb))))) +fW = FR.fits_add1(53n, Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)), f53(one, h1, Fa, hFa), f53(one, h1, Fb, hFb)) +fV = L.subst(Nat, z => {C.fits(54n, z) == True{} : Bool}, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(C.shift(53n, one), Nat.add(Fa, Fb)), Equal.sym(Nat, Nat.add(C.shift(53n, one), Nat.add(Fa, Fb)), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), eW), fW) +eA = Equal.trans(Nat, SW.value(X.add(WU.U64{0, c}, X.add(fa, fb))), C.low(64n, Nat.add(SW.value(WU.U64{0, c}), SW.value(X.add(fa, fb)))), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), WA.add_value(WU.U64{0, c}, X.add(fa, fb)), Equal.trans(Nat, C.low(64n, Nat.add(SW.value(WU.U64{0, c}), SW.value(X.add(fa, fb)))), C.low(64n, Nat.add(C.shift(53n, one), SW.value(X.add(fa, fb)))), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Equal.cong(Nat, Nat, z => C.low(64n, Nat.add(z, SW.value(X.add(fa, fb)))), SW.value(WU.U64{0, c}), C.shift(53n, one), c53(one, h1, c, hc)), Equal.trans(Nat, C.low(64n, Nat.add(C.shift(53n, one), SW.value(X.add(fa, fb)))), C.low(64n, Nat.add(C.shift(53n, one), Nat.add(Fa, Fb))), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Equal.cong(Nat, Nat, z => C.low(64n, Nat.add(C.shift(53n, one), z)), SW.value(X.add(fa, fb)), Nat.add(Fa, Fb), addv2(fa, fb, Fa, Fb, hfa, hfb, hFa, hFb)), Equal.trans(Nat, C.low(64n, Nat.add(C.shift(53n, one), Nat.add(Fa, Fb))), Nat.add(C.shift(53n, one), Nat.add(Fa, Fb)), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), WW.low_fit(64n, Nat.add(C.shift(53n, one), Nat.add(Fa, Fb)), SH.fits_mono(54n, 64n, Nat.add(C.shift(53n, one), Nat.add(Fa, Fb)), {==}, fV)), eW)))) +fA = L.subst(Nat, z => {C.fits(54n, z) == True{} : Bool}, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), SW.value(X.add(WU.U64{0, c}, X.add(fa, fb))), Equal.sym(Nat, SW.value(X.add(WU.U64{0, c}, X.add(fa, fb))), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), eA), fW) +eS = Equal.trans(Nat, SW.value(X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), C.shift(9n, SW.value(X.add(WU.U64{0, c}, X.add(fa, fb)))), C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), shl_v(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n, 54n, {==}, {==}, fA), Equal.cong(Nat, Nat, z => C.shift(9n, z), SW.value(X.add(WU.U64{0, c}, X.add(fa, fb))), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), eA)) +f63 = Equal.trans(Bool, C.fits(63n, C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))))), C.fits(54n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), True{}, RT.fits_sh(9n, 54n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), fW) +h63 = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), SW.value(X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), Equal.sym(Nat, SW.value(X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), eS), f63) +f0 = Equal.trans(Bool, C.fits(53n, C.shift(53n, one)), Nat.is_lt(C.shift(53n, one), C.shift(53n, one)), False{}, Equal.sym(Bool, Nat.is_lt(C.shift(53n, one), C.shift(53n, one)), C.fits(53n, C.shift(53n, one)), FR.lt_fit(53n, one, h1, C.shift(53n, one))), N.lt_irrefl(C.shift(53n, one))) +hle = L.subst(Nat, z => {Nat.is_le(C.shift(53n, one), z) == True{} : Bool}, Nat.add(C.shift(53n, one), Nat.add(Fa, Fb)), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), eW, N.le_add_right(C.shift(53n, one), Nat.add(Fa, Fb))) +f62 = Equal.trans(Bool, C.fits(62n, C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))))), C.fits(53n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), False{}, RT.fits_sh(9n, 53n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), FR.nfit(53n, C.shift(53n, one), Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), hle, f0)) +h62 = L.subst(Nat, z => {C.fits(62n, z) == False{} : Bool}, C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), SW.value(X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), Equal.sym(Nat, SW.value(X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), eS), f62) +hx = Equal.trans(Nat, Nat.add(Nat.add(e, 1916n), 2180n), Nat.add(e, 4096n), Nat.add(4096n, e), NA.add_assoc(e, 1916n, 2180n), NA.add_comm(e, 4096n)) +r1 = FR.round_pack(s, Nat.add(F.off(), e), X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n), Nat.add(e, 1916n), hx, h62, h63) +r2 = Equal.cong(Nat, F.F64, z => SF.round(s, z, Nat.add(e, 1916n)), SW.value(X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), eS) +r3 = RT.round_shift(s, 9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(e, 1916n)) +ex = Equal.trans(Nat, Nat.add(Nat.add(e, 1916n), 9n), Nat.add(e, 1925n), Nat.add(1925n, e), NA.add_assoc(e, 1916n, 9n), NA.add_comm(e, 1925n)) +r4 = Equal.cong(Nat, F.F64, z => SF.round(s, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), z), Nat.add(Nat.add(e, 1916n), 9n), Nat.add(1925n, e), ex) Equal.trans(F.F64, F.round_pack(s, Nat.add(F.off(), e), X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), SF.round(s, SW.value(X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), Nat.add(e, 1916n)), SF.round(s, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(1925n, e)), r1, Equal.trans(F.F64, SF.round(s, SW.value(X.shl(X.add(WU.U64{0, c}, X.add(fa, fb)), 9n)), Nat.add(e, 1916n)), SF.round(s, C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), Nat.add(e, 1916n)), SF.round(s, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(1925n, e)), r2, Equal.trans(F.F64, SF.round(s, C.shift(9n, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one)))), Nat.add(e, 1916n)), SF.round(s, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(Nat.add(e, 1916n), 9n)), SF.round(s, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(1925n, e)), r3, r4))) Uses (42): 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_le 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=U32 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/lemmas/proofs/nat_algebra.bend&name=double_self https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst 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=lt_irrefl https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=pw https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addc.bend&name=addv2 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addc.bend&name=c53 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addc.bend&name=f53 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addc.bend&name=shl_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addc.bend&name=swap4 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=fits_add1 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=lt_fit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=nfit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=round_pack 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/w64add.bend&name=add_value 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=low_fit 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=low 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=off https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=round_pack 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