(inl(i) 
s') 
(inl(i) s1) (inl(i) s) (inr(i) s) v) (inl(i) s') (inl(i) s1) (inl(i) s) (inr(i) s)
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)
s1) (inl(u) s) (inr(u) s)
i:Vertices(the_graph).
(i v) (inl(i) s') (inl(i) dfs(the_obj;s;u)) (inr(i) dfs(the_obj;s;u))
[u / v])
(inl(i) s' @ s1) (inl(i) s) (inr(i) s)
x:T, l1,l2:T List. (x l1 @ l2) 
(x l1) (x l2)
0
l:T List, a,x:T. (x [a / l]) x = a (x l)
-1
| 1 | 21. i = u (inl(i) s') (inl(i) s1) (inl(i) s) (inr(i) s) | 1 step |
| 2 | 21. (i v) (inl(i) s') (inl(i) s1) (inl(i) s) (inr(i) s) | 3 steps |
About:
 |  |  |  |  |  |
 |  |  |  |  |
 |