---

Step * of Lemma bag-count-member

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b:bag(T)].  uiff(1 ≤ (#x in b);x ↓∈ b)
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "bag-count-sqequal" 0 THENA Auto)
   THEN D 0
   THEN Auto
   THEN (BagToList (-2) THENA Auto)) }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. b : T List
5. 1 ≤ #([y∈b|eq x y])
⊢ x ↓∈ b

2
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. b : T List
5. x ↓∈ b
⊢ 1 ≤ #([y∈b|eq x y])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[b:bag(T)].    uiff(1  \mleq{}  (\#x  in  b);x  \mdownarrow{}\mmember{}  b)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "bag-count-sqequal"  0  THENA  Auto)
  THEN  D  0
  THEN  Auto
  THEN  (BagToList  (-2)  THENA  Auto))

---

Home Index