Vertices(the_graph)
(
x,y:Vertices(the_graph). 
(eq(x,y)) 
x = y)(eacc:(
T:Type. (TVertices(the_graph)T)TVertices(the_graph)T)(T:Type, s:T, x:Vertices(the_graph), f:(TVertices(the_graph)T). 
L:Vertices(the_graph) List. (y:Vertices(the_graph). x-the_graph- > y (y 
L)) & eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L))(vacc:(T:Type. (TVertices(the_graph)T)TT)(T:Type, s:T, f:(TVertices(the_graph)T). L:Vertices(the_graph) List. no_repeats(Vertices(the_graph);L) & (y:Vertices(the_graph). (y L)) & vacc(f,s) = list_accum(s',x'.f(s',x');s;L))Top))
is mentioned
In prior sections: graph 1 3