---

Step * of Lemma binary_map_case-wf2

∀[X,T,Key:Type]. ∀[x:binary-map(T;Key)]. ∀[E:X]. ∀[F:key:Key
                                                     ─→ value:T
                                                     ─→ cnt:ℤ
                                                     ─→ left:binary-map(T;Key)
                                                     ─→ right:binary-map(T;Key)
                                                     ─→ X].
  (binary_map_case(x;E;key,value,cnt,left,right.F[key;value;cnt;left;right]) ∈ X)
BY
{ (Intros
   THEN Unhide
   THEN RepeatFor 2 (DVar `x')
   THEN Unfold `binary_map_case` 0
   THEN RecUnfold `binary_map_ind` 0⋅
   THEN RepUR ``bm_E bm_T`` 0
   THEN Try (RWO "bm_cnt_prop_T" (-3))
   THEN Auto) }

---

Latex:


\mforall{}[X,T,Key:Type].  \mforall{}[x:binary-map(T;Key)].  \mforall{}[E:X].  \mforall{}[F:key:Key
                                                                                                          {}\mrightarrow{}  value:T
                                                                                                          {}\mrightarrow{}  cnt:\mBbbZ{}
                                                                                                          {}\mrightarrow{}  left:binary-map(T;Key)
                                                                                                          {}\mrightarrow{}  right:binary-map(T;Key)
                                                                                                          {}\mrightarrow{}  X].
    (binary\_map\_case(x;E;key,value,cnt,left,right.F[key;value;cnt;left;right])  \mmember{}  X)


By

(Intros
  THEN  Unhide
  THEN  RepeatFor  2  (DVar  `x')
  THEN  Unfold  `binary\_map\_case`  0
  THEN  RecUnfold  `binary\_map\_ind`  0\mcdot{}
  THEN  RepUR  ``bm\_E  bm\_T``  0
  THEN  Try  (RWO  "bm\_cnt\_prop\_T"  (-3))
  THEN  Auto)

---

Home Index