---

Step * of Lemma bag-union-bagp

∀[T:Type]. ∀[bbs:bag(bag(T))].  (0 < #([b∈bbs|0 <z #(b)]) ⇒ (bag-union(bbs) ∈ T Bag+))
BY
{ (Auto
   THEN Reduce 0
   THEN Auto
   THEN MemTypeCD
   THEN Auto
   THEN (BagInd 2 THENA Auto)
   THEN Folds ``empty-bag cons-bag`` 0
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN (RWW "bag-size-append" 0 THENA Auto)
   THEN AutoSplit
   THEN (Auto THEN Auto' THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bbs:bag(bag(T))].    (0  <  \#([b\mmember{}bbs|0  <z  \#(b)])  {}\mRightarrow{}  (bag-union(bbs)  \mmember{}  T  Bag\msupplus{}))


By

---

Latex:
(Auto
  THEN  Reduce  0
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  (BagInd  2  THENA  Auto)
  THEN  Folds  ``empty-bag  cons-bag``  0
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  (RWW  "bag-size-append"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  (Auto  THEN  Auto'  THEN  Auto)\mcdot{})

---

Home Index