---

Step * 1 of Lemma bm_count_prop_pos


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))
BY
{ (RWO "bm_count_T" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  Key  :  Type
3.  m  :  binary\_map(T;Key)
4.  key  :  Key@i
5.  value  :  T@i
6.  cnt  :  \mBbbZ{}@i
7.  left  :  binary\_map(T;Key)@i
8.  right  :  binary\_map(T;Key)@i
9.  0  \mleq{}  bm\_count(left)@i
10.  0  \mleq{}  bm\_count(right)@i
\mvdash{}  0  \mleq{}  bm\_count(bm\_T(key;value;cnt;left;right))


By

---

Latex:
(RWO  "bm\_count\_T"  0  THEN  Auto)

---

Home Index