---

Step * of Lemma int-bag-sum-append

∀[b1,b2:bag(ℤ)].  (Σ(b1 + b2) ~ Σ(b1) + Σ(b2))
BY
{ (Auto
   THEN RepUR ``int-bag-sum`` 0
   THEN (RWO "bag-summation-append" 0 THEN Auto)
   THEN Reduce 0
   THEN Auto
   THEN RepeatFor 2 ((D 0 THEN Reduce 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[b1,b2:bag(\mBbbZ{})].    (\mSigma{}(b1  +  b2)  \msim{}  \mSigma{}(b1)  +  \mSigma{}(b2))


By

---

Latex:
(Auto
  THEN  RepUR  ``int-bag-sum``  0
  THEN  (RWO  "bag-summation-append"  0  THEN  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  RepeatFor  2  ((D  0  THEN  Reduce  0  THEN  Auto)))

---

Home Index