---

Step * 1 of Lemma bag-count-is-zero


1. T : Type
2. eq : EqDecider(T)
3. x : T
4. bs : bag(T)
5. ¬x ↓∈ bs
6. uiff(x ↓∈ bs;1 ≤ (#x in bs))
⊢ (#x in bs) = 0 ∈ ℕ
BY
{ (RWO "-1" (-2) THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  bs  :  bag(T)
5.  \mneg{}x  \mdownarrow{}\mmember{}  bs
6.  uiff(x  \mdownarrow{}\mmember{}  bs;1  \mleq{}  (\#x  in  bs))
\mvdash{}  (\#x  in  bs)  =  0


By

---

Latex:
(RWO  "-1"  (-2)  THEN  Auto')

---

Home Index