the_obj:GraphObject(the_graph), L:V List. paren(V;dfsl(the_obj;L)) & no_repeats(V+V;dfsl(the_obj;L)) & dfsl-traversal(the_graph;L;dfsl(the_obj;L)) & (i:V. (i 
L) 
(inr(i) dfsl(the_obj;L)) & (inl(i) dfsl(the_obj;L)))i:Vertices(the_graph). (inl(i) s) L-the_graph- > *i) & ((i:Vertices(the_graph). L-the_graph- > *i 
non-trivial-loop(the_graph;i)) (L1,L2:Vertices(the_graph) List. L = (L1 @ L2) (
s1,s2:traversal(the_graph). s = (s2 @ s1) traversal(the_graph) & paren(Vertices(the_graph);s1) & paren(Vertices(the_graph);s2) & (j:Vertices(the_graph). ((inl(j) s1) 
L1-the_graph- > *j) & ((inl(j) s2) L2-the_graph- > *j & L1-the_graph- > *j)))))
is mentioned by
| Thm* For any graph
the_obj:GraphObject(the_graph), L:V List. paren(V;dfsl(the_obj;L)) & no_repeats(V+V;dfsl(the_obj;L)) & dfsl-traversal(the_graph;L;dfsl(the_obj;L)) & (i:V. (i L) (inr(i) dfsl(the_obj;L)) & (inl(i) dfsl(the_obj;L))) | [dfsl-properties] |
In prior sections: graph 1 2
Try larger context:
Graphs