---

Step * 2 4 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. 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)
BY
{ (AutoSplit THEN Auto THEN MemTypeCD THEN Reduce 0 THEN Auto THEN BLemma `bm_cnt_prop_T` THEN Reduce 0 THEN Auto) }

---

Latex:



1.  T  :  Type
2.  Key  :  Type
3.  k  :  Key
4.  v  :  T
5.  key  :  Key
6.  value  :  T
7.  cnt  :  \mBbbZ{}
8.  k1  :  Key
9.  v1  :  T
10.  c1  :  \mBbbZ{}
11.  left  :  binary\_map(T;Key)
12.  l5  :  binary\_map(T;Key)
13.  k2  :  Key
14.  v2  :  T
15.  c2  :  \mBbbZ{}
16.  l6  :  binary\_map(T;Key)
17.  m12  :  binary\_map(T;Key)
18.  cnt  =  (1  +  c1  +  c2)
19.  \muparrow{}bm\_cnt\_prop(bm\_T(k1;v1;c1;left;l5))
20.  \muparrow{}bm\_cnt\_prop(bm\_T(k2;v2;c2;l6;m12))
\mvdash{}  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    \mmember{}  binary-map(T;Key)


By

(AutoSplit
  THEN  Auto
  THEN  MemTypeCD
  THEN  Reduce  0
  THEN  Auto
  THEN  BLemma  `bm\_cnt\_prop\_T`
  THEN  Reduce  0
  THEN  Auto)

---

Home Index