(f(n-1,list_accum(i,y.f(y,i);x;upto(0;n-1)))) ~ list_accum(i,y.f(y,i);x;upto(0;n))
f,x:Top. primrec(n-1;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n-1))
x:Top. primrec(n-1;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n-1))
n = 0
(f(n-1,primrec(n-1;x;f))) ~ list_accum(i,y.f(y,i);x;upto(0;n))
| 1 | (f(n-1,list_accum(i,y.f(y,i);x;upto(0;n-1)))) ~ list_accum(i,y.f(y,i);x;upto(0;n)) | 10 steps |
About:
 |  |  |  |  |  |  |  |  |