(11steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

At: topsort-properties 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))
By: Unfold `topsorted` 0
Generated subgoal:

19. i: Vertices(the_graph)
10. j: Vertices(the_graph)
11. i-the_graph- > *j
12. i = j
i before j topsort(the_obj)		7 steps

About:
unioninlinrandall

(11steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc