For any graph
the_obj:GraphObject(the_graph). paren(V;depthfirst(the_obj)) & no_repeats(V+V;depthfirst(the_obj)) & df-traversal(the_graph;depthfirst(the_obj)) & depthfirst-traversal(the_graph;depthfirst(the_obj)) & (i:V. (inr(i) 
depthfirst(the_obj)) & (inl(i) depthfirst(the_obj)))
the_obj:GraphObject(the_graph), i:V. (inr(i) depthfirst(the_obj)) & (inl(i) depthfirst(the_obj))
[the_graph;the_obj]
the_obj:GraphObject(the_graph). paren(V;depthfirst(the_obj)) & no_repeats(V+V;depthfirst(the_obj))
[the_graph;the_obj]
the_obj:GraphObject(the_graph). df-traversal(the_graph;depthfirst(the_obj))
[the_graph;the_obj]
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))
| 1 | 1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. i:Vertices(the_graph). (inr(i) depthfirst(the_obj)) & (inl(i) depthfirst(the_obj))4. paren(Vertices(the_graph);depthfirst(the_obj)) 5. no_repeats(Vertices(the_graph)+Vertices(the_graph);depthfirst(the_obj)) 6. df-traversal(the_graph;depthfirst(the_obj)) 7. x: Vertices(the_graph) 8. y: Vertices(the_graph) Dec(x = y) | 1 step |
About:
 |  |  |  |  |  |  |  |