---

Step * 1 1 of Lemma completeInductionFast


1. P :   @i'
2. g : n:. ((m:n. (P m))  (P n))@i
 n:. (P n)
BY
{ (Assert n:. m:n.  (P m) THEN Auto) }

1
1. P :   @i'
2. g : n:. ((m:n. (P m))  (P n))@i
3. n : @i
4. m : n@i
 P m

2
1. P :   @i'
2. g : n:. ((m:n. (P m))  (P n))@i
3. n:. m:n.  (P m)
4. n : @i
 P n



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


By

(Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}n.    (P  m)\mkleeneclose{}\mcdot{}  THEN  Auto)



Home Index