---

Step * 1 1 1 1 1 1 1 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
5. n : ℕ
6. ∀n:ℕn. ∀x:MultiTree(T).  ((MTree-rank(x) ≤ n) ⇒ P[x])@i
7. labels : {L:Atom List| 0 < ||L||} @i
8. children : {a:Atom| (a ∈ labels)}  ─→ MultiTree(T)@i
9. ∀u:{a:Atom| (a ∈ labels)} . ((MTree-rank(children u) ≤ n) ⇒ P[children u])@i
10. MTree-rank(MTree_Node(labels;children)) ≤ n@i
11. a : Atom@i
12. (a ∈ labels)@i
⊢ MTree-rank(children a) < n
BY
{ (RecUnfold `MTree-rank` (-3) THEN Reduce (-3)) }

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
7. labels : {L:Atom List| 0 < ||L||} @i
8. children : {a:Atom| (a ∈ labels)}  ─→ MultiTree(T)@i
9. ∀u:{a:Atom| (a ∈ labels)} . ((MTree-rank(children u) ≤ n) ⇒ P[children u])@i
10. (imax-list(map(λa.MTree-rank(children a);labels)) + 1) ≤ n@i
11. a : Atom@i
12. (a ∈ labels)@i
⊢ MTree-rank(children a) < n

---

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
5.  n  :  \mBbbN{}
6.  \mforall{}n:\mBbbN{}n.  \mforall{}x:MultiTree(T).    ((MTree-rank(x)  \mleq{}  n)  {}\mRightarrow{}  P[x])@i
7.  labels  :  \{L:Atom  List|  0  <  ||L||\}  @i
8.  children  :  \{a:Atom|  (a  \mmember{}  labels)\}    {}\mrightarrow{}  MultiTree(T)@i
9.  \mforall{}u:\{a:Atom|  (a  \mmember{}  labels)\}  .  ((MTree-rank(children  u)  \mleq{}  n)  {}\mRightarrow{}  P[children  u])@i
10.  MTree-rank(MTree\_Node(labels;children))  \mleq{}  n@i
11.  a  :  Atom@i
12.  (a  \mmember{}  labels)@i
\mvdash{}  MTree-rank(children  a)  <  n


By

(RecUnfold  `MTree-rank`  (-3)  THEN  Reduce  (-3))

---

Home Index