At:
topsortl-properties
2
1
1.
the_graph: Graph
2.
the_obj: GraphObject(the_graph)
3.
L: Vertices(the_graph) List
4.
i:Vertices(the_graph). (i 
L)
5.
paren(Vertices(the_graph);dfsl(the_obj;L))
6.
no_repeats(Vertices(the_graph)+Vertices(the_graph);dfsl(the_obj;L))
7.
dfsl-traversal(the_graph;L;dfsl(the_obj;L))
8.
i:Vertices(the_graph). (i L) 
(inr(i) dfsl(the_obj;L)) & (inl(i) dfsl(the_obj;L))
9.
i: Vertices(the_graph)
(i topsortl(the_obj;L))
By:
Unfold `topsortl` 0
THEN
InstHyp [i] -2
THEN
EasyHyp
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
Generated subgoals:
None
About:
