---

Step * of Lemma MultiTree-definition

∀[T,A:Type]. ∀[R:A ─→ MultiTree(T) ─→ ℙ].
  ((∀labels:{L:Atom List| 0 < ||L||} . ∀children:{a:Atom| (a ∈ labels)}  ─→ MultiTree(T).
      ((∀u:{a:Atom| (a ∈ labels)} . {x:A| R[x;children u]} ) ⇒ {x:A| R[x;MTree_Node(labels;children)]} ))
  ⇒ (∀val:T. {x:A| R[x;MTree_Leaf(val)]} )
  ⇒ {∀v:MultiTree(T). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `MultiTree-induction` }

---

Latex:


\mforall{}[T,A:Type].  \mforall{}[R:A  {}\mrightarrow{}  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)\}  .  \{x:A|  R[x;children  u]\}  )  {}\mRightarrow{}  \{x:A|  R[x;MTree\_Node(labels;children\000C)]\}  ))
    {}\mRightarrow{}  (\mforall{}val:T.  \{x:A|  R[x;MTree\_Leaf(val)]\}  )
    {}\mRightarrow{}  \{\mforall{}v:MultiTree(T).  \{x:A|  R[x;v]\}  \})


By

ProveDatatypeDefinition  `MultiTree-induction`

---

Home Index