---

Step * 1 1 1 1 2 1 of Lemma completeInductionFast


1. P :   @i'
2. g : n:. ((m:n. (P m))  (P n))@i
3. n : @i
4. n:. (fix((f,n. g[n;f]))  m:n. (P m))
5. fix((f,n. g[n;f]))  m:n. (P m)
6. m : n@i
 P m
BY
{ (UseWitness fix((f,n. g[n;f])) m THEN Auto) }



1.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}@i'
2.  g  :  \mforall{}n:\mBbbN{}.  ((\mforall{}m:\mBbbN{}n.  (P  m))  {}\mRightarrow{}  (P  n))@i
3.  n  :  \mBbbN{}@i
4.  \mforall{}n:\mBbbN{}.  (fix((\mlambda{}f,n.  g[n;f]))  \mmember{}  \mforall{}m:\mBbbN{}n.  (P  m))
5.  fix((\mlambda{}f,n.  g[n;f]))  \mmember{}  \mforall{}m:\mBbbN{}n.  (P  m)
6.  m  :  \mBbbN{}n@i
\mvdash{}  P  m


By

(UseWitness  \mkleeneopen{}fix((\mlambda{}f,n.  g[n;f]))  m\mkleeneclose{}\mcdot{}  THEN  Auto)



Home Index