At:
dfsl member
2
1
1
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.
i:Vertices(the_graph). (i 
L1) 
(inr(i) s)
10.
i:Vertices(the_graph). (i L1) (inl(i) s)
11.
s': traversal(the_graph)
12.
(inl(i) s') 
(inl(i) s) (inr(i) s)
13.
l_disjoint(Vertices(the_graph)+Vertices(the_graph);s';s)
14.
no_repeats(Vertices(the_graph)+Vertices(the_graph);s')
15.
paren(Vertices(the_graph);s')
16.
dfs(the_obj;s;i) = (s' @ s)
17.
i@0: Vertices(the_graph)
18.
(i@0 L1)
(inr(i@0) s') (inr(i@0) s) & (inl(i@0) s') (inl(i@0) s)
By:
Obvious
Generated subgoals:
None
About:
