---

Step * 1 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. 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)
BY
{ (OnVar `left' BinaryMapCase  THEN OnVar `m7' BinaryMapCase ) }

1
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_E();bm_T(key;value;cnt;bm_E();bm_E())) ∈ binary-map(T;Key)

2
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_single_L(k;v;bm_E();bm_T(key;value;cnt;bm_E();bm_T(k1;v1;c1;left;m12))) ∈ binary-map(T;Key)

3
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. l5 : binary_map(T;Key)
13. cnt = (1 + c1 + 0) ∈ ℤ
14. ↑bm_cnt_prop(bm_T(k1;v1;c1;left;l5))
⊢ bm_double_L(k;v;bm_E();bm_T(key;value;cnt;bm_T(k1;v1;c1;left;l5);bm_E())) ∈ binary-map(T;Key)

4
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. l5 : binary_map(T;Key)
13. k2 : Key
14. v2 : T
15. c2 : ℤ
16. l6 : binary_map(T;Key)
17. m12 : binary_map(T;Key)
18. cnt = (1 + c1 + c2) ∈ ℤ
19. ↑bm_cnt_prop(bm_T(k1;v1;c1;left;l5))
20. ↑bm_cnt_prop(bm_T(k2;v2;c2;l6;m12))
⊢ if c1 <z c2
  then bm_single_L(k;v;bm_E();bm_T(key;value;cnt;bm_T(k1;v1;c1;left;l5);bm_T(k2;v2;c2;l6;m12)))
  else bm_double_L(k;v;bm_E();bm_T(key;value;cnt;bm_T(k1;v1;c1;left;l5);bm_T(k2;v2;c2;l6;m12)))
  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.  cnt  =  (1  +  bm\_numItems(left)  +  bm\_numItems(m7))
11.  \muparrow{}bm\_cnt\_prop(left)
12.  \muparrow{}bm\_cnt\_prop(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

(OnVar  `left'  BinaryMapCase    THEN  OnVar  `m7'  BinaryMapCase  )

---

Home Index