---

Step * of Lemma binary_map-induction

∀[T,Key:Type]. ∀[P:binary_map(T;Key) ─→ ℙ].
  (P[bm_E()]
  ⇒ (∀key:Key. ∀value:T. ∀cnt:ℤ. ∀left,right:binary_map(T;Key).
        (P[left] ⇒ P[right] ⇒ P[bm_T(key;value;cnt;left;right)]))
  ⇒ {∀v:binary_map(T;Key). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[P:binary\_map(T;Key)  {}\mrightarrow{}  \mBbbP{}].
    (P[bm\_E()]
    {}\mRightarrow{}  (\mforall{}key:Key.  \mforall{}value:T.  \mforall{}cnt:\mBbbZ{}.  \mforall{}left,right:binary\_map(T;Key).
                (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[bm\_T(key;value;cnt;left;right)]))
    {}\mRightarrow{}  \{\mforall{}v:binary\_map(T;Key).  P[v]\})


By

ProveDatatypeInd

---

Home Index