At:
dfs-cases
2
2
1
1.
the_graph: Graph
2.
the_obj: GraphObject(the_graph)
3.
s: traversal(the_graph)
4.
i: Vertices(the_graph)
5.
x,y:Vertices(the_graph). the_obj.eq(x,y) 
x = y
6.
T:Type, s:T, x:Vertices(the_graph), f:(T
Vertices(the_graph)
T).
L:Vertices(the_graph) List.
(
y:Vertices(the_graph). x-the_graph- > y 
(y
L))
& the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L)
7.
T:Type, s:T, f:(T
Vertices(the_graph)
T).
L:Vertices(the_graph) List.
no_repeats(Vertices(the_graph);L)
& (
y:Vertices(the_graph). (y
L))
& the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L)
8.
((inl(i)
s)
(inr(i)
s))
9.
L:Vertices(the_graph) List, s:traversal(the_graph).
s2:traversal(the_graph). list_accum(s',j.dfs(the_obj;s';j);s;L) = (s2 @ s)
10.
L: Vertices(the_graph) List
11.
y:Vertices(the_graph). i-the_graph- > y 
(y
L)
12.
s2: traversal(the_graph)
13.
(inr(i)
s)
(inl(i)
s)
([inl(i)] @ s2 @ [inr(i)]) = nil
traversal(the_graph)
By:
Analyze 8
THEN
ObviousFrom [-1]
Generated subgoals:
None
About: