---

Step * 1 1 1 1 1 of Lemma comp_nat_ind_tp


1. [P] : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])
⊢ ∀zz,i:ℕ.  P[i] supposing i < zz
BY
{ D 0 }

1
1. [P] : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])
3. zz : ℕ
⊢ ∀i:ℕ. P[i] supposing i < zz

2
.....wf..... 
1. P : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])
⊢ istype(ℕ)

---

Latex:

---

Latex:

1.  [P]  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}\{k\}
2.  \mforall{}i:\mBbbN{}.  ((\mforall{}j:\mBbbN{}.  P[j]  supposing  j  <  i)  {}\mRightarrow{}  P[i])
\mvdash{}  \mforall{}zz,i:\mBbbN{}.    P[i]  supposing  i  <  zz


By

---

Latex:
D  0

---

Home Index