---

Step * 2 of Lemma count_bounds


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))
BY
{ (InstLemma `b2i_bounds` [u (=b) a] THENA Auto) }

1
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))

---

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||)
\mvdash{}  (0  \mleq{}  (b2i(u  (=\msubb{})  a)  +  (a  \#\mmember{}  v)))  \mwedge{}  ((b2i(u  (=\msubb{})  a)  +  (a  \#\mmember{}  v))  \mleq{}  (||v||  +  1))


By

---

Latex:
(InstLemma  `b2i\_bounds`  [u  (=\msubb{})  a]  THENA  Auto)

---

Home Index