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

At: topsort-properties 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))

By:
Unfold `topsort` 0
THEN
BackThru Thm* s:(A+B) List. no_repeats(A+B;s) no_repeats(A;mapoutl(s))


Generated subgoals:

None

About:
listunioninlinruniverseimpliesandall

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