---

Step * 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
⊢ ∀x:MultiTree(T). ((MTree-rank(x) ≤ n) ⇒ P[x])
BY
{ (BLemma `MultiTree-induction` THENA 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
5. n : ℕ
6. ∀n:ℕn. ∀x:MultiTree(T).  ((MTree-rank(x) ≤ n) ⇒ P[x])@i
⊢ ∀labels:{L:Atom List| 0 < ||L||} . ∀children:{a:Atom| (a ∈ labels)}  ─→ MultiTree(T).
    ((∀u:{a:Atom| (a ∈ labels)} . ((MTree-rank(children u) ≤ n) ⇒ P[children u]))
    ⇒ (MTree-rank(MTree_Node(labels;children)) ≤ n)
    ⇒ P[MTree_Node(labels;children)])

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

---

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


By

(BLemma  `MultiTree-induction`  THENA  Auto)

---

Home Index