---

Step * of Lemma bm_count_prop_pos

∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  (0 ≤ bm_count(m))
BY
{ (Auto
   THEN InstLemma `binary_map-induction` [⌈T⌉;⌈Key⌉;⌈λ2m.0 ≤ bm_count(m)⌉]⋅
   THEN AllReduce
   THEN Auto
   THEN RWO "bm_count_T" 0
   THEN Auto') }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[m:binary\_map(T;Key)].    (0  \mleq{}  bm\_count(m))


By

(Auto
  THEN  InstLemma  `binary\_map-induction`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}Key\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}m.0  \mleq{}  bm\_count(m)\mkleeneclose{}]\mcdot{}
  THEN  AllReduce
  THEN  Auto
  THEN  RWO  "bm\_count\_T"  0
  THEN  Auto')

---

Home Index