def mul_k

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/width.bend:409

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

409# (al + 2^k ah)(bl + 2^k bh) == al bl + 2^k t + 2^(2k) (kc + ah bh) when al bh + ah bl == t + 2^k kc
410def mul_k(+k: Nat, +al: Nat, +ah: Nat, +bl: Nat, +bh: Nat, +t: Nat, +kc: Nat, +e: {Nat.add(t, C.shift(k, kc)) == Nat.add(Nat.mul(al, bh), Nat.mul(ah, bl)) : Nat}) -> {Nat.mul(Nat.add(al, C.shift(k, ah)), Nat.add(bl, C.shift(k, bh))) == Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, t)), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh))))) : Nat}:
411  Equal.trans(Nat, Nat.mul(Nat.add(al, C.shift(k, ah)), Nat.add(bl, C.shift(k, bh))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, t)), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh))))), expand_k(k, al, ah, bl, bh), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, Nat.mul(al, bh)), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh)))))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, t)), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh))))), NA.add_assoc(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh)), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Equal.trans(Nat, Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, Nat.mul(al, bh)), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh)))))), Nat.add(Nat.mul(al, bl), Nat.add(Nat.add(C.shift(k, Nat.mul(al, bh)), C.shift(k, Nat.mul(ah, bl))), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, t)), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(al, bl), z), Nat.add(C.shift(k, Nat.mul(al, bh)), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(Nat.add(C.shift(k, Nat.mul(al, bh)), C.shift(k, Nat.mul(ah, bl))), C.shift(k, C.shift(k, Nat.mul(ah, bh)))), Equal.sym(Nat, Nat.add(Nat.add(C.shift(k, Nat.mul(al, bh)), C.shift(k, Nat.mul(ah, bl))), C.shift(k, C.shift(k, Nat.mul(ah, bh)))), Nat.add(C.shift(k, Nat.mul(al, bh)), Nat.add(C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), NA.add_assoc(C.shift(k, Nat.mul(al, bh)), C.shift(k, Nat.mul(ah, bl)), C.shift(k, C.shift(k, Nat.mul(ah, bh)))))), Equal.trans(Nat, Nat.add(Nat.mul(al, bl), Nat.add(Nat.add(C.shift(k, Nat.mul(al, bh)), C.shift(k, Nat.mul(ah, bl))), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, Nat.add(Nat.mul(al, bh), Nat.mul(ah, bl))), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, t)), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(al, bl), Nat.add(z, C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(C.shift(k, Nat.mul(al, bh)), C.shift(k, Nat.mul(ah, bl))), C.shift(k, Nat.add(Nat.mul(al, bh), Nat.mul(ah, bl))), Equal.sym(Nat, C.shift(k, Nat.add(Nat.mul(al, bh), Nat.mul(ah, bl))), Nat.add(C.shift(k, Nat.mul(al, bh)), C.shift(k, Nat.mul(ah, bl))), shift_add(k, Nat.mul(al, bh), Nat.mul(ah, bl)))), Equal.trans(Nat, Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, Nat.add(Nat.mul(al, bh), Nat.mul(ah, bl))), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, Nat.add(t, C.shift(k, kc))), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, t)), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, z), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(Nat.mul(al, bh), Nat.mul(ah, bl)), Nat.add(t, C.shift(k, kc)), Equal.sym(Nat, Nat.add(t, C.shift(k, kc)), Nat.add(Nat.mul(al, bh), Nat.mul(ah, bl)), e)), Equal.trans(Nat, Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, Nat.add(t, C.shift(k, kc))), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(Nat.mul(al, bl), Nat.add(Nat.add(C.shift(k, t), C.shift(k, C.shift(k, kc))), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, t)), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(al, bl), Nat.add(z, C.shift(k, C.shift(k, Nat.mul(ah, bh))))), C.shift(k, Nat.add(t, C.shift(k, kc))), Nat.add(C.shift(k, t), C.shift(k, C.shift(k, kc))), shift_add(k, t, C.shift(k, kc))), Equal.trans(Nat, Nat.add(Nat.mul(al, bl), Nat.add(Nat.add(C.shift(k, t), C.shift(k, C.shift(k, kc))), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, t), Nat.add(C.shift(k, C.shift(k, kc)), C.shift(k, C.shift(k, Nat.mul(ah, bh)))))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, t)), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(al, bl), z), Nat.add(Nat.add(C.shift(k, t), C.shift(k, C.shift(k, kc))), C.shift(k, C.shift(k, Nat.mul(ah, bh)))), Nat.add(C.shift(k, t), Nat.add(C.shift(k, C.shift(k, kc)), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), NA.add_assoc(C.shift(k, t), C.shift(k, C.shift(k, kc)), C.shift(k, C.shift(k, Nat.mul(ah, bh))))), Equal.trans(Nat, Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, t), Nat.add(C.shift(k, C.shift(k, kc)), C.shift(k, C.shift(k, Nat.mul(ah, bh)))))), Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, t), C.shift(k, Nat.add(C.shift(k, kc), C.shift(k, Nat.mul(ah, bh)))))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, t)), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, t), z)), Nat.add(C.shift(k, C.shift(k, kc)), C.shift(k, C.shift(k, Nat.mul(ah, bh)))), C.shift(k, Nat.add(C.shift(k, kc), C.shift(k, Nat.mul(ah, bh)))), Equal.sym(Nat, C.shift(k, Nat.add(C.shift(k, kc), C.shift(k, Nat.mul(ah, bh)))), Nat.add(C.shift(k, C.shift(k, kc)), C.shift(k, C.shift(k, Nat.mul(ah, bh)))), shift_add(k, C.shift(k, kc), C.shift(k, Nat.mul(ah, bh))))), Equal.trans(Nat, Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, t), C.shift(k, Nat.add(C.shift(k, kc), C.shift(k, Nat.mul(ah, bh)))))), Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, t), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh)))))), Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, t)), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, t), C.shift(k, z))), Nat.add(C.shift(k, kc), C.shift(k, Nat.mul(ah, bh))), C.shift(k, Nat.add(kc, Nat.mul(ah, bh))), Equal.sym(Nat, C.shift(k, Nat.add(kc, Nat.mul(ah, bh))), Nat.add(C.shift(k, kc), C.shift(k, Nat.mul(ah, bh))), shift_add(k, kc, Nat.mul(ah, bh)))), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, t)), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh))))), Nat.add(Nat.mul(al, bl), Nat.add(C.shift(k, t), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh)))))), NA.add_assoc(Nat.mul(al, bl), C.shift(k, t), C.shift(k, C.shift(k, Nat.add(kc, Nat.mul(ah, bh)))))))))))))))