---

Step * 1 of Lemma comp_nat_ind_a


1. [P] : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])
3. i : ℕ
⊢ P[i]
BY
{ (% Generalize %
   Assert ∀j,s:ℕ.  (s < j ⇒ P[s])⋅
   THEN Try (Complete ((InstHyp [⌜i + 1⌝;⌜i⌝] (-1) THEN Auto)))
   ) }

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

---

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{}
\mvdash{}  P[i]


By

---

Latex:
(\%  Generalize  \%
  Assert  \mforall{}j,s:\mBbbN{}.    (s  <  j  {}\mRightarrow{}  P[s])\mcdot{}
  THEN  Try  (Complete  ((InstHyp  [\mkleeneopen{}i  +  1\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]  (-1)  THEN  Auto)))
  )

---

Home Index