Nuprl - Proof: primrec list accum 2 1 1 1 1 2

(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
9. 0 < n

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

By: Subst (upto(n-1-0;n) ~ [(n-1)]) 0 THEN Reduce 0

Generated subgoals:

1 upto(n-1-0;n) ~ [(n-1)] 1 step

2 z@0:Top. (f(n-1,z@0)) ~ (f(n-1,z@0)) Auto

About:

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

1	`upto(n-1-0;n) ~ [(n-1)]`	1 step

2	`z@0:Top. (f(n-1,z@0)) ~ (f(n-1,z@0))`	Auto