At:
dfsl-properties
2
1
2
1
1.
the_graph: Graph
2.
the_obj: GraphObject(the_graph)
3.
L: Vertices(the_graph) List
4.
L1: Vertices(the_graph) List
5.
s: traversal(the_graph)
6.
i: Vertices(the_graph)
7.
paren(Vertices(the_graph);s)
8.
no_repeats(Vertices(the_graph)+Vertices(the_graph);s)
9.
dfsl-traversal(the_graph;L1;s)
10.
(inl(i) 
s)
11.
df-traversal(the_graph;s)
dfsl-traversal(the_graph;L1 @ [i];s)
By:
BackThru
Thm* For any graph
L1,L2:V List, s:Traversal. L1-- > *L2 
dfsl-traversal(the_graph;L1;s) dfsl-traversal(the_graph;L1 @ L2;s)
THEN
RWO
Thm* For any graph
A:V List, x:V. A-- > *[x] 
A-- > *x
0
THEN
Analyze 9
THEN
EasyHyp
Generated subgoals:
None
About:
