---

Step * 2 2 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. k1 : Key
9. v1 : T
10. c1 : ℤ
11. left : binary_map(T;Key)
12. m12 : binary_map(T;Key)
13. cnt = (1 + 0 + c1) ∈ ℤ
14. ↑bm_cnt_prop(bm_T(k1;v1;c1;left;m12))
⊢ bm_double_R(k;v;bm_T(key;value;cnt;bm_E();bm_T(k1;v1;c1;left;m12));bm_E()) ∈ binary-map(T;Key)
BY
{ (Auto
   THEN Try (Complete ((MemTypeCD THEN Auto THEN Reduce 0 THEN Auto)))
   THEN MemTypeCD
   THEN Auto
   THEN BLemma `bm_cnt_prop_T`
   THEN Reduce 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.  k1  :  Key
9.  v1  :  T
10.  c1  :  \mBbbZ{}
11.  left  :  binary\_map(T;Key)
12.  m12  :  binary\_map(T;Key)
13.  cnt  =  (1  +  0  +  c1)
14.  \muparrow{}bm\_cnt\_prop(bm\_T(k1;v1;c1;left;m12))
\mvdash{}  bm\_double\_R(k;v;bm\_T(key;value;cnt;bm\_E();bm\_T(k1;v1;c1;left;m12));bm\_E())  \mmember{}  binary-map(T;Key)


By

(Auto
  THEN  Try  (Complete  ((MemTypeCD  THEN  Auto  THEN  Reduce  0  THEN  Auto)))
  THEN  MemTypeCD
  THEN  Auto
  THEN  BLemma  `bm\_cnt\_prop\_T`
  THEN  Reduce  0
  THEN  Auto)

---

Home Index