x,y:Vertices(the_graph). the_obj.eq(x,y) x = y

T:Type, s:T, x:Vertices(the_graph), f:(TVertices(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)

T:Type, s:T, f:(TVertices(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)

((inl(i) s) (inr(i) s))

s:traversal(the_graph). s2:traversal(the_graph). list_accum(s',j.dfs(the_obj;s';j);s;v) = (s2 @ s)

s2:traversal(the_graph). list_accum(s',j.dfs(the_obj;s';j);dfs(the_obj;s1;u);v) = (s2 @ s1)

1

14. s2: traversal(the_graph) 15. list_accum(s',j.dfs(the_obj;s';j);dfs(the_obj;s1;u);v) = (s2 @ dfs(the_obj;s1;u)) 16. s': traversal(the_graph) 17. (inl(u) s') (inl(u) s1) (inr(u) s1) 18. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s';s1) 19. no_repeats(Vertices(the_graph)+Vertices(the_graph);s') 20. paren(Vertices(the_graph);s') 21. dfs(the_obj;s1;u) = (s' @ s1) s2@0:traversal(the_graph). (s2 @ s' @ s1) = (s2@0 @ s1) traversal(the_graph)

1 step

About: