---

Step * 1 2 of Lemma MTree-rank_wf


1. T : Type@i'
2. labels : {L:Atom List| 0 < ||L||} 
3. t2 : {a:Atom| (a ∈ labels)}  ─→ MultiTree(T)
4. ∀a:ℕ||labels||. (MTree-rank(t2 labels[a]) ∈ ℕ)
5. map(λa.MTree-rank(t2 a);labels) ∈ ℕ List
⊢ imax-list(map(λa.MTree-rank(t2 a);labels)) + 1 ∈ ℕ
BY
{ (GenConclTerm ⌈map(λa.MTree-rank(t2 a);labels)⌉⋅ THENA Auto) }

1
1. T : Type@i'
2. labels : {L:Atom List| 0 < ||L||} 
3. t2 : {a:Atom| (a ∈ labels)}  ─→ MultiTree(T)
4. ∀a:ℕ||labels||. (MTree-rank(t2 labels[a]) ∈ ℕ)
5. map(λa.MTree-rank(t2 a);labels) ∈ ℕ List
6. v : ℕ List@i
7. map(λa.MTree-rank(t2 a);labels) = v ∈ (ℕ List)@i
⊢ imax-list(v) + 1 ∈ ℕ

---

Latex:



1.  T  :  Type@i'
2.  labels  :  \{L:Atom  List|  0  <  ||L||\} 
3.  t2  :  \{a:Atom|  (a  \mmember{}  labels)\}    {}\mrightarrow{}  MultiTree(T)
4.  \mforall{}a:\mBbbN{}||labels||.  (MTree-rank(t2  labels[a])  \mmember{}  \mBbbN{})
5.  map(\mlambda{}a.MTree-rank(t2  a);labels)  \mmember{}  \mBbbN{}  List
\mvdash{}  imax-list(map(\mlambda{}a.MTree-rank(t2  a);labels))  +  1  \mmember{}  \mBbbN{}


By

(GenConclTerm  \mkleeneopen{}map(\mlambda{}a.MTree-rank(t2  a);labels)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index