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

At: primrec list accum 1

f,x:Top. primrec(0;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;0))

By:
RecUnfold `upto` 0
THEN
Reduce 0


Generated subgoals:

None

About:
natural_numberapplysqequaltopall

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