---

Step * 1 of Lemma nat-ind-boot


1. P :   @i'
2. P 0@i
3. n:. ((P n)  (P (n + 1)))@i
4. n : @i
 P n
BY
{ ((RenameVar `b' 2 THEN RenameVar `c' 3)
   THEN InstLemma `test-nat-bootstrap` [P;b;c]
   THEN Auto
   THEN InstHyp [n] 5
   THEN Auto) }

1
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



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


By

((RenameVar  `b'  2  THEN  RenameVar  `c'  3)
  THEN  InstLemma  `test-nat-bootstrap`  [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  5\mcdot{}
  THEN  Auto)



Home Index