For any graph the_obj:GraphObject(the_graph), l:V List, s:Traversal. s':Traversal. (i:V. (i l) (inl(i) s') (inl(i) s) (inr(i) s)) & l_disjoint(V+V;s';s) & no_repeats(V+V;s') & paren(V;s') & list_accum(s',j.dfs(the_obj;s';j);s;l) = (s' @ s)

1	1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. l: Vertices(the_graph) List 4. s: traversal(the_graph) s':traversal(the_graph). (i:Vertices(the_graph). (i nil) (inl(i) s') (inl(i) s) (inr(i) s)) & l_disjoint(Vertices(the_graph)+Vertices(the_graph);s';s) & no_repeats(Vertices(the_graph)+Vertices(the_graph);s') & paren(Vertices(the_graph);s') & s = (s' @ s) traversal(the_graph)	5 steps
2	1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. l: Vertices(the_graph) List 4. u: Vertices(the_graph) 5. v: Vertices(the_graph) List 6. s:traversal(the_graph). s':traversal(the_graph). (i:Vertices(the_graph). (i v) (inl(i) s') (inl(i) s) (inr(i) s)) & l_disjoint(Vertices(the_graph)+Vertices(the_graph);s';s) & no_repeats(Vertices(the_graph)+Vertices(the_graph);s') & paren(Vertices(the_graph);s') & list_accum(s',j.dfs(the_obj;s';j);s;v) = (s' @ s) 7. s: traversal(the_graph) s':traversal(the_graph). (i:Vertices(the_graph). (i [u / v]) (inl(i) s') (inl(i) s) (inr(i) s)) & l_disjoint(Vertices(the_graph)+Vertices(the_graph);s';s) & no_repeats(Vertices(the_graph)+Vertices(the_graph);s') & paren(Vertices(the_graph);s') & list_accum(s',j.dfs(the_obj;s';j);dfs(the_obj;s;u);v) = (s' @ s)	10 steps

About: