y,s'. if M.adj(x,y)
f(s';y) else s' fi)
A.size, edges = {p:(A.size
A.size)| 
(A.adj(1of(p),2of(p))) }, incidence = e.e > size
size
Type
t:Graph. Vertices(t) Type| Some definitions of interest. | |
| adjm-edge-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-graph | Def adjm-graph(A) == < vertices = A.size, edges = {p:(A.sizeA.size)| (A.adj(1of(p),2of(p))) }, incidence = e.e > |
| adjmatrix | Def AdjMatrix == size:sizesize |
| Thm* AdjMatrix Type | |
| gr_v | Def Vertices(t) == 1of(t) |
| Thm* t:Graph. Vertices(t) Type |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |