---

Step * of Lemma MultiTree_ind_wf

∀[T,A:Type]. ∀[R:A ─→ MultiTree(T) ─→ ℙ]. ∀[v:MultiTree(T)]. ∀[Node:labels:{L:Atom List| 0 < ||L||} 
                                                                    ─→ children:({a:Atom| (a ∈ labels)}  ─→ MultiTree(T)\000C)
                                                                    ─→ (u:{a:Atom| (a ∈ labels)}  ─→ {x:A| R[x;children \000Cu]} )
                                                                    ─→ {x:A| R[x;MTree_Node(labels;children)]} ].
∀[Leaf:val:T ─→ {x:A| R[x;MTree_Leaf(val)]} ].
  (MultiTree_ind(v;
                 MTree_Node(labels,children)⇒ rec1.Node[labels;children;rec1];
                 MTree_Leaf(val)⇒ Leaf[val])  ∈ {x:A| R[x;v]} )
BY
{ ProveDatatypeIndWf TERMOF{MultiTree-definition:o, 1:l, i:l}⋅ }

---

Latex:


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


By

ProveDatatypeIndWf  TERMOF\{MultiTree-definition:o,  1:l,  i:l\}\mcdot{}

---

Home Index