x,y:Vertices(the_graph). the_obj.eq(x,y) 
x = y
T:Type, s:T, x:Vertices(the_graph), f:(T
Vertices(the_graph)T).
L:Vertices(the_graph) List.
(y:Vertices(the_graph). x-the_graph- > y (y 
L))
& the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L)
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))
& the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L)
s) 
(inr(i) s)
s':traversal(the_graph). ((inr(i) s) (inl(i) s) 
s' = nil) & (
(inr(i) s) & (inl(i) s) (s2:traversal(the_graph). s' = ([inl(i)] @ s2 @ [inr(i)]) traversal(the_graph))) & s = (s' @ s) traversal(the_graph)
None
About:
| | | | | | | | |
 |  |  |  |  |  |  |