---

Step * 1 1 2 of Lemma empty-bag-iff-size


1. T : Type
2. bs : bag(T)
3. #(bs) ≤ 0
4. x : T
⊢ ¬x ↓∈ bs
BY
{ ((D 0 THENA Auto) THEN Assert ⌜0 < #(bs)⌝⋅ THEN Auto) }

1
.....assertion..... 
1. T : Type
2. bs : bag(T)
3. #(bs) ≤ 0
4. x : T
5. x ↓∈ bs
⊢ 0 < #(bs)

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  bag(T)
3.  \#(bs)  \mleq{}  0
4.  x  :  T
\mvdash{}  \mneg{}x  \mdownarrow{}\mmember{}  bs


By

---

Latex:
((D  0  THENA  Auto)  THEN  Assert  \mkleeneopen{}0  <  \#(bs)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index