(4steps total)
PrintForm
Definitions
Lemmas
graph
1
3
Sections
Graphs
Doc
At:
adjm-vertex-accum-properties
3
1.
M:
AdjMatrix
2.
T:
Type
3.
s:
T
4.
f:
T
M.size
T
primrec(M.size;s;
x',s'. f(s',x')) = list_accum(s',x'.f(s',x');s;upto(0;M.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:
(4steps total)
PrintForm
Definitions
Lemmas
graph
1
3
Sections
Graphs
Doc
M.sizeT
primrec(M.size;s;
x',s'. f(s',x')) = list_accum(s',x'.f(s',x');s;upto(0;M.size))
n:, f,x:Top. primrec(n;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n))
0