---

Step * 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. left : binary_map(T;Key)
9. m7 : binary_map(T;Key)
10. ↑bm_cnt_prop(bm_T(key;value;cnt;left;m7))
⊢ binary_map_case(left;binary_map_case(m7;bm_T(k;v;2;bm_E();bm_T(key;value;cnt;left;m7));
                                       key2r,value2r,cnt2r,left2r,right2r.
                                       bm_single_L(k;v;bm_E();bm_T(key;value;cnt;left;m7)));
                  key2l,value2l,cnt2l,left2l,right2l.
                  binary_map_case(m7;bm_double_L(k;v;bm_E();bm_T(key;value;cnt;left;m7));
                                  key2r,value2r,cnt2r,left2r,right2r.if cnt2l <z cnt2r
                                  then bm_single_L(k;v;bm_E();bm_T(key;value;cnt;left;m7))
                                  else bm_double_L(k;v;bm_E();bm_T(key;value;cnt;left;m7))
                                  fi )) ∈ binary-map(T;Key)
BY
{ ((RWO "bm_cnt_prop_T" (-1) THENA Auto) THEN RepD) }

1
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. cnt = (1 + bm_numItems(left) + bm_numItems(m7)) ∈ ℤ
11. ↑bm_cnt_prop(left)
12. ↑bm_cnt_prop(m7)
⊢ binary_map_case(left;binary_map_case(m7;bm_T(k;v;2;bm_E();bm_T(key;value;cnt;left;m7));
                                       key2r,value2r,cnt2r,left2r,right2r.
                                       bm_single_L(k;v;bm_E();bm_T(key;value;cnt;left;m7)));
                  key2l,value2l,cnt2l,left2l,right2l.
                  binary_map_case(m7;bm_double_L(k;v;bm_E();bm_T(key;value;cnt;left;m7));
                                  key2r,value2r,cnt2r,left2r,right2r.if cnt2l <z cnt2r
                                  then bm_single_L(k;v;bm_E();bm_T(key;value;cnt;left;m7))
                                  else bm_double_L(k;v;bm_E();bm_T(key;value;cnt;left;m7))
                                  fi )) ∈ binary-map(T;Key)

---

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))
\mvdash{}  binary\_map\_case(left;binary\_map\_case(m7;bm\_T(k;v;2;bm\_E();bm\_T(key;value;cnt;left;m7));
                                                                              key2r,value2r,cnt2r,left2r,right2r.
                                                                              bm\_single\_L(k;v;bm\_E();bm\_T(key;value;cnt;left;m7)));
                                    key2l,value2l,cnt2l,left2l,right2l.
                                    binary\_map\_case(m7;bm\_double\_L(k;v;bm\_E();bm\_T(key;value;cnt;left;m7));
                                                                    key2r,value2r,cnt2r,left2r,right2r.if  cnt2l  <z  cnt2r
                                                                    then  bm\_single\_L(k;v;bm\_E();bm\_T(key;value;cnt;left;m7))
                                                                    else  bm\_double\_L(k;v;bm\_E();bm\_T(key;value;cnt;left;m7))
                                                                    fi  ))  \mmember{}  binary-map(T;Key)


By

((RWO  "bm\_cnt\_prop\_T"  (-1)  THENA  Auto)  THEN  RepD)

---

Home Index