---

Step * 2 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. v ∈ bag(bag(T))
⊢ 0 < #(u) + #(bag-union(v)) ⇐⇒ 0 < #(u) ∨ (∃b∈v. 0 < #(b))
BY
{ (Auto THEN SplitOrHyps THEN ThinTrivial THEN Auto') }

1
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))

---

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))
5.  v  \mmember{}  bag(bag(T))
\mvdash{}  0  <  \#(u)  +  \#(bag-union(v))  \mLeftarrow{}{}\mRightarrow{}  0  <  \#(u)  \mvee{}  (\mexists{}b\mmember{}v.  0  <  \#(b))


By

---

Latex:
(Auto  THEN  SplitOrHyps  THEN  ThinTrivial  THEN  Auto')

---

Home Index