---

Step * 1 1 2 1 1 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. primrec(n;b;c)  P n
6. ((n + 1) = 0)
7. (n + 1) - 1 ~ n
8. (n)
9. let m := n in
   c m primrec(m;b;c) ~ c n primrec(n;b;c)
 let m := n in
  c m primrec(m;b;c)  P (n + 1)
BY
{ (HypSubst 9 0 THEN MemCD) }

1
.....subterm..... T:t
1:n
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)
9. let m := n in
   c m primrec(m;b;c) ~ c n primrec(n;b;c)
 c n  P n  (P (n + 1))

2
.....subterm..... T:t
2:n
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)
9. let m := n in
   c m primrec(m;b;c) ~ c n primrec(n;b;c)
 primrec(n;b;c)  P n



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.  primrec(n;b;c)  \mmember{}  P  n
6.  \mneg{}((n  +  1)  =  0)
7.  (n  +  1)  -  1  \msim{}  n
8.  (n)\mdownarrow{}
9.  let  m  :=  n  in
      c  m  primrec(m;b;c)  \msim{}  c  n  primrec(n;b;c)
\mvdash{}  let  m  :=  n  in
    c  m  primrec(m;b;c)  \mmember{}  P  (n  +  1)


By

(HypSubst  9  0  THEN  MemCD)



Home Index