---

Step * 1 of Lemma rank-Ex1_wf


1. T : Type
2. t1 : RankEx1(T) List
3. ∀i:ℕ||t1||. (rank-Ex1(t1[i]) ∈ ℕ)
⊢ imax-list([0 / map(λu.rank-Ex1(u);t1)]) + 1 ∈ ℕ
BY
{ (BLemma `add-nat` THEN Try (BLemma `imax-list-is-nat`) THEN Try (CompleteAuto)) }

1
.....wf..... 
1. T : Type
2. t1 : RankEx1(T) List
3. ∀i:ℕ||t1||. (rank-Ex1(t1[i]) ∈ ℕ)
⊢ map(λu.rank-Ex1(u);t1) ∈ ℤ List

---

Latex:



1.  T  :  Type
2.  t1  :  RankEx1(T)  List
3.  \mforall{}i:\mBbbN{}||t1||.  (rank-Ex1(t1[i])  \mmember{}  \mBbbN{})
\mvdash{}  imax-list([0  /  map(\mlambda{}u.rank-Ex1(u);t1)])  +  1  \mmember{}  \mBbbN{}


By

(BLemma  `add-nat`  THEN  Try  (BLemma  `imax-list-is-nat`)  THEN  Try  (CompleteAuto))

---

Home Index