---

Step * of Lemma bm_numItems_is_cnt_prop0

∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  (bm_numItems(m) ~ fst(bm_cnt_prop0(m)))
BY
{ (Auto
   THEN BinaryMapCase (-1)
   THEN Try ((RWO "bm_numItems_E" 0 THENA Auto))
   THEN Try ((RWO "bm_cnt_prop0_E" 0 THENA Auto))
   THEN Try ((RWO "bm_numItems_T" 0 THENA Auto))
   THEN Try ((RWO "bm_cnt_prop0_T" 0 THENA Auto))
   THEN Reduce 0
   THEN Auto) }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[m:binary\_map(T;Key)].    (bm\_numItems(m)  \msim{}  fst(bm\_cnt\_prop0(m)))


By

(Auto
  THEN  BinaryMapCase  (-1)
  THEN  Try  ((RWO  "bm\_numItems\_E"  0  THENA  Auto))
  THEN  Try  ((RWO  "bm\_cnt\_prop0\_E"  0  THENA  Auto))
  THEN  Try  ((RWO  "bm\_numItems\_T"  0  THENA  Auto))
  THEN  Try  ((RWO  "bm\_cnt\_prop0\_T"  0  THENA  Auto))
  THEN  Reduce  0
  THEN  Auto)

---

Home Index