---

Step * 1 2 1 1 of Lemma MTree-rank_wf


1. T : Type@i'
2. labels : Atom List
3. 0 < ||labels||
4. t2 : {a:Atom| (a ∈ labels)}  ─→ MultiTree(T)
5. ∀a:ℕ||labels||. (MTree-rank(t2 labels[a]) ∈ ℕ)
6. map(λa.MTree-rank(t2 a);labels) ∈ ℕ List
7. v : ℕ List@i
8. map(λa.MTree-rank(t2 a);labels) = v ∈ (ℕ List)@i
9. ||labels|| = ||v|| ∈ ℤ
⊢ imax-list(v) + 1 ∈ ℕ
BY
{ (Assert 0 ≤ imax-list(v) BY
         (BLemma `imax-list-ub` THEN Auto)) }

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

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

---

Latex:



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


By

(Assert  0  \mleq{}  imax-list(v)  BY
              (BLemma  `imax-list-ub`  THEN  Auto))

---

Home Index