x,s'. f(s';x))y,s'. if M.adj(x,y)
f(s';y) else s' fi)x,s'. f(s';x))
0 b else c(n-1,primrec(n-1;b;c)) fi (recursive)
is mentioned by
| Def adjl-vertex-accum(A;s',x.f(s';x);s) == primrec(A.size;s;x,s'. f(s';x)) | [adjl-vertex-accum] |
| Def adjm-edge-accum(M;s',x'.f(s';x');s;x) == primrec(M.size;s;y,s'. if M.adj(x,y) f(s';y) else s' fi) | [adjm-edge-accum] |
| Def adjm-vertex-accum(M;s',x.f(s';x);s) == primrec(M.size;s;x,s'. f(s';x)) | [adjm-vertex-accum] |
In prior sections: mb nat graph 1 1 mb list 1
Try larger context:
Graphs