---

Step * 1 of Lemma MTree-induction2


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]}
BY
{ Assert ⌈∀n:ℕ. ∀x:MultiTree(T).  ((MTree-rank(x) ≤ n) ⇒ P[x])⌉⋅ }

1
.....assertion..... 
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
⊢ ∀n:ℕ. ∀x:MultiTree(T).  ((MTree-rank(x) ≤ n) ⇒ P[x])

2
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
5. ∀n:ℕ. ∀x:MultiTree(T).  ((MTree-rank(x) ≤ n) ⇒ P[x])
⊢ {∀x:MultiTree(T). P[x]}

---

Latex:



1.  [T]  :  Type
2.  [P]  :  MultiTree(T)  {}\mrightarrow{}  \mBbbP{}
3.  \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)])@i
4.  \mforall{}val:T.  P[MTree\_Leaf(val)]@i
\mvdash{}  \{\mforall{}x:MultiTree(T).  P[x]\}


By

Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}x:MultiTree(T).    ((MTree-rank(x)  \mleq{}  n)  {}\mRightarrow{}  P[x])\mkleeneclose{}\mcdot{}

---

Home Index