traversal(the_graph)

i:Vertices(the_graph), s:traversal(the_graph). M([inl(i) / s])M(s)

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)

d:, s:traversal(the_graph), i:Vertices(the_graph). M(s)d dfs(the_obj;s;i) {s':traversal(the_graph)| M(s')d }

1

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 dfs(the_obj;s;i) {s':traversal(the_graph)| M(s')d }

8 steps

About: