---

Step * of Lemma bag-combine-append-left

∀[A,B:Type]. ∀[ba,bb:bag(A)]. ∀[f:A ⟶ bag(B)].  (⋃x∈ba + bb.f[x] = (⋃x∈ba.f[x] + ⋃x∈bb.f[x]) ∈ bag(B))
BY
{ (Auto
   THEN RepUR ``bag-combine`` 0
   THEN (RWO "bag-map-append" 0 THENA Auto)
   THEN (BagToList (-2) THENA Auto)
   THEN (BagToList (-3) THENA Auto)
   THEN RepUR ``bag-map bag-union bag-append`` 0
   THEN (RWO "concat_append" 0 THENA Auto)
   THEN Try (Fold `bag-map` 0)
   THEN Try (Fold `bag-union` 0)
   THEN Try (Fold `bag-append` 0)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[ba,bb:bag(A)].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].    (\mcup{}x\mmember{}ba  +  bb.f[x]  =  (\mcup{}x\mmember{}ba.f[x]  +  \mcup{}x\mmember{}bb.f[x]))


By

---

Latex:
(Auto
  THEN  RepUR  ``bag-combine``  0
  THEN  (RWO  "bag-map-append"  0  THENA  Auto)
  THEN  (BagToList  (-2)  THENA  Auto)
  THEN  (BagToList  (-3)  THENA  Auto)
  THEN  RepUR  ``bag-map  bag-union  bag-append``  0
  THEN  (RWO  "concat\_append"  0  THENA  Auto)
  THEN  Try  (Fold  `bag-map`  0)
  THEN  Try  (Fold  `bag-union`  0)
  THEN  Try  (Fold  `bag-append`  0)
  THEN  Auto)

---

Home Index