At:
dfs-dfl-traversal
1
1
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.
s3: traversal(the_graph)
11.
i: Vertices(the_graph)
12.
j: Vertices(the_graph)
13.
i-the_graph- > j
14.
paren(Vertices(the_graph);s2)
15.
k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k
16.
paren(Vertices(the_graph);s3)
17.
x-the_graph- > *i
18.
j:Vertices(the_graph). (inr(j) s1) (inl(j) s1) j-the_graph- > *i
19.
dfl-traversal(the_graph;L @ [x];s1)
20.
x-the_graph- > *j
21.
(j:Vertices(the_graph). (inr(j) s2 @ s1) (inl(j) s2 @ s1) j-the_graph- > *i)
dfl-traversal(the_graph;L @ [x];s2 @ s1) dfl-traversal(the_graph;L @ [x];s3 @ s2 @ s1)
j@0:Vertices(the_graph). (inr(j@0) s1) (inl(j@0) s1) j@0-the_graph- > *j
By:
Auto
THEN
InstHyp [j@0] -7
THEN
Connect
Generated subgoals:
None
About:
