---

Step * 1 of Lemma bag-member-count


1. T : Type
2. eq : EqDecider(T)
3. x : T
4. bs : bag(T)
5. x ↓∈ bs
⊢ 1 ≤ #([y∈bs|eq x y])
BY
{ (D -1
   THEN (Auto THEN Unhide THEN Auto)
   THEN D -1
   THEN Auto
   THEN RevHypSubst' (-2) 0
   THEN Auto
   THEN ThinVar `bs'
   THEN RepUR ``bag-size bag-filter`` 0)⋅ }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. L : T List
5. (x ∈ L)
⊢ 1 ≤ ||filter(λy.(eq x y);L)||

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  bs  :  bag(T)
5.  x  \mdownarrow{}\mmember{}  bs
\mvdash{}  1  \mleq{}  \#([y\mmember{}bs|eq  x  y])


By

---

Latex:
(D  -1
  THEN  (Auto  THEN  Unhide  THEN  Auto)
  THEN  D  -1
  THEN  Auto
  THEN  RevHypSubst'  (-2)  0
  THEN  Auto
  THEN  ThinVar  `bs'
  THEN  RepUR  ``bag-size  bag-filter``  0)\mcdot{}

---

Home Index