---

Step * 2 1 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. cnt = 1 ∈ ℤ
⊢ bm_T(k;v;2;bm_T(key;value;cnt;bm_E();bm_E());bm_E()) ∈ binary-map(T;Key)
BY
{ (MemTypeCD THEN Auto THEN RepeatFor 2 ((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.  cnt  =  1
\mvdash{}  bm\_T(k;v;2;bm\_T(key;value;cnt;bm\_E();bm\_E());bm\_E())  \mmember{}  binary-map(T;Key)


By

(MemTypeCD  THEN  Auto  THEN  RepeatFor  2  ((BLemma  `bm\_cnt\_prop\_T`  THEN  Reduce  0  THEN  Auto)))

---

Home Index