---

Step * of Lemma bm_count_prop_pos

∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  (0 ≤ bm_count(m))
BY
{ ((UnivCD THENA Auto)
   THEN InstLemma `binary_map-induction` [⌜T⌝;⌜Key⌝;⌜λ2m.0 ≤ bm_count(m)⌝]⋅
   THEN Auto
   THEN AllReduce
   THEN Auto) }

1
1. T : Type
2. Key : Type
3. m : binary_map(T;Key)
4. key : Key@i
5. value : T@i
6. cnt : ℤ@i
7. left : binary_map(T;Key)@i
8. right : binary_map(T;Key)@i
9. 0 ≤ bm_count(left)@i
10. 0 ≤ bm_count(right)@i
⊢ 0 ≤ bm_count(bm_T(key;value;cnt;left;right))

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  InstLemma  `binary\_map-induction`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}Key\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}m.0  \mleq{}  bm\_count(m)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  AllReduce
  THEN  Auto)

---

Home Index