A.size, edges = {p:(A.size
A.size)| 
(A.adj(1of(p),2of(p))) }, incidence = 
e.e > x,s'. f(s';x))size
size
Type
t:Graph. Vertices(t) Type| Some definitions of interest. | |
| adjm-graph | Def adjm-graph(A) == < vertices = A.size, edges = {p:(A.sizeA.size)| (A.adj(1of(p),2of(p))) }, incidence = e.e > |
| adjm-vertex-accum | Def adjm-vertex-accum(M;s',x.f(s';x);s) == primrec(M.size;s;x,s'. f(s';x)) |
| adjmatrix | Def AdjMatrix == size:sizesize |
| Thm* AdjMatrix Type | |
| gr_v | Def Vertices(t) == 1of(t) |
| Thm* t:Graph. Vertices(t) Type |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |