At:
primrec list accum
2
1
1
1
1
1
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
upto(n-1-0;n-1) ~ nil
By:
RecUnfold `upto` 0
THEN
SplitOnConclITE
Generated subgoals:
None
About:
