---

Step * 1 1 2 of Lemma nat-ind-boot-direct


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)
BY
{ (((Reduce 0 THEN Unfold `primrec` 0) THEN RW (AddrC [2] UnrollRecursionC) 0) THEN Reduce 0) }

1
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
 if n + 1=0
     then b
     else let m := (n + 1) - 1 in
          c m (fix((primrec,n. if n=0  then b  else let m := n - 1 in c m (primrec m))) m)  P (n + 1)



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


By

(((Reduce  0  THEN  Unfold  `primrec`  0)  THEN  RW  (AddrC  [2]  UnrollRecursionC)  0)  THEN  Reduce  0)



Home Index