At:
topsort-properties
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))
By:
Unfold `topsort` 0
THEN
RWO
Thm* s:(A+B) List, x:A. (x mapoutl(s)) 
(
y:A+B. (y s) & isl(y) & x = outl(y))
0
THEN
InstConcl [inl(i)]
THEN
Reduce 0
THEN
InstHyp [i] -2
Generated subgoals:
None
About:
