G.size, edges = x:G.size
||G.out(x)||, incidence = 
e. < 1of(e),(G.out(1of(e)))[2of(e)] > > x,s'. f(s';x))size
(size List)
Type
t:Graph. Vertices(t) Type| Some definitions of interest. | |
| adjl-graph | Def adjl-graph(G) == < vertices = G.size, edges = x:G.size||G.out(x)||, incidence = e. < 1of(e),(G.out(1of(e)))[2of(e)] > > |
| adjl-vertex-accum | Def adjl-vertex-accum(A;s',x.f(s';x);s) == primrec(A.size;s;x,s'. f(s';x)) |
| adjlist | Def AdjList == size:size(size List) |
| Thm* AdjList Type | |
| gr_v | Def Vertices(t) == 1of(t) |
| Thm* t:Graph. Vertices(t) Type |
About:
 |  |  |  |  |  |
 |  |  |  |  |
 |