---

Step * of Lemma bag-combine-combine

∀[A,B,C:Type]. ∀[b:bag(A)]. ∀[f:A ⟶ bag(B)]. ∀[g:B ⟶ bag(C)].  (⋃x∈⋃y∈b.f[y].g[x] = ⋃x∈b.⋃y∈f[x].g[y] ∈ bag(C))
BY
{ (Auto
   THEN (BagInd (-3) THENA Auto)
   THEN Try (Fold `empty-bag` 0)
   THEN Reduce 0
   THEN Auto
   THEN Try (Fold `cons-bag` 0)
   THEN (RWO "bag-combine-cons-left" 0 THENA Auto)
   THEN (RWO "bag-combine-append-left" 0 THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[b:bag(A)].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].  \mforall{}[g:B  {}\mrightarrow{}  bag(C)].
    (\mcup{}x\mmember{}\mcup{}y\mmember{}b.f[y].g[x]  =  \mcup{}x\mmember{}b.\mcup{}y\mmember{}f[x].g[y])


By

---

Latex:
(Auto
  THEN  (BagInd  (-3)  THENA  Auto)
  THEN  Try  (Fold  `empty-bag`  0)
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  (Fold  `cons-bag`  0)
  THEN  (RWO  "bag-combine-cons-left"  0  THENA  Auto)
  THEN  (RWO  "bag-combine-append-left"  0  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index