---

Step * of Lemma bm_cnt_prop_T

∀[T,Key:Type]. ∀[key:Key]. ∀[value:T]. ∀[cnt:ℤ]. ∀[left,right:binary_map(T;Key)].
  uiff(↑bm_cnt_prop(bm_T(key;value;cnt;left;right));(cnt = (1 + bm_numItems(left) + bm_numItems(right)) ∈ ℤ)
  ∧ (↑bm_cnt_prop(left))
  ∧ (↑bm_cnt_prop(right)))
BY
{ (Auto
   THEN Try ((RepUR ``bm_cnt_prop`` (-1)
              THEN (RWO "bm_cnt_prop0_T" (-1) THENA Auto)
              THEN Reduce (-1)
              THEN (RWO "bm_numItems_is_cnt_prop0<" (-1) THENA Auto)
              THEN AllPushDown
              THEN Auto))
   THEN Try (Complete ((RepUR ``bm_cnt_prop`` 0 THEN Auto)))
   THEN RepUR ``bm_cnt_prop`` 0
   THEN (RWO "bm_cnt_prop0_T" 0 THENA Auto)
   THEN Reduce 0
   THEN (RWO "bm_numItems_is_cnt_prop0<" 0 THENA Auto)
   THEN AllPushDown
   THEN Auto
   THEN Fold `bm_cnt_prop` 0
   THEN Auto) }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[key:Key].  \mforall{}[value:T].  \mforall{}[cnt:\mBbbZ{}].  \mforall{}[left,right:binary\_map(T;Key)].
    uiff(\muparrow{}bm\_cnt\_prop(bm\_T(key;value;cnt;left;right));(cnt
                                                                                                        =  (1  +  bm\_numItems(left)  +  bm\_numItems(right)))
    \mwedge{}  (\muparrow{}bm\_cnt\_prop(left))
    \mwedge{}  (\muparrow{}bm\_cnt\_prop(right)))


By

(Auto
  THEN  Try  ((RepUR  ``bm\_cnt\_prop``  (-1)
                        THEN  (RWO  "bm\_cnt\_prop0\_T"  (-1)  THENA  Auto)
                        THEN  Reduce  (-1)
                        THEN  (RWO  "bm\_numItems\_is\_cnt\_prop0<"  (-1)  THENA  Auto)
                        THEN  AllPushDown
                        THEN  Auto))
  THEN  Try  (Complete  ((RepUR  ``bm\_cnt\_prop``  0  THEN  Auto)))
  THEN  RepUR  ``bm\_cnt\_prop``  0
  THEN  (RWO  "bm\_cnt\_prop0\_T"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RWO  "bm\_numItems\_is\_cnt\_prop0<"  0  THENA  Auto)
  THEN  AllPushDown
  THEN  Auto
  THEN  Fold  `bm\_cnt\_prop`  0
  THEN  Auto)

---

Home Index