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