---

Step * of Lemma MultiTree-induction

∀[T:Type]. ∀[P:MultiTree(T) ─→ ℙ].
  ((∀labels:{L:Atom List| 0 < ||L||} . ∀children:{a:Atom| (a ∈ labels)}  ─→ MultiTree(T).
      ((∀u:{a:Atom| (a ∈ labels)} . P[children u]) ⇒ P[MTree_Node(labels;children)]))
  ⇒ (∀val:T. P[MTree_Leaf(val)])
  ⇒ {∀v:MultiTree(T). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:


\mforall{}[T:Type].  \mforall{}[P:MultiTree(T)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}labels:\{L:Atom  List|  0  <  ||L||\}  .  \mforall{}children:\{a:Atom|  (a  \mmember{}  labels)\}    {}\mrightarrow{}  MultiTree(T).
            ((\mforall{}u:\{a:Atom|  (a  \mmember{}  labels)\}  .  P[children  u])  {}\mRightarrow{}  P[MTree\_Node(labels;children)]))
    {}\mRightarrow{}  (\mforall{}val:T.  P[MTree\_Leaf(val)])
    {}\mRightarrow{}  \{\mforall{}v:MultiTree(T).  P[v]\})


By

ProveDatatypeInd

---

Home Index