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

At: primrec list accum 2 1 1 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))
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. i:. i < n (z:Top. (f(n-1,list_accum(i,y.f(y,i);z;upto(n-1-i;n-1)))) ~ list_accum(i,y.f(y,i);z;upto(n-1-i;n)))
(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))
By:
InstHyp [n-1;x] -1
THEN
NthHypSq -1
THEN
RepeatFor 4 Analyze
Generated subgoals:

None

About:
intnatural_numbersubtractless_thanapplyequalsqequaltopimpliesall

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