Step
*
1
2
1
1
1
1
1
2
of Lemma
test-nat-bootstrap
1. P : 
 
 
@i'
2. b : P 0@i
3. c : n:
 
 P n 
 (P (n + 1))@i
4. n : 
5. primrec(n;b;c) 
 P n
6. 
((n + 1) = 0)
7. (n + 1) - 1 ~ n
8. (n)
 c n primrec(n;b;c) ~ c n primrec(n;b;c)
BY
{ Trivial }
1.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}@i'
2.  b  :  P  0@i
3.  c  :  n:\mBbbN{}  {}\mrightarrow{}  P  n  {}\mrightarrow{}  (P  (n  +  1))@i
4.  n  :  \mBbbN{}
5.  primrec(n;b;c)  \mmember{}  P  n
6.  \mneg{}((n  +  1)  =  0)
7.  (n  +  1)  -  1  \msim{}  n
8.  (n)\mdownarrow{}
\mvdash{}  c  n  primrec(n;b;c)  \msim{}  c  n  primrec(n;b;c)
By
Trivial
Home
Index