---

Step * 1 2 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 : 
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)
BY
{ ((AutoSplit THEN Fold `primrec` 0) THEN (Assert (n + 1) - 1 ~ n BY Auto)) }

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
6. ((n + 1) = 0)
7. (n + 1) - 1 ~ n
 let m := (n + 1) - 1 in
  c m primrec(m;b;c)  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{}
5.  (\mlambda{}n.primrec(n;b;c))  n  \mmember{}  P  n
\mvdash{}  if  n  +  1=0
          then  b
          else  let  m  :=  (n  +  1)  -  1  in
                    c  m  (fix((\mlambda{}primrec,n.  if  n=0    then  b    else  let  m  :=  n  -  1  in  c  m  (primrec  m)))  m)  \mmember{}  P  (n  +\000C  1)


By

((AutoSplit  THEN  Fold  `primrec`  0)  THEN  (Assert  (n  +  1)  -  1  \msim{}  n  BY  Auto))



Home Index