---

Step * 1 1 2 of Lemma comp_nat_ind_a


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]
BY
{ ((Assert ∀t:ℕ. (t < s ⇒ P[t]) BY Auto) THEN Auto) }

---

Latex:

---

Latex:

1.  [P]  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}\{k\}
2.  \mforall{}i:\mBbbN{}.  ((\mforall{}j:\mBbbN{}.  P[j]  supposing  j  <  i)  {}\mRightarrow{}  P[i])
3.  i  :  \mBbbN{}
4.  j  :  \mBbbN{}\msupplus{}
5.  \mforall{}s:\mBbbN{}.  (s  <  j  -  1  {}\mRightarrow{}  P[s])
6.  s  :  \mBbbN{}
7.  s  <  j
\mvdash{}  P[s]


By

---

Latex:
((Assert  \mforall{}t:\mBbbN{}.  (t  <  s  {}\mRightarrow{}  P[t])  BY  Auto)  THEN  Auto)

---

Home Index