---

Step * of Lemma binary_map_ind-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
                                                     ─→ X
                                                     ─→ X].
  (binary_map_ind(x;E;key,value,cnt,left,right,recL,recR.F[key;value;cnt;left;right;recL;recR]) ∈ X)
BY
{ (Intros THEN Unhide THEN DVar `x' THEN BinMapInd `x' THEN OnSomeHyp(\i.RWO "bm_cnt_prop_T" i 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
                                                                                                          {}\mrightarrow{}  X
                                                                                                          {}\mrightarrow{}  X].
    (binary\_map\_ind(x;E;key,value,cnt,left,right,recL,recR.F[key;value;cnt;left;right;recL;recR])  \mmember{}  X)


By

(Intros
  THEN  Unhide
  THEN  DVar  `x'
  THEN  BinMapInd  `x'
  THEN  OnSomeHyp(\mbackslash{}i.RWO  "bm\_cnt\_prop\_T"  i  THEN  Auto)\mcdot{})

---

Home Index