---

Step * of Lemma l_tree-induction

∀[L,T:Type]. ∀[P:l_tree(L;T) ─→ ℙ].
  ((∀val:L. P[l_tree_leaf(val)])
  ⇒ (∀val:T. ∀left_subtree,right_subtree:l_tree(L;T).
        (P[left_subtree] ⇒ P[right_subtree] ⇒ P[l_tree_node(val;left_subtree;right_subtree)]))
  ⇒ {∀v:l_tree(L;T). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:


\mforall{}[L,T:Type].  \mforall{}[P:l\_tree(L;T)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}val:L.  P[l\_tree\_leaf(val)])
    {}\mRightarrow{}  (\mforall{}val:T.  \mforall{}left$_{subtree}$,right$_{subtree}$:l\_tree(L;T\000C).
                (P[left$_{subtree}$]  {}\mRightarrow{}  P[right$_{subtree}$]  {}\mRightarrow{}  P[l\_\000Ctree\_node(val;left$_{subtree}$;right$_{subtree}$)]))
    {}\mRightarrow{}  \{\mforall{}v:l\_tree(L;T).  P[v]\})


By

ProveDatatypeInd

---

Home Index