---

Step * of Lemma bm_count_prop

∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  bm_numItems(m) = bm_count(m) ∈ ℤ supposing ↑bm_cnt_prop(m)
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN InstLemma `binary_map-induction` [⌜T⌝;⌜Key⌝;⌜λ2m.bm_numItems(m) = bm_count(m) ∈ ℤ supposing ↑bm_cnt_prop(m)⌝]⋅
   THEN Auto
   THEN Try ((RWO "bm_numItems_E" 0 THENA Auto))
   THEN Try ((RWO "bm_count_E" 0 THENA Auto))
   THEN Try ((RWO "bm_cnt_prop_E" 0 THENA Auto))
   THEN Try (Complete (Auto))
   THEN Try ((RWO "bm_numItems_T" 0 THENA Auto))
   THEN Try ((RWO "bm_count_T" 0 THENA Auto))
   THEN Try ((RWO "bm_numItems_T" (-1) THENA Auto))
   THEN (RWO "bm_cnt_prop_T" (-1) THENA Auto)
   THEN RepD
   THEN (RWO "-4" (-3) THENA Auto)
   THEN RWO "-5" (-3)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,Key:Type].  \mforall{}[m:binary\_map(T;Key)].    bm\_numItems(m)  =  bm\_count(m)  supposing  \muparrow{}bm\_cnt\_prop(m)


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  InstLemma  `binary\_map-induction`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}Key\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}m.bm\_numItems(m)  =  bm\_count(m) 
                                                                                                              supposing  \muparrow{}bm\_cnt\_prop(m)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((RWO  "bm\_numItems\_E"  0  THENA  Auto))
  THEN  Try  ((RWO  "bm\_count\_E"  0  THENA  Auto))
  THEN  Try  ((RWO  "bm\_cnt\_prop\_E"  0  THENA  Auto))
  THEN  Try  (Complete  (Auto))
  THEN  Try  ((RWO  "bm\_numItems\_T"  0  THENA  Auto))
  THEN  Try  ((RWO  "bm\_count\_T"  0  THENA  Auto))
  THEN  Try  ((RWO  "bm\_numItems\_T"  (-1)  THENA  Auto))
  THEN  (RWO  "bm\_cnt\_prop\_T"  (-1)  THENA  Auto)
  THEN  RepD
  THEN  (RWO  "-4"  (-3)  THENA  Auto)
  THEN  RWO  "-5"  (-3)
  THEN  Auto)

---

Home Index