At:
dfs wf
1
1
1
1.
the_graph: Graph
2.
the_obj: GraphObject(the_graph)
3.
M: traversal(the_graph)

4.
i:Vertices(the_graph), s:traversal(the_graph). M([inl(i) / s])
M(s)
5.
i:Vertices(the_graph), s:traversal(the_graph).
member-paren(x,y.the_obj.eq(x,y);i;s) 
M([inr(i) / s]) < M(s)
6.
d:
7.
d1:
.
d1 < d

(
s:traversal(the_graph), i:Vertices(the_graph).
M(s)
d1 
dfs(the_obj;s;i)
{s':traversal(the_graph)| M(s')
d1 })
8.
s: traversal(the_graph)
9.
i: Vertices(the_graph)
10.
M(s)
d
11.
member-paren(x,y.the_obj.eq(x,y);i;s)
s
{s':traversal(the_graph)| M(s')
d }
By:
Analyze
Generated subgoals:
None
About: