---

Step * of Lemma bm_T'_wf

∀[T,Key:Type]. ∀[k:Key]. ∀[v:T]. ∀[m1,m2:binary-map(T;Key)].  (bm_T'(k;v;m1;m2) ∈ binary-map(T;Key))
BY
{ (Auto
   THEN All (RepUR ``bm_T' binary-map``)
   THEN DVarSets
   THEN Fold `binary-map` 0
   THEN BinaryMapCase (-4)
   THEN BinaryMapCase (-2)) }

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. ↑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)

2
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)

3
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))
11. k1 : Key
12. v1 : T
13. c1 : ℤ
14. l1 : binary_map(T;Key)
15. m12 : binary_map(T;Key)
16. ↑bm_cnt_prop(bm_T(k1;v1;c1;l1;m12))
⊢ if bm_wt(cnt) ≤z c1
    then if bm_numItems(l1) <z bm_numItems(m12)
         then bm_single_L(k;v;bm_T(key;value;cnt;left;m7);bm_T(k1;v1;c1;l1;m12))
         else bm_double_L(k;v;bm_T(key;value;cnt;left;m7);bm_T(k1;v1;c1;l1;m12))
         fi 
  if bm_wt(c1) ≤z cnt
    then if bm_numItems(m7) <z bm_numItems(left)
         then bm_single_R(k;v;bm_T(key;value;cnt;left;m7);bm_T(k1;v1;c1;l1;m12))
         else bm_double_R(k;v;bm_T(key;value;cnt;left;m7);bm_T(k1;v1;c1;l1;m12))
         fi 
  else bm_T(k;v;cnt + c1 + 1;bm_T(key;value;cnt;left;m7);bm_T(k1;v1;c1;l1;m12))
  fi  ∈ binary-map(T;Key)

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[k:Key].  \mforall{}[v:T].  \mforall{}[m1,m2:binary-map(T;Key)].    (bm\_T'(k;v;m1;m2)  \mmember{}  binary-map(T;Key))


By

(Auto
  THEN  All  (RepUR  ``bm\_T'  binary-map``)
  THEN  DVarSets
  THEN  Fold  `binary-map`  0
  THEN  BinaryMapCase  (-4)
  THEN  BinaryMapCase  (-2))

---

Home Index