---

Step * 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. 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_T(key;value;cnt;left;m7);bm_E());
                                       key1r,value1r,cnt1r,left1r,right1r.
                                       bm_double_R(k;v;bm_T(key;value;cnt;left;m7);bm_E()));
                  key1l,value1l,cnt1l,left1l,right1l.
                  binary_map_case(m7;bm_single_R(k;v;bm_T(key;value;cnt;left;m7);bm_E());
                                  key1r,value1r,cnt1r,left1r,right1r.if cnt1r <z cnt1l
                                  then bm_single_R(k;v;bm_T(key;value;cnt;left;m7);bm_E())
                                  else bm_double_R(k;v;bm_T(key;value;cnt;left;m7);bm_E())
                                  fi )) ∈ binary-map(T;Key)
BY
{ ((RWO "bm_cnt_prop_T" (-1) THENA Auto) THEN RepD THEN 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_T(key;value;cnt;bm_E();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_double_R(k;v;bm_T(key;value;cnt;bm_E();bm_T(k1;v1;c1;left;m12));bm_E()) ∈ 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_single_R(k;v;bm_T(key;value;cnt;bm_T(k1;v1;c1;left;l5);bm_E());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 c2 <z c1
  then bm_single_R(k;v;bm_T(key;value;cnt;bm_T(k1;v1;c1;left;l5);bm_T(k2;v2;c2;l6;m12));bm_E())
  else bm_double_R(k;v;bm_T(key;value;cnt;bm_T(k1;v1;c1;left;l5);bm_T(k2;v2;c2;l6;m12));bm_E())
  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\_T(key;value;cnt;left;m7);bm\_E());
                                                                              key1r,value1r,cnt1r,left1r,right1r.
                                                                              bm\_double\_R(k;v;bm\_T(key;value;cnt;left;m7);bm\_E()));
                                    key1l,value1l,cnt1l,left1l,right1l.
                                    binary\_map\_case(m7;bm\_single\_R(k;v;bm\_T(key;value;cnt;left;m7);bm\_E());
                                                                    key1r,value1r,cnt1r,left1r,right1r.if  cnt1r  <z  cnt1l
                                                                    then  bm\_single\_R(k;v;bm\_T(key;value;cnt;left;m7);bm\_E())
                                                                    else  bm\_double\_R(k;v;bm\_T(key;value;cnt;left;m7);bm\_E())
                                                                    fi  ))  \mmember{}  binary-map(T;Key)


By

((RWO  "bm\_cnt\_prop\_T"  (-1)  THENA  Auto)
  THEN  RepD
  THEN  OnVar  `left'  BinaryMapCase 
  THEN  OnVar  `m7'  BinaryMapCase  )

---

Home Index