At:
dfs-properties
2
1
1
1.
the_graph: Graph
2.
the_obj: GraphObject(the_graph)
3.
s: traversal(the_graph)
4.
i: Vertices(the_graph)
5.
s2: traversal(the_graph)
6.
(inl(i) 
s2) 
(inl(i) s) (inr(i) s)
7.
l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s)
8.
no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
9.
paren(Vertices(the_graph);s2)
10.
dfs(the_obj;s;i) = (s2 @ s)
11.
s1: traversal(the_graph)
12.
j:Vertices(the_graph). (inr(j) s1) 
i-the_graph- > *j
13.
dfs(the_obj;s;i) = (s1 @ s)
14.
s': traversal(the_graph)
15.
(inr(i) s) (inl(i) s) s' = nil
16.
(inr(i) s) & (inl(i) s)
(
s2:traversal(the_graph). s' = ([inl(i)] @ s2 @ [inr(i)]) traversal(the_graph))
17.
dfs(the_obj;s;i) = (s' @ s)
18.
(inr(i) s)
19.
(inl(i) s)
20.
s' = s2 (Vertices(the_graph)+Vertices(the_graph)) List
s2 = s'
By:
HypSubst -1 0
Generated subgoals:
None
About:
