---

Step * 1 1 of Lemma completeInductionShortExt


1. P :   @i'
2. n:. ((m:n. (P m))  (P n))@i
3. n : @i
4. n1 : @i
5. (p.m:p. (P m)) n1@i
6. m : n1 + 1@i
 P m
BY
{ Reduce 5 }

1
1. P :   @i'
2. n:. ((m:n. (P m))  (P n))@i
3. n : @i
4. n1 : @i
5. m:n1. (P m)@i
6. m : n1 + 1@i
 P m



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.  n1  :  \mBbbN{}@i
5.  (\mlambda{}p.\mforall{}m:\mBbbN{}p.  (P  m))  n1@i
6.  m  :  \mBbbN{}n1  +  1@i
\mvdash{}  P  m


By

Reduce  5



Home Index