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