---

Step * of Lemma bag-combine-append-empty

∀[f,bs:Top].  (⋃x∈bs.f[x] @ [] ~ ⋃x∈bs.f[x])
BY
{ (Auto
   THEN RepUR ``bag-combine bag-union bag-map`` 0
   THEN (Subst ⌜[] ~ concat([])⌝ 0⋅ THENA (Reduce 0 THEN Auto))
   THEN (RWO "concat_append<" 0 THENA Auto)
   THEN RWO "map-append-empty" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f,bs:Top].    (\mcup{}x\mmember{}bs.f[x]  @  []  \msim{}  \mcup{}x\mmember{}bs.f[x])


By

---

Latex:
(Auto
  THEN  RepUR  ``bag-combine  bag-union  bag-map``  0
  THEN  (Subst  \mkleeneopen{}[]  \msim{}  concat([])\mkleeneclose{}  0\mcdot{}  THENA  (Reduce  0  THEN  Auto))
  THEN  (RWO  "concat\_append<"  0  THENA  Auto)
  THEN  RWO  "map-append-empty"  0
  THEN  Auto)

---

Home Index