---

Step * of Lemma MultiTree_ind_wf_simple

∀[T,A:Type]. ∀[v:MultiTree(T)]. ∀[Node:labels:{L:Atom List| 0 < ||L||} 
                                       ─→ children:({a:Atom| (a ∈ labels)}  ─→ MultiTree(T))
                                       ─→ (u:{a:Atom| (a ∈ labels)}  ─→ A)
                                       ─→ A]. ∀[Leaf:val:T ─→ A].
  (MultiTree_ind(v;
                 MTree_Node(labels,children)⇒ rec1.Node[labels;children;rec1];
                 MTree_Leaf(val)⇒ Leaf[val])  ∈ A)
BY
{ ProveDatatypeIndWfSimple 1 `MultiTree_ind_wf` }

---

Latex:


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


By

ProveDatatypeIndWfSimple  1  `MultiTree\_ind\_wf`

---

Home Index