---

Step * 1 1 of Lemma comp_nat_ind_a

.....assertion..... 
1. [P] : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])
3. i : ℕ
⊢ ∀j,s:ℕ.  (s < j ⇒ P[s])
BY
{ (% do simple nat induction%
((BLemma `nat_ind_a` THENM RepD) THENA Auto)) }

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

2
1. [P] : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])
3. i : ℕ
4. j : ℕ+
5. ∀s:ℕ. (s < j - 1 ⇒ P[s])
6. s : ℕ
7. s < j
⊢ P[s]

---

Latex:

---

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


By

---

Latex:
(\%  do  simple  nat  induction\%
((BLemma  `nat\_ind\_a`  THENM  RepD)  THENA  Auto))

---

Home Index