At:
topsortl-properties
2
2
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))
no_repeats(Vertices(the_graph);topsortl(the_obj;L))
By:
Unfold `topsortl` 0
THEN
BackThru
Thm* s:(A+B) List. no_repeats(A+B;s) no_repeats(A;mapoutl(s))
Generated subgoals:
None
About:
