---

Step * 1 2 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:ℕ. ∀x:MultiTree(T).  ((MTree-rank(x) ≤ n) ⇒ P[x])
6. x : MultiTree(T)@i
⊢ P[x]
BY
{ (InstHyp [⌈MTree-rank(x)⌉] 5⋅ THEN Auto) }

---

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


By

(InstHyp  [\mkleeneopen{}MTree-rank(x)\mkleeneclose{}]  5\mcdot{}  THEN  Auto)

---

Home Index