---

Step * 1 1 of Lemma MTree-induction2

.....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])
BY
{ CompleteInductionOnNat }

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

---

Latex:


.....assertion..... 
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{}n:\mBbbN{}.  \mforall{}x:MultiTree(T).    ((MTree-rank(x)  \mleq{}  n)  {}\mRightarrow{}  P[x])


By

CompleteInductionOnNat

---

Home Index