---

Step * of Lemma bm_count_T

∀[key,value,cnt,left,right:Top].  (bm_count(bm_T(key;value;cnt;left;right)) ~ 1 + bm_count(left) + bm_count(right))
BY
{ (RepUR ``bm_count`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[key,value,cnt,left,right:Top].
    (bm\_count(bm\_T(key;value;cnt;left;right))  \msim{}  1  +  bm\_count(left)  +  bm\_count(right))


By

---

Latex:
(RepUR  ``bm\_count``  0  THEN  Auto)

---

Home Index