---

Step * 2 1 1 2 1 1 1 of Lemma bag-member-parts'


1. T : Type
2. eq : EqDecider(T)
3. x : T
4. c : bag(T)
⊢ ((#x in c) = 0 ∈ ℤ) ⇒ (¬x ↓∈ c)
BY
{ ((Auto THEN D 0 THEN Auto)
   THEN InstLemma `bag-member-count` [⌜T⌝;⌜eq⌝;⌜x⌝;⌜c⌝]⋅
   THEN Auto
   THEN ThinTrivial
   THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  c  :  bag(T)
\mvdash{}  ((\#x  in  c)  =  0)  {}\mRightarrow{}  (\mneg{}x  \mdownarrow{}\mmember{}  c)


By

---

Latex:
((Auto  THEN  D  0  THEN  Auto)
  THEN  InstLemma  `bag-member-count`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  ThinTrivial
  THEN  Auto')

---

Home Index