For any graph the_obj:GraphObject(the_graph). (non-trivial-loop-free(the_graph) topsorted(the_graph;topsort(the_obj))) & (i:V. (i topsort(the_obj))) & no_repeats(V;topsort(the_obj))

RepeatFor 2 (Analyze 0)
THEN
Inst Thm* 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_graph;the_obj]

1	1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. paren(Vertices(the_graph);depthfirst(the_obj)) 4. no_repeats(Vertices(the_graph)+Vertices(the_graph);depthfirst(the_obj)) 5. df-traversal(the_graph;depthfirst(the_obj)) 6. depthfirst-traversal(the_graph;depthfirst(the_obj)) 7. i:Vertices(the_graph). (inr(i) depthfirst(the_obj)) & (inl(i) depthfirst(the_obj)) 8. non-trivial-loop-free(the_graph) topsorted(the_graph;topsort(the_obj))	8 steps
2	1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. paren(Vertices(the_graph);depthfirst(the_obj)) 4. no_repeats(Vertices(the_graph)+Vertices(the_graph);depthfirst(the_obj)) 5. df-traversal(the_graph;depthfirst(the_obj)) 6. depthfirst-traversal(the_graph;depthfirst(the_obj)) 7. i:Vertices(the_graph). (inr(i) depthfirst(the_obj)) & (inl(i) depthfirst(the_obj)) 8. i: Vertices(the_graph) (i topsort(the_obj))	1 step
3	1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. paren(Vertices(the_graph);depthfirst(the_obj)) 4. no_repeats(Vertices(the_graph)+Vertices(the_graph);depthfirst(the_obj)) 5. df-traversal(the_graph;depthfirst(the_obj)) 6. depthfirst-traversal(the_graph;depthfirst(the_obj)) 7. i:Vertices(the_graph). (inr(i) depthfirst(the_obj)) & (inl(i) depthfirst(the_obj)) no_repeats(Vertices(the_graph);topsort(the_obj))	1 step

About: