---

Step * of Lemma bm_numItems_T_reduce_lemma

∀right,left,cnt,value,key:Top.  (bm_numItems(bm_T(key;value;cnt;left;right)) ~ cnt)
BY
{ ((UnivCD THENA Auto) THEN Unfold `bm_numItems` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}right,left,cnt,value,key:Top.    (bm\_numItems(bm\_T(key;value;cnt;left;right))  \msim{}  cnt)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `bm\_numItems`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index