---

Step * of Lemma bag-union-union-as-combine

∀[X:Type]. ∀[x:bag(bag(bag(X)))].  (bag-union(bag-union(x)) = ⋃z∈x.bag-union(z) ∈ bag(X))
BY
{ (xxxAutoxxx
   THEN Unfold `bag-combine` 0
   THEN (RWO "bag-union-as-combine" 0 THENA Auto)
   THEN (RWO "bag-union-as-combine" 0 THENA Auto)
   THEN (RWO "bag-combine-assoc" 0 THENA Auto)
   THEN (RWO "bag-combine-map" 0 THENA Auto)
   THEN Reduce 0
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[x:bag(bag(bag(X)))].    (bag-union(bag-union(x))  =  \mcup{}z\mmember{}x.bag-union(z))


By

---

Latex:
(xxxAutoxxx
  THEN  Unfold  `bag-combine`  0
  THEN  (RWO  "bag-union-as-combine"  0  THENA  Auto)
  THEN  (RWO  "bag-union-as-combine"  0  THENA  Auto)
  THEN  (RWO  "bag-combine-assoc"  0  THENA  Auto)
  THEN  (RWO  "bag-combine-map"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  EqCD
  THEN  Auto)

---

Home Index