---

Step * 2 1 of Lemma count_bounds


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

---

Latex:

---

Latex:

1.  s  :  DSet
2.  a  :  |s|
3.  u  :  |s|
4.  v  :  |s|  List
5.  (0  \mleq{}  (a  \#\mmember{}  v))  \mwedge{}  ((a  \#\mmember{}  v)  \mleq{}  ||v||)
6.  (0  \mleq{}  b2i(u  (=\msubb{})  a))  \mwedge{}  (b2i(u  (=\msubb{})  a)  \mleq{}  1)
\mvdash{}  (0  \mleq{}  (b2i(u  (=\msubb{})  a)  +  (a  \#\mmember{}  v)))  \mwedge{}  ((b2i(u  (=\msubb{})  a)  +  (a  \#\mmember{}  v))  \mleq{}  (||v||  +  1))


By

---

Latex:
Auto'

---

Home Index