---

Step * 1 1 of Lemma nat-ind-boot


1. P :   @i'
2. b : P 0@i
3. c : n:. ((P n)  (P (n + 1)))@i
4. n : @i
5. n:. ((n.primrec(n;b;c)) n  P n)
6. (n.primrec(n;b;c)) n  P n
 P n
BY
{ (UseWitness (n.primrec(n;b;c)) n THEN Trivial) }



1.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}@i'
2.  b  :  P  0@i
3.  c  :  \mforall{}n:\mBbbN{}.  ((P  n)  {}\mRightarrow{}  (P  (n  +  1)))@i
4.  n  :  \mBbbN{}@i
5.  \mforall{}n:\mBbbN{}.  ((\mlambda{}n.primrec(n;b;c))  n  \mmember{}  P  n)
6.  (\mlambda{}n.primrec(n;b;c))  n  \mmember{}  P  n
\mvdash{}  P  n


By

(UseWitness  \mkleeneopen{}(\mlambda{}n.primrec(n;b;c))  n\mkleeneclose{}\mcdot{}  THEN  Trivial)



Home Index