---

Step * 3 3 of Lemma bm_T'_wf


1. T : Type
2. Key : Type
3. k : Key
4. v : T
5. key : Key
6. value : T
7. cnt : ℤ
8. left : binary_map(T;Key)
9. m7 : binary_map(T;Key)
10. ↑bm_cnt_prop(bm_T(key;value;cnt;left;m7))
11. k1 : Key
12. v1 : T
13. c1 : ℤ
14. ¬(bm_wt(c1) ≤ cnt)
15. ¬(bm_wt(cnt) ≤ c1)
16. l1 : binary_map(T;Key)
17. m12 : binary_map(T;Key)
18. ↑bm_cnt_prop(bm_T(k1;v1;c1;l1;m12))
⊢ bm_T(k;v;cnt + c1 + 1;bm_T(key;value;cnt;left;m7);bm_T(k1;v1;c1;l1;m12)) ∈ binary-map(T;Key)
BY
{ (MemTypeCD THEN Auto THEN BLemma `bm_cnt_prop_T` THEN Auto THEN RWO "bm_numItems_T" 0 THEN Auto) }

---

Latex:



1.  T  :  Type
2.  Key  :  Type
3.  k  :  Key
4.  v  :  T
5.  key  :  Key
6.  value  :  T
7.  cnt  :  \mBbbZ{}
8.  left  :  binary\_map(T;Key)
9.  m7  :  binary\_map(T;Key)
10.  \muparrow{}bm\_cnt\_prop(bm\_T(key;value;cnt;left;m7))
11.  k1  :  Key
12.  v1  :  T
13.  c1  :  \mBbbZ{}
14.  \mneg{}(bm\_wt(c1)  \mleq{}  cnt)
15.  \mneg{}(bm\_wt(cnt)  \mleq{}  c1)
16.  l1  :  binary\_map(T;Key)
17.  m12  :  binary\_map(T;Key)
18.  \muparrow{}bm\_cnt\_prop(bm\_T(k1;v1;c1;l1;m12))
\mvdash{}  bm\_T(k;v;cnt  +  c1  +  1;bm\_T(key;value;cnt;left;m7);bm\_T(k1;v1;c1;l1;m12))  \mmember{}  binary-map(T;Key)


By

(MemTypeCD  THEN  Auto  THEN  BLemma  `bm\_cnt\_prop\_T`  THEN  Auto  THEN  RWO  "bm\_numItems\_T"  0  THEN  Auto)

---

Home Index