---

Step * 3 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_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)
BY
{ (Auto
   THEN Try (Complete ((MemTypeCD THEN Auto)))
   THEN Reduce 0
   THEN BinMapCase `m7'
   THEN Auto
   THEN All(\i.Try(RWO "bm_cnt_prop_T" i))
   THEN Auto
   THEN AllReduce
   THEN All(\i.Try (FLemma `bm_cnt_prop_pos` [i] THENA Complete Auto))
   THEN (Assert ⌈cnt = 1 ∈ ℤ⌉⋅ THENA Auto)
   THEN (Assert ⌈1 ≤ c1⌉⋅ THENA Auto)
   THEN All (RepUR ``bm_wt``)
   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.  left  :  binary\_map(T;Key)
9.  m7  :  binary\_map(T;Key)
10.  \mneg{}bm\_numItems(m7)  <  bm\_numItems(left)
11.  \muparrow{}bm\_cnt\_prop(bm\_T(key;value;cnt;left;m7))
12.  k1  :  Key
13.  v1  :  T
14.  c1  :  \mBbbZ{}
15.  \mneg{}(bm\_wt(cnt)  \mleq{}  c1)
16.  l1  :  binary\_map(T;Key)
17.  m12  :  binary\_map(T;Key)
18.  \muparrow{}bm\_cnt\_prop(bm\_T(k1;v1;c1;l1;m12))
19.  bm\_wt(c1)  \mleq{}  cnt
\mvdash{}  bm\_double\_R(k;v;bm\_T(key;value;cnt;left;m7);bm\_T(k1;v1;c1;l1;m12))  \mmember{}  binary-map(T;Key)


By

(Auto
  THEN  Try  (Complete  ((MemTypeCD  THEN  Auto)))
  THEN  Reduce  0
  THEN  BinMapCase  `m7'
  THEN  Auto
  THEN  All(\mbackslash{}i.Try(RWO  "bm\_cnt\_prop\_T"  i))
  THEN  Auto
  THEN  AllReduce
  THEN  All(\mbackslash{}i.Try  (FLemma  `bm\_cnt\_prop\_pos`  [i]  THENA  Complete  Auto))
  THEN  (Assert  \mkleeneopen{}cnt  =  1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}1  \mleq{}  c1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  (RepUR  ``bm\_wt``)
  THEN  Auto')

---

Home Index