G:Graph. (x,y:Vertices(G). Dec(x = y)) 
(s:traversal(G). paren(Vertices(G);s) no_repeats(Vertices(G)+Vertices(G);s) df-traversal(G;s) depthfirst-traversal(G;s))i:Vertices(the_graph), s1,s2:traversal(the_graph). (j:Vertices(the_graph). i-the_graph- > *j 
non-trivial-loop(the_graph;j)) s = (s1 @ [inl(i)] @ s2) 
traversal(the_graph) (j:Vertices(the_graph). j = i i-the_graph- > *j (inl(j) s2))
is mentioned by
| Thm* G:Graph. (x,y:Vertices(G). Dec(x = y)) (s:traversal(G). paren(Vertices(G);s) no_repeats(Vertices(G)+Vertices(G);s) df-traversal(G;s) depthfirst-traversal(G;s)) | [paren-df-traversal] |
Try larger context:
Graphs