---

Step * 3 1 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_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)
BY
{ (Auto
   THEN Try (Complete ((MemTypeCD THEN Auto)))
   THEN Reduce 0
   THEN BinMapCase `l1'
   THEN Auto
   THEN (RWO "bm_cnt_prop_T" (-2)
         THEN Auto
         THEN AllReduce
         THEN (FLemma `bm_cnt_prop_pos` [-2] THENA Auto)
         THEN (Assert ⌈bm_numItems(m12) = 0 ∈ ℤ⌉⋅ THENA Auto')
         THEN ((Assert cnt < 1 BY
                      OnMaybeHyp 15 (\h. (RepUR ``bm_wt`` h THEN Complete (Auto'))))
               THEN Assert ⌈1 ≤ cnt⌉⋅
               THEN Auto'
               THEN OnMaybeHyp 10 (\h. (RWO "bm_cnt_prop_T" h
                                        THEN Auto
                                        THEN All(\i.Try (FLemma `bm_cnt_prop_pos` [i] THENA Complete Auto))
                                        THEN Complete (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.  \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.  \mneg{}bm\_numItems(l1)  <  bm\_numItems(m12)
17.  \muparrow{}bm\_cnt\_prop(bm\_T(k1;v1;c1;l1;m12))
18.  bm\_wt(cnt)  \mleq{}  c1
\mvdash{}  bm\_double\_L(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  `l1'
  THEN  Auto
  THEN  (RWO  "bm\_cnt\_prop\_T"  (-2)
              THEN  Auto
              THEN  AllReduce
              THEN  (FLemma  `bm\_cnt\_prop\_pos`  [-2]  THENA  Auto)
              THEN  (Assert  \mkleeneopen{}bm\_numItems(m12)  =  0\mkleeneclose{}\mcdot{}  THENA  Auto')
              THEN  ((Assert  cnt  <  1  BY
                                        OnMaybeHyp  15  (\mbackslash{}h.  (RepUR  ``bm\_wt``  h  THEN  Complete  (Auto'))))
                          THEN  Assert  \mkleeneopen{}1  \mleq{}  cnt\mkleeneclose{}\mcdot{}
                          THEN  Auto'
                          THEN  OnMaybeHyp  10  (\mbackslash{}h.
                          (RWO  "bm\_cnt\_prop\_T"  h
                            THEN  Auto
                            THEN  All(\mbackslash{}i.Try  (FLemma  `bm\_cnt\_prop\_pos`  [i]  THENA  Complete  Auto))
                            THEN  Complete  (Auto'))\mcdot{}))\mcdot{}))

---

Home Index