t:AdjMatrix. t.adj 
t.size
t.size
y,s'. if M.adj(x,y)
f(s';y) else s' fi)x,s'. f(s';x))A.size, edges = {p:(A.size
A.size)| 
(A.adj(1of(p),2of(p))) }, incidence = e.e > is mentioned by
| Thm* t:AdjMatrix. t.adj t.sizet.size | [adjm_adj_wf] |
| 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] |
| Def adjm-graph(A) == < vertices = A.size, edges = {p:(A.sizeA.size)| (A.adj(1of(p),2of(p))) }, incidence = e.e > | [adjm-graph] |
Try larger context:
Graphs