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: