At:
dfs-dfl-traversal
2
1
2
1.
the_graph: Graph
2.
the_obj: GraphObject(the_graph)
3.
L: Vertices(the_graph) List
4.
s: traversal(the_graph)
5.
x: Vertices(the_graph)
6.
dfl-traversal(the_graph;L;s)
7.
j:Vertices(the_graph). (inr(j) 
s) 
(inl(j) s) j-the_graph- > *x
8.
s1: traversal(the_graph)
9.
s2: traversal(the_graph)
10.
i: Vertices(the_graph)
11.
(inr(i) s1)
12.
(inl(i) s1)
13.
paren(Vertices(the_graph);s2)
14.
l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)
15.
no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
16.
j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j
17.
j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) 
(inl(j) s1) (inr(j) s1)
18.
x-the_graph- > *i
19.
j:Vertices(the_graph). (inr(j) s1) (inl(j) s1) j-the_graph- > *i
20.
dfl-traversal(the_graph;L @ [x];s1)
21.
j: Vertices(the_graph)
22.
(inr(j) s1)
23.
(inl(j) [inr(i) / s1])
j-the_graph- > *i
By:
BackThruSomeHyp
THEN
ObviousFrom [-1]
Generated subgoals:
None
About:
