Nuprl - Proof: primrec list accum 2 1 1 1

(14steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

1. n:
2. 0 < n
3. f,x:Top. primrec(n-1;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n-1))
4. f: Top
5. x:Top. primrec(n-1;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n-1))
6. x: Top
7. primrec(n-1;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n-1))
8. n = 0

i:. i < n (z:Top. (f(n-1,list_accum(i,y.f(y,i);z;upto(n-1-i;n-1)))) ~ list_accum(i,y.f(y,i);z;upto(n-1-i;n)))

By: Analyze 0 THEN NatInd -1

Generated subgoals:

1 0 < n (z:Top. (f(n-1,list_accum(i,y.f(y,i);z;upto(n-1-0;n-1)))) ~ list_accum(i,y.f(y,i);z;upto(n-1-0;n))) 5 steps

2 9. i:
10. 0 < i
11. i-1 < n (z:Top. (f(n-1,list_accum(i,y.f(y,i);z;upto(n-1-(i-1);n-1)))) ~ list_accum(i,y.f(y,i);z;upto(n-1-(i-1);n)))
i < n (z:Top. (f(n-1,list_accum(i,y.f(y,i);z;upto(n-1-i;n-1)))) ~ list_accum(i,y.f(y,i);z;upto(n-1-i;n))) 2 steps

About:

(14steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

1	`0 < n (z:Top. (f(n-1,list_accum(i,y.f(y,i);z;upto(n-1-0;n-1)))) ~ list_accum(i,y.f(y,i);z;upto(n-1-0;n)))`	5 steps

2	9. `i:` 10. `0 < i` 11. `i-1 < n (z:Top. (f(n-1,list_accum(i,y.f(y,i);z;upto(n-1-(i-1);n-1)))) ~ list_accum(i,y.f(y,i);z;upto(n-1-(i-1);n)))` `i < n (z:Top. (f(n-1,list_accum(i,y.f(y,i);z;upto(n-1-i;n-1)))) ~ list_accum(i,y.f(y,i);z;upto(n-1-i;n)))`	2 steps