def mexp

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64mexp.bend:78

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

78# x0 + 21 + sa + sb is the spec's product exponent
79def 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}:
80  +ex0 = x0_eq(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy)
81  +exx = x_eq(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy)
82  +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))))
83  +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)))))
84  +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))
85  +e2 = W64M.add4(ea, sa, eb, sb)
86  +e3 = W64M.add4(Xx, 2171n, Xy, 2171n)
87  +T2 = Nat.add(sa, sb)
88  +W = Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), T2)
89  +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))))))))
90  +e5 = A.add_cancel_r(Nat.add(W, 3000n), Nat.add(Xx, Xy), 4342n, e4)
91  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)))