---

Step * of Lemma count_bounds

∀s:DSet. ∀a:|s|. ∀bs:|s| List.  ((0 ≤ (a #∈ bs)) ∧ ((a #∈ bs) ≤ ||bs||))
BY
{ (((UnivCD THENA Auto) THEN ListInd (-1)) THEN AbReduce 0) }

1
1. s : DSet
2. a : |s|
⊢ (0 ≤ 0) ∧ (0 ≤ 0)

2
1. s : DSet
2. a : |s|
3. u : |s|
4. v : |s| List
5. (0 ≤ (a #∈ v)) ∧ ((a #∈ v) ≤ ||v||)
⊢ (0 ≤ (b2i(u (=b) a) + (a #∈ v))) ∧ ((b2i(u (=b) a) + (a #∈ v)) ≤ (||v|| + 1))

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a:|s|.  \mforall{}bs:|s|  List.    ((0  \mleq{}  (a  \#\mmember{}  bs))  \mwedge{}  ((a  \#\mmember{}  bs)  \mleq{}  ||bs||))


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  ListInd  (-1))  THEN  AbReduce  0)

---

Home Index