---

Step * of Lemma bm_cnt_prop0_T

∀[key,value,cnt,left,right:Top].
  (bm_cnt_prop0(bm_T(key;value;cnt;left;right)) ~ <cnt
                                                  , (cnt =z 1 + (fst(bm_cnt_prop0(left))) + (fst(bm_cnt_prop0(right))))
                                                    ∧b (snd(bm_cnt_prop0(left)))
                                                    ∧b (snd(bm_cnt_prop0(right)))
                                                  >)
BY
{ (RepUR ``bm_cnt_prop0`` 0 THEN Auto) }

---

Latex:


\mforall{}[key,value,cnt,left,right:Top].
    (bm\_cnt\_prop0(bm\_T(key;value;cnt;left;right))  \msim{}  <cnt
                                                                                                    ,  (cnt  =\msubz{}  1
                                                                                                        +  (fst(bm\_cnt\_prop0(left)))
                                                                                                        +  (fst(bm\_cnt\_prop0(right))))
                                                                                                        \mwedge{}\msubb{}  (snd(bm\_cnt\_prop0(left)))
                                                                                                        \mwedge{}\msubb{}  (snd(bm\_cnt\_prop0(right)))
                                                                                                    >)


By

(RepUR  ``bm\_cnt\_prop0``  0  THEN  Auto)

---

Home Index