---

Step * of Lemma MTree-induction2

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

1
1. [T] : Type
2. [P] : MultiTree(T) ─→ ℙ
3. ∀labels:{L:Atom List| 0 < ||L||} . ∀children:{a:Atom| (a ∈ labels)}  ─→ MultiTree(T).
     ((∀a∈labels.P[children a]) ⇒ P[MTree_Node(labels;children)])@i
4. ∀val:T. P[MTree_Leaf(val)]@i
⊢ {∀x:MultiTree(T). P[x]}

---

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{}a\mmember{}labels.P[children  a])  {}\mRightarrow{}  P[MTree\_Node(labels;children)]))
    {}\mRightarrow{}  (\mforall{}val:T.  P[MTree\_Leaf(val)])
    {}\mRightarrow{}  \{\mforall{}x:MultiTree(T).  P[x]\})


By

Auto

---

Home Index