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

Auto
THEN
Inst Thm* dfs_induction2 [the_graph;the_obj;i,s1,s2. (inl(i) s2) (inl(i) s1) (inr(i) s1);s;i]

1	1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. s: traversal(the_graph) 4. i: Vertices(the_graph) 5. s1: traversal(the_graph) 6. i1: Vertices(the_graph) 7. (inl(i1) s1) (inr(i1) s1) (inl(i1) nil) (inl(i1) s1) (inr(i1) s1)	1 step
2	1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. s: traversal(the_graph) 4. i: Vertices(the_graph) 5. s1: traversal(the_graph) 6. s2: traversal(the_graph) 7. s3: traversal(the_graph) 8. i1: Vertices(the_graph) 9. j: Vertices(the_graph) 10. i1-the_graph- > j 11. paren(Vertices(the_graph);s2) 12. paren(Vertices(the_graph);s3) 13. (inl(j) s2) (inl(j) s1) (inr(j) s1) 14. (inl(i1) s3) (inl(i1) s2 @ s1) (inr(i1) s2 @ s1) (inl(i1) s3 @ s2) (inl(i1) s1) (inr(i1) s1)	3 steps
3	1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. s: traversal(the_graph) 4. i: Vertices(the_graph) 5. s1: traversal(the_graph) 6. s2: traversal(the_graph) 7. i1: Vertices(the_graph) 8. (inl(i1) s1) 9. (inr(i1) s1) 10. (inl(i1) s2) (inl(i1) [inr(i1) / s1]) (inr(i1) [inr(i1) / s1]) (inl(i1) [inl(i1) / (s2 @ [inr(i1)])]) (inl(i1) s1) (inr(i1) s1)	1 step

About: