def expand16

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64mul.bend:130

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

130# (al + 2^16 ah)(bl + 2^16 bh) == (al bl + 2^16 al bh) + (2^16 ah bl + 2^32 ah bh)
131def expand16(+al: Nat, +ah: Nat, +bl: Nat, +bh: Nat) -> {Nat.mul(Nat.add(al, WD.sc(16n, ah)), Nat.add(bl, WD.sc(16n, bh))) == Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))) : Nat}:
132  +b = Nat.add(bl, WD.sc(16n, bh))
133  +sa = WD.sc(16n, ah)
134  +sb = WD.sc(16n, bh)
135  +e6 = Equal.trans(Nat, Nat.mul(sa, sb), WD.sc(16n, Nat.mul(ah, sb)), WD.sc(32n, Nat.mul(ah, bh)), mul_sc_l(16n, ah, sb), Equal.trans(Nat, WD.sc(16n, Nat.mul(ah, sb)), WD.sc(16n, WD.sc(16n, Nat.mul(ah, bh))), WD.sc(32n, Nat.mul(ah, bh)), cong_sc(16n, Nat.mul(ah, sb), WD.sc(16n, Nat.mul(ah, bh)), mul_sc_r(16n, ah, bh)), sc_sc(16n, 16n, Nat.mul(ah, bh))))
136  +l1 = Nat.add(Nat.mul(al, b), Nat.mul(sa, b))
137  +l2 = Nat.add(Nat.add(Nat.mul(al, bl), Nat.mul(al, sb)), Nat.mul(sa, b))
138  +l3 = Nat.add(Nat.add(Nat.mul(al, bl), Nat.mul(al, sb)), Nat.add(Nat.mul(sa, bl), Nat.mul(sa, sb)))
139  +l4 = Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(Nat.mul(sa, bl), Nat.mul(sa, sb)))
140  +l5 = Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), Nat.mul(sa, sb)))
141  Equal.trans(Nat, Nat.mul(Nat.add(al, sa), b), l1, Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))), NA.mul_add_right(al, sa, b),
142    Equal.trans(Nat, l1, l2, Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))), cong_l(Nat.mul(al, b), Nat.add(Nat.mul(al, bl), Nat.mul(al, sb)), Nat.mul(sa, b), NA.mul_add_left(al, bl, sb)),
143      Equal.trans(Nat, l2, l3, Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))), cong_r(Nat.add(Nat.mul(al, bl), Nat.mul(al, sb)), Nat.mul(sa, b), Nat.add(Nat.mul(sa, bl), Nat.mul(sa, sb)), NA.mul_add_left(sa, bl, sb)),
144        Equal.trans(Nat, l3, l4, Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))), cong_l(Nat.add(Nat.mul(al, bl), Nat.mul(al, sb)), Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(Nat.mul(sa, bl), Nat.mul(sa, sb)), cong_r(Nat.mul(al, bl), Nat.mul(al, sb), WD.sc(16n, Nat.mul(al, bh)), mul_sc_r(16n, al, bh))),
145          Equal.trans(Nat, l4, l5, Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))), cong_r(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(Nat.mul(sa, bl), Nat.mul(sa, sb)), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), Nat.mul(sa, sb)), cong_l(Nat.mul(sa, bl), WD.sc(16n, Nat.mul(ah, bl)), Nat.mul(sa, sb), mul_sc_l(16n, ah, bl))),
146            cong_r(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), Nat.mul(sa, sb)), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh))), cong_r(WD.sc(16n, Nat.mul(ah, bl)), Nat.mul(sa, sb), WD.sc(32n, Nat.mul(ah, bh)), e6)))))))