---

Step * 3 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))
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)
BY
{ (RepeatFor 3 (Try (AutoSplit)) THEN Try (Complete ((Auto THEN MemTypeCD THEN Auto)))) }

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))
11. k1 : Key
12. v1 : T
13. c1 : ℤ
14. l1 : binary_map(T;Key)
15. m12 : binary_map(T;Key)
16. ¬bm_numItems(l1) < bm_numItems(m12)
17. ↑bm_cnt_prop(bm_T(k1;v1;c1;l1;m12))
18. bm_wt(cnt) ≤ c1
⊢ bm_double_L(k;v;bm_T(key;value;cnt;left;m7);bm_T(k1;v1;c1;l1;m12)) ∈ 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_numItems(m7) < bm_numItems(left)
11. ↑bm_cnt_prop(bm_T(key;value;cnt;left;m7))
12. k1 : Key
13. v1 : T
14. c1 : ℤ
15. ¬(bm_wt(cnt) ≤ c1)
16. l1 : binary_map(T;Key)
17. m12 : binary_map(T;Key)
18. ↑bm_cnt_prop(bm_T(k1;v1;c1;l1;m12))
19. bm_wt(c1) ≤ cnt
⊢ bm_double_R(k;v;bm_T(key;value;cnt;left;m7);bm_T(k1;v1;c1;l1;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. 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. ¬(bm_wt(c1) ≤ cnt)
15. ¬(bm_wt(cnt) ≤ c1)
16. l1 : binary_map(T;Key)
17. m12 : binary_map(T;Key)
18. ↑bm_cnt_prop(bm_T(k1;v1;c1;l1;m12))
⊢ bm_T(k;v;cnt + c1 + 1;bm_T(key;value;cnt;left;m7);bm_T(k1;v1;c1;l1;m12)) ∈ 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))
11.  k1  :  Key
12.  v1  :  T
13.  c1  :  \mBbbZ{}
14.  l1  :  binary\_map(T;Key)
15.  m12  :  binary\_map(T;Key)
16.  \muparrow{}bm\_cnt\_prop(bm\_T(k1;v1;c1;l1;m12))
\mvdash{}  if  bm\_wt(cnt)  \mleq{}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)  \mleq{}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    \mmember{}  binary-map(T;Key)


By

(RepeatFor  3  (Try  (AutoSplit))  THEN  Try  (Complete  ((Auto  THEN  MemTypeCD  THEN  Auto))))

---

Home Index