---

Step * 2 1 1 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))
5. 0 < #(bag-union(v)) ⇐ (∃b∈v. 0 < #(b))
6. v ∈ bag(bag(T))
7. 0 < #(u) + #(bag-union(v))
⊢ 0 < #(u) ∨ (∃b∈v. 0 < #(b))
BY
{ (Decide ⌜0 < #(u)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Decide  \mkleeneopen{}0  <  \#(u)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index