---

Step * 1 of Lemma test-nat-bootstrap


1. P :   @i'
2. b : P 0@i
3. c : n:  P n  (P (n + 1))@i
4. n : @i
 (n.primrec(n;b;c)) n  P n
BY
{ Refine `natInductionBootStrap` [mk_int_arg 4;mk_var_arg `%']  }

1
1. P :   @i'
2. b : P 0@i
3. c : n:  P n  (P (n + 1))@i
 (n.primrec(n;b;c)) 0  P 0

2
1. P :   @i'
2. b : P 0@i
3. c : n:  P n  (P (n + 1))@i
4. n : 
5. (n.primrec(n;b;c)) n  P n
 (n.primrec(n;b;c)) (n + 1)  P (n + 1)



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{}@i
\mvdash{}  (\mlambda{}n.primrec(n;b;c))  n  \mmember{}  P  n


By

Refine  `natInductionBootStrap`  [mk\_int\_arg  4;mk\_var\_arg  `\%'] 



Home Index