f,x:Top. primrec(0;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;0))
2. 0 < n
3.
f,x:Top. primrec(n-1;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n-1)) f,x:Top. primrec(n;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n))
n:
, f,x:Top. primrec(n;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n))
| 1 | f,x:Top. primrec(0;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;0)) | 1 step |
| 2 | 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)) f,x:Top. primrec(n;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n)) | 12 steps |
About:
 |  |  |  |  |