---

Step * 1 2 of Lemma completeInductionBootStrap


1. P :   @i'
2. n:. ((m:n. (P m))  (P n))@i
3. n : @i
4. n:. ((p.m:p. (P m)) n)
 P n
BY
{ (Reduce (-1) THEN InstHyp [n + 1] (-1) THEN Auto) }



1.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}@i'
2.  \mforall{}n:\mBbbN{}.  ((\mforall{}m:\mBbbN{}n.  (P  m))  {}\mRightarrow{}  (P  n))@i
3.  n  :  \mBbbN{}@i
4.  \mforall{}n:\mBbbN{}.  ((\mlambda{}p.\mforall{}m:\mBbbN{}p.  (P  m))  n)
\mvdash{}  P  n


By

(Reduce  (-1)  THEN  InstHyp  [\mkleeneopen{}n  +  1\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)



Home Index