the_obj:GraphObject(the_graph), L:V List, s:Traversal, x:V. dfl-traversal(the_graph;L;s) 
(j:V. (inr(j) 
s) 
(inl(j) s) j-the_graph- > *x) dfl-traversal(the_graph;L @ [x];dfs(the_obj;s;x))i:Vertices(the_graph), s1,s2:traversal(the_graph). s = (s1 @ [inr(i)] @ s2) traversal(the_graph) (j:Vertices(the_graph). (inr(j) s2) (inl(j) s2) j-the_graph- > *i)) & (j:Vertices(the_graph). (inr(j) s) L-the_graph- > *j) & (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) L-the_graph- > *i)
is mentioned by
| Thm* For any graph
the_obj:GraphObject(the_graph), L:V List, s:Traversal, x:V. dfl-traversal(the_graph;L;s) (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *x) dfl-traversal(the_graph;L @ [x];dfs(the_obj;s;x)) | [dfs-dfl-traversal] |
In prior sections: graph 1 2
Try larger context:
Graphs