F64mexp.mexp: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mexp.bend as F64mexp Lines 78-91 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mexp.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mexp.bend&start_line=78&end_line=91 import Base import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F 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/w64mul.bend as W64M import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR # x0 + 21 + sa + sb is the spec's product exponent def mexp(+ea: Nat, +eb: Nat, +sa: Nat, +sb: Nat, +Xx: Nat, +Xy: Nat, +n2x: {Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat}, +n2y: {Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hsb: {Nat.is_le(sb, 53n) == True{} : Bool}, +hXx: {Nat.is_le(1926n, Xx) == True{} : Bool}, +hXy: {Nat.is_le(1926n, Xy) == True{} : Bool}) -> {Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(sa, sb)) == Nat.sub(Nat.add(Xx, Xy), SF.zb()) : Nat}: +ex0 = x0_eq(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy) +exx = x_eq(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy) +eS0 = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 5119n), Nat.add(5119n, Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n))), Nat.add(ea, eb), NA.add_comm(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 5119n), N.sub_add(Nat.add(ea, eb), 5119n, N.le_trans(5119n, 8088n, Nat.add(ea, eb), {==}, s_ge(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy)))) +eS = Equal.trans(Nat, Nat.add(ea, eb), Nat.add(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 5119n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 5119n), Nat.add(ea, eb), eS0), Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 5119n), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n), 5119n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), Equal.cong(Nat, Nat, z => Nat.add(z, 5119n), Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n), Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), exx)), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n), 5119n), Nat.add(Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), 2180n), 5119n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(z, 2180n), 5119n), Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), ex0)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), 2180n), 5119n), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), 7299n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), NA.add_assoc(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), 2180n, 5119n), NA.add_assoc(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n, 7299n))))) +e1 = Equal.trans(Nat, Nat.add(Nat.add(ea, sa), Nat.add(eb, sb)), Nat.add(Nat.add(Xx, 2171n), Nat.add(eb, sb)), Nat.add(Nat.add(Xx, 2171n), Nat.add(Xy, 2171n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(eb, sb)), Nat.add(ea, sa), Nat.add(Xx, 2171n), n2x), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Xx, 2171n), z), Nat.add(eb, sb), Nat.add(Xy, 2171n), n2y)) +e2 = W64M.add4(ea, sa, eb, sb) +e3 = W64M.add4(Xx, 2171n, Xy, 2171n) +T2 = Nat.add(sa, sb) +W = Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), T2) +e4 = Equal.trans(Nat, Nat.add(Nat.add(W, 3000n), 4342n), Nat.add(W, 7342n), Nat.add(Nat.add(Xx, Xy), 4342n), NA.add_assoc(W, 3000n, 4342n), Equal.trans(Nat, Nat.add(W, 7342n), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(T2, 7342n)), Nat.add(Nat.add(Xx, Xy), 4342n), NA.add_assoc(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), T2, 7342n), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(T2, 7342n)), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(7342n, T2)), Nat.add(Nat.add(Xx, Xy), 4342n), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), z), Nat.add(T2, 7342n), Nat.add(7342n, T2), NA.add_comm(T2, 7342n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(7342n, T2)), Nat.add(Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), 7342n), T2), Nat.add(Nat.add(Xx, Xy), 4342n), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), 7342n), T2), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(7342n, T2)), NA.add_assoc(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), 7342n, T2)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), 7342n), T2), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), T2), Nat.add(Nat.add(Xx, Xy), 4342n), Equal.cong(Nat, Nat, z => Nat.add(z, T2), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), 7342n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), NA.add_assoc(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n, 7342n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), T2), Nat.add(Nat.add(ea, eb), T2), Nat.add(Nat.add(Xx, Xy), 4342n), Equal.cong(Nat, Nat, z => Nat.add(z, T2), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), Nat.add(ea, eb), Equal.sym(Nat, Nat.add(ea, eb), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), eS)), Equal.trans(Nat, Nat.add(Nat.add(ea, eb), T2), Nat.add(Nat.add(ea, sa), Nat.add(eb, sb)), Nat.add(Nat.add(Xx, Xy), 4342n), Equal.sym(Nat, Nat.add(Nat.add(ea, sa), Nat.add(eb, sb)), Nat.add(Nat.add(ea, eb), T2), e2), Equal.trans(Nat, Nat.add(Nat.add(ea, sa), Nat.add(eb, sb)), Nat.add(Nat.add(Xx, 2171n), Nat.add(Xy, 2171n)), Nat.add(Nat.add(Xx, Xy), 4342n), e1, e3)))))))) +e5 = A.add_cancel_r(Nat.add(W, 3000n), Nat.add(Xx, Xy), 4342n, e4) Equal.sym(Nat, Nat.sub(Nat.add(Xx, Xy), SF.zb()), W, Equal.trans(Nat, Nat.sub(Nat.add(Xx, Xy), 3000n), Nat.sub(Nat.add(W, 3000n), 3000n), W, Equal.cong(Nat, Nat, z => Nat.sub(z, 3000n), Nat.add(Xx, Xy), Nat.add(W, 3000n), Equal.sym(Nat, Nat.add(W, 3000n), Nat.add(Xx, Xy), e5)), FR.sub_add_l(W, 3000n))) Uses (20): 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.is_le 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_trans 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/lib/u32alg.bend&name=add_cancel_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mexp.bend&name=s_ge https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mexp.bend&name=x0_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mexp.bend&name=x_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=sub_add_l https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&name=add4 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=zb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=off