def expand_k

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

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

406def expand_k(+k: Nat, +al: Nat, +ah: Nat, +bl: Nat, +bh: 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}:
407  Equal.trans(Nat, Nat.mul(Nat.add(al, C.shift(k, ah)), Nat.add(bl, C.shift(k, bh))), Nat.add(Nat.mul(al, Nat.add(bl, C.shift(k, bh))), Nat.mul(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))))), NA.mul_add_right(al, C.shift(k, ah), Nat.add(bl, C.shift(k, bh))), Equal.trans(Nat, Nat.add(Nat.mul(al, Nat.add(bl, C.shift(k, bh))), Nat.mul(C.shift(k, ah), Nat.add(bl, C.shift(k, bh)))), Nat.add(Nat.add(Nat.mul(al, bl), Nat.mul(al, C.shift(k, bh))), Nat.mul(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))))), Equal.cong(Nat, Nat, t => Nat.add(t, Nat.mul(C.shift(k, ah), Nat.add(bl, C.shift(k, bh)))), Nat.mul(al, Nat.add(bl, C.shift(k, bh))), Nat.add(Nat.mul(al, bl), Nat.mul(al, C.shift(k, bh))), NA.mul_add_left(al, bl, C.shift(k, bh))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(al, bl), Nat.mul(al, C.shift(k, bh))), Nat.mul(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.mul(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))))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(Nat.mul(al, bl), t), Nat.mul(C.shift(k, ah), Nat.add(bl, C.shift(k, bh)))), Nat.mul(al, C.shift(k, bh)), C.shift(k, Nat.mul(al, bh)), shift_mul_r(k, al, bh)), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), Nat.mul(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(Nat.mul(C.shift(k, ah), bl), Nat.mul(C.shift(k, ah), 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))))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), t), Nat.mul(C.shift(k, ah), Nat.add(bl, C.shift(k, bh))), Nat.add(Nat.mul(C.shift(k, ah), bl), Nat.mul(C.shift(k, ah), C.shift(k, bh))), NA.mul_add_left(C.shift(k, ah), bl, C.shift(k, bh))), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), Nat.add(Nat.mul(C.shift(k, ah), bl), Nat.mul(C.shift(k, ah), 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)), Nat.mul(C.shift(k, ah), 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))))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), Nat.add(t, Nat.mul(C.shift(k, ah), C.shift(k, bh)))), Nat.mul(C.shift(k, ah), bl), C.shift(k, Nat.mul(ah, bl)), shift_mul_l(k, ah, bl)), 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)), Nat.mul(C.shift(k, ah), 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, Nat.mul(ah, 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))))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(Nat.mul(al, bl), C.shift(k, Nat.mul(al, bh))), Nat.add(C.shift(k, Nat.mul(ah, bl)), t)), Nat.mul(C.shift(k, ah), C.shift(k, bh)), C.shift(k, Nat.mul(ah, C.shift(k, bh))), shift_mul_l(k, ah, C.shift(k, bh))), Equal.cong(Nat, Nat, t => 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, t))), Nat.mul(ah, C.shift(k, bh)), C.shift(k, Nat.mul(ah, bh)), shift_mul_r(k, ah, bh))))))))