(4steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

At: adjl-vertex-accum-properties 3
1. A: AdjList
2. T: Type
3. s: T
4. f: TA.sizeT
primrec(A.size;s;x',s'. f(s',x')) = list_accum(s',x'.f(s',x');s;upto(0;A.size))
By:
RWO Thm* n:, f,x:Top. primrec(n;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n)) 0
THEN
Reduce 0
Generated subgoals:

None

About:
natural_numberlambdaapplyfunctionuniverseequalsqequaltopall

(4steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc