---

Step * of Lemma bag-count-is-zero

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  (#x in bs) ~ 0 supposing ¬x ↓∈ bs
BY
{ (Auto THEN (InstLemma `bag-member-count` [⌜T⌝;⌜eq⌝;⌜x⌝;⌜bs⌝]⋅ THENA Auto)) }

1
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 ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[bs:bag(T)].    (\#x  in  bs)  \msim{}  0  supposing  \mneg{}x  \mdownarrow{}\mmember{}  bs


By

---

Latex:
(Auto  THEN  (InstLemma  `bag-member-count`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index