def sub_alg

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

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

296def sub_alg(+lo: Nat, +hi: Nat, +al: Nat, +ah: Nat, +bl: Nat, +bh: Nat, +s: Nat, +b1: Nat, +b2: Nat, +b3: Nat, +e1: {Nat.add(lo, bl) == Nat.add(al, C.shift(32n, b1)) : Nat}, +e2: {Nat.add(s, bh) == Nat.add(ah, C.shift(32n, b2)) : Nat}, +e3: {Nat.add(hi, b1) == Nat.add(s, C.shift(32n, b3)) : Nat}) -> {Nat.add(Nat.add(lo, C.shift(32n, hi)), Nat.add(bl, C.shift(32n, bh))) == Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))) : Nat}:
297  Equal.trans(Nat, Nat.add(Nat.add(lo, C.shift(32n, hi)), Nat.add(bl, C.shift(32n, bh))), Nat.add(Nat.add(lo, bl), Nat.add(C.shift(32n, hi), C.shift(32n, bh))), Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), W64M.add4(lo, C.shift(32n, hi), bl, C.shift(32n, bh)), Equal.trans(Nat, Nat.add(Nat.add(lo, bl), Nat.add(C.shift(32n, hi), C.shift(32n, bh))), Nat.add(Nat.add(lo, bl), C.shift(32n, Nat.add(hi, bh))), Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(lo, bl), t), Nat.add(C.shift(32n, hi), C.shift(32n, bh)), C.shift(32n, Nat.add(hi, bh)), Equal.sym(Nat, C.shift(32n, Nat.add(hi, bh)), Nat.add(C.shift(32n, hi), C.shift(32n, bh)), WW.shift_add(32n, hi, bh))), Equal.trans(Nat, Nat.add(Nat.add(lo, bl), C.shift(32n, Nat.add(hi, bh))), Nat.add(Nat.add(al, C.shift(32n, b1)), C.shift(32n, Nat.add(hi, bh))), Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(32n, Nat.add(hi, bh))), Nat.add(lo, bl), Nat.add(al, C.shift(32n, b1)), e1), Equal.trans(Nat, Nat.add(Nat.add(al, C.shift(32n, b1)), C.shift(32n, Nat.add(hi, bh))), Nat.add(al, Nat.add(C.shift(32n, b1), C.shift(32n, Nat.add(hi, bh)))), Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), NA.add_assoc(al, C.shift(32n, b1), C.shift(32n, Nat.add(hi, bh))), Equal.trans(Nat, Nat.add(al, Nat.add(C.shift(32n, b1), C.shift(32n, Nat.add(hi, bh)))), Nat.add(al, C.shift(32n, Nat.add(b1, Nat.add(hi, bh)))), Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), Equal.cong(Nat, Nat, t => Nat.add(al, t), Nat.add(C.shift(32n, b1), C.shift(32n, Nat.add(hi, bh))), C.shift(32n, Nat.add(b1, Nat.add(hi, bh))), Equal.sym(Nat, C.shift(32n, Nat.add(b1, Nat.add(hi, bh))), Nat.add(C.shift(32n, b1), C.shift(32n, Nat.add(hi, bh))), WW.shift_add(32n, b1, Nat.add(hi, bh)))), Equal.trans(Nat, Nat.add(al, C.shift(32n, Nat.add(b1, Nat.add(hi, bh)))), Nat.add(al, C.shift(32n, Nat.add(ah, C.shift(32n, Nat.add(b2, b3))))), Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), Equal.cong(Nat, Nat, t => Nat.add(al, C.shift(32n, t)), Nat.add(b1, Nat.add(hi, bh)), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), Equal.trans(Nat, Nat.add(b1, Nat.add(hi, bh)), Nat.add(hi, Nat.add(b1, bh)), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), NA.add_swap(b1, hi, bh), Equal.trans(Nat, Nat.add(hi, Nat.add(b1, bh)), Nat.add(Nat.add(hi, b1), bh), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), Equal.sym(Nat, Nat.add(Nat.add(hi, b1), bh), Nat.add(hi, Nat.add(b1, bh)), NA.add_assoc(hi, b1, bh)), Equal.trans(Nat, Nat.add(Nat.add(hi, b1), bh), Nat.add(Nat.add(s, C.shift(32n, b3)), bh), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), Equal.cong(Nat, Nat, t => Nat.add(t, bh), Nat.add(hi, b1), Nat.add(s, C.shift(32n, b3)), e3), Equal.trans(Nat, Nat.add(Nat.add(s, C.shift(32n, b3)), bh), Nat.add(s, Nat.add(C.shift(32n, b3), bh)), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), NA.add_assoc(s, C.shift(32n, b3), bh), Equal.trans(Nat, Nat.add(s, Nat.add(C.shift(32n, b3), bh)), Nat.add(s, Nat.add(bh, C.shift(32n, b3))), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), Equal.cong(Nat, Nat, t => Nat.add(s, t), Nat.add(C.shift(32n, b3), bh), Nat.add(bh, C.shift(32n, b3)), N.add_comm(C.shift(32n, b3), bh)), Equal.trans(Nat, Nat.add(s, Nat.add(bh, C.shift(32n, b3))), Nat.add(Nat.add(s, bh), C.shift(32n, b3)), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), Equal.sym(Nat, Nat.add(Nat.add(s, bh), C.shift(32n, b3)), Nat.add(s, Nat.add(bh, C.shift(32n, b3))), NA.add_assoc(s, bh, C.shift(32n, b3))), Equal.trans(Nat, Nat.add(Nat.add(s, bh), C.shift(32n, b3)), Nat.add(Nat.add(ah, C.shift(32n, b2)), C.shift(32n, b3)), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(32n, b3)), Nat.add(s, bh), Nat.add(ah, C.shift(32n, b2)), e2), Equal.trans(Nat, Nat.add(Nat.add(ah, C.shift(32n, b2)), C.shift(32n, b3)), Nat.add(ah, Nat.add(C.shift(32n, b2), C.shift(32n, b3))), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), NA.add_assoc(ah, C.shift(32n, b2), C.shift(32n, b3)), Equal.cong(Nat, Nat, t => Nat.add(ah, t), Nat.add(C.shift(32n, b2), C.shift(32n, b3)), C.shift(32n, Nat.add(b2, b3)), Equal.sym(Nat, C.shift(32n, Nat.add(b2, b3)), Nat.add(C.shift(32n, b2), C.shift(32n, b3)), WW.shift_add(32n, b2, b3)))))))))))), Equal.trans(Nat, Nat.add(al, C.shift(32n, Nat.add(ah, C.shift(32n, Nat.add(b2, b3))))), Nat.add(al, Nat.add(C.shift(32n, ah), C.shift(32n, C.shift(32n, Nat.add(b2, b3))))), Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), Equal.cong(Nat, Nat, t => Nat.add(al, t), C.shift(32n, Nat.add(ah, C.shift(32n, Nat.add(b2, b3)))), Nat.add(C.shift(32n, ah), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), WW.shift_add(32n, ah, C.shift(32n, Nat.add(b2, b3)))), Equal.sym(Nat, Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), Nat.add(al, Nat.add(C.shift(32n, ah), C.shift(32n, C.shift(32n, Nat.add(b2, b3))))), NA.add_assoc(al, C.shift(32n, ah), C.shift(32n, C.shift(32n, Nat.add(b2, b3))))))))))))