def add_alg

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64add.bend:48

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/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/math/typed/width.bend as WW

48# the limb sums: al + bl == l + 2^32 c1, ah + bh == s + 2^32 c2, s + c1 == h + 2^32 c3
49def add_alg(+al: Nat, +ah: Nat, +bl: Nat, +bh: Nat, +l: Nat, +c1: Nat, +s: Nat, +c2: Nat, +h: Nat, +c3: Nat, +e1: {Nat.add(l, C.shift(32n, c1)) == Nat.add(al, bl) : Nat}, +e2: {Nat.add(s, C.shift(32n, c2)) == Nat.add(ah, bh) : Nat}, +e3: {Nat.add(h, C.shift(32n, c3)) == Nat.add(s, c1) : Nat}) -> {Nat.add(Nat.add(al, C.shift(32n, ah)), Nat.add(bl, C.shift(32n, bh))) == Nat.add(Nat.add(l, C.shift(32n, h)), C.shift(32n, C.shift(32n, Nat.add(c3, c2)))) : Nat}:
50  Equal.trans(Nat, Nat.add(Nat.add(al, C.shift(32n, ah)), Nat.add(bl, C.shift(32n, bh))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Nat.add(Nat.add(l, C.shift(32n, h)), C.shift(32n, C.shift(32n, Nat.add(c3, c2)))), Equal.trans(Nat, Nat.add(Nat.add(al, C.shift(32n, ah)), Nat.add(bl, C.shift(32n, bh))), Nat.add(Nat.add(al, bl), Nat.add(C.shift(32n, ah), C.shift(32n, bh))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), W64M.add4(al, C.shift(32n, ah), bl, C.shift(32n, bh)), Equal.trans(Nat, Nat.add(Nat.add(al, bl), Nat.add(C.shift(32n, ah), C.shift(32n, bh))), Nat.add(Nat.add(al, bl), C.shift(32n, Nat.add(ah, bh))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(al, bl), t), Nat.add(C.shift(32n, ah), C.shift(32n, bh)), C.shift(32n, Nat.add(ah, bh)), Equal.sym(Nat, C.shift(32n, Nat.add(ah, bh)), Nat.add(C.shift(32n, ah), C.shift(32n, bh)), WW.shift_add(32n, ah, bh))), Equal.trans(Nat, Nat.add(Nat.add(al, bl), C.shift(32n, Nat.add(ah, bh))), Nat.add(Nat.add(l, C.shift(32n, c1)), C.shift(32n, Nat.add(ah, bh))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(32n, Nat.add(ah, bh))), Nat.add(al, bl), Nat.add(l, C.shift(32n, c1)), Equal.sym(Nat, Nat.add(l, C.shift(32n, c1)), Nat.add(al, bl), e1)), Equal.trans(Nat, Nat.add(Nat.add(l, C.shift(32n, c1)), C.shift(32n, Nat.add(ah, bh))), Nat.add(Nat.add(l, C.shift(32n, c1)), C.shift(32n, Nat.add(s, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(l, C.shift(32n, c1)), C.shift(32n, t)), Nat.add(ah, bh), Nat.add(s, C.shift(32n, c2)), Equal.sym(Nat, Nat.add(s, C.shift(32n, c2)), Nat.add(ah, bh), e2)), Equal.trans(Nat, Nat.add(Nat.add(l, C.shift(32n, c1)), C.shift(32n, Nat.add(s, C.shift(32n, c2)))), Nat.add(Nat.add(l, C.shift(32n, c1)), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(l, C.shift(32n, c1)), t), C.shift(32n, Nat.add(s, C.shift(32n, c2))), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2))), WW.shift_add(32n, s, C.shift(32n, c2))), Equal.trans(Nat, Nat.add(Nat.add(l, C.shift(32n, c1)), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, c1), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2))))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), NA.add_assoc(l, C.shift(32n, c1), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2)))), Equal.cong(Nat, Nat, t => Nat.add(l, t), Nat.add(C.shift(32n, c1), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2)))), Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2)))), NA.add_swap(C.shift(32n, c1), C.shift(32n, s), C.shift(32n, C.shift(32n, c2)))))))))), Equal.sym(Nat, Nat.add(Nat.add(l, C.shift(32n, h)), C.shift(32n, C.shift(32n, Nat.add(c3, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.trans(Nat, Nat.add(Nat.add(l, C.shift(32n, h)), C.shift(32n, C.shift(32n, Nat.add(c3, c2)))), Nat.add(Nat.add(l, C.shift(32n, h)), C.shift(32n, Nat.add(C.shift(32n, c3), C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(l, C.shift(32n, h)), C.shift(32n, t)), C.shift(32n, Nat.add(c3, c2)), Nat.add(C.shift(32n, c3), C.shift(32n, c2)), WW.shift_add(32n, c3, c2)), Equal.trans(Nat, Nat.add(Nat.add(l, C.shift(32n, h)), C.shift(32n, Nat.add(C.shift(32n, c3), C.shift(32n, c2)))), Nat.add(Nat.add(l, C.shift(32n, h)), Nat.add(C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(l, C.shift(32n, h)), t), C.shift(32n, Nat.add(C.shift(32n, c3), C.shift(32n, c2))), Nat.add(C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2))), WW.shift_add(32n, C.shift(32n, c3), C.shift(32n, c2))), Equal.trans(Nat, Nat.add(Nat.add(l, C.shift(32n, h)), Nat.add(C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, h), Nat.add(C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2))))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), NA.add_assoc(l, C.shift(32n, h), Nat.add(C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2)))), Equal.trans(Nat, Nat.add(l, Nat.add(C.shift(32n, h), Nat.add(C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2))))), Nat.add(l, Nat.add(Nat.add(C.shift(32n, h), C.shift(32n, C.shift(32n, c3))), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(l, t), Nat.add(C.shift(32n, h), Nat.add(C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2)))), Nat.add(Nat.add(C.shift(32n, h), C.shift(32n, C.shift(32n, c3))), C.shift(32n, C.shift(32n, c2))), Equal.sym(Nat, Nat.add(Nat.add(C.shift(32n, h), C.shift(32n, C.shift(32n, c3))), C.shift(32n, C.shift(32n, c2))), Nat.add(C.shift(32n, h), Nat.add(C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2)))), NA.add_assoc(C.shift(32n, h), C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2))))), Equal.trans(Nat, Nat.add(l, Nat.add(Nat.add(C.shift(32n, h), C.shift(32n, C.shift(32n, c3))), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, Nat.add(h, C.shift(32n, c3))), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(l, Nat.add(t, C.shift(32n, C.shift(32n, c2)))), Nat.add(C.shift(32n, h), C.shift(32n, C.shift(32n, c3))), C.shift(32n, Nat.add(h, C.shift(32n, c3))), Equal.sym(Nat, C.shift(32n, Nat.add(h, C.shift(32n, c3))), Nat.add(C.shift(32n, h), C.shift(32n, C.shift(32n, c3))), WW.shift_add(32n, h, C.shift(32n, c3)))), Equal.trans(Nat, Nat.add(l, Nat.add(C.shift(32n, Nat.add(h, C.shift(32n, c3))), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, Nat.add(s, c1)), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(l, Nat.add(C.shift(32n, t), C.shift(32n, C.shift(32n, c2)))), Nat.add(h, C.shift(32n, c3)), Nat.add(s, c1), e3), Equal.trans(Nat, Nat.add(l, Nat.add(C.shift(32n, Nat.add(s, c1)), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(Nat.add(C.shift(32n, s), C.shift(32n, c1)), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(l, Nat.add(t, C.shift(32n, C.shift(32n, c2)))), C.shift(32n, Nat.add(s, c1)), Nat.add(C.shift(32n, s), C.shift(32n, c1)), WW.shift_add(32n, s, c1)), Equal.cong(Nat, Nat, t => Nat.add(l, t), Nat.add(Nat.add(C.shift(32n, s), C.shift(32n, c1)), C.shift(32n, C.shift(32n, c2))), Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2)))), NA.add_assoc(C.shift(32n, s), C.shift(32n, c1), C.shift(32n, C.shift(32n, c2)))))))))))))