---

Step * 2 of Lemma non-empty-bag-union-of-list


1. [T] : Type
2. u : bag(T)
3. v : bag(T) List
4. 0 < #(bag-union(v)) ⇐⇒ (∃b∈v. 0 < #(b))
⊢ 0 < #(bag-union([u / v])) ⇐⇒ (∃b∈[u / v]. 0 < #(b))
BY
{ (RepUR ``bag-union bag-size concat`` 0⋅
   THEN Fold `concat` 0
   THEN Fold `bag-union` 0
   THEN Folds ``bag-append bag-size`` 0
   THEN (Assert v ∈ bag(bag(T)) BY
               (DoSubsume THEN Auto THEN BLemma `list-subtype-bag` THEN Auto))
   THEN (RWO "bag-size-append l_exists_cons" 0 THENA Auto)) }

1
1. [T] : Type
2. u : bag(T)
3. v : bag(T) List
4. 0 < #(bag-union(v)) ⇐⇒ (∃b∈v. 0 < #(b))
5. v ∈ bag(bag(T))
⊢ 0 < #(u) + #(bag-union(v)) ⇐⇒ 0 < #(u) ∨ (∃b∈v. 0 < #(b))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  u  :  bag(T)
3.  v  :  bag(T)  List
4.  0  <  \#(bag-union(v))  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}b\mmember{}v.  0  <  \#(b))
\mvdash{}  0  <  \#(bag-union([u  /  v]))  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}b\mmember{}[u  /  v].  0  <  \#(b))


By

---

Latex:
(RepUR  ``bag-union  bag-size  concat``  0\mcdot{}
  THEN  Fold  `concat`  0
  THEN  Fold  `bag-union`  0
  THEN  Folds  ``bag-append  bag-size``  0
  THEN  (Assert  v  \mmember{}  bag(bag(T))  BY
                          (DoSubsume  THEN  Auto  THEN  BLemma  `list-subtype-bag`  THEN  Auto))
  THEN  (RWO  "bag-size-append  l\_exists\_cons"  0  THENA  Auto))

---

Home Index