For any graph the_obj:GraphObject(the_graph), L:V List, s:Traversal, x:V. dfl-traversal(the_graph;L;s) (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *x) dfl-traversal(the_graph;L @ [x];dfs(the_obj;s;x))

Auto
THEN
Inst Thm* dfs_induction4 [the_graph;the_obj;i,s1,s2. x-the_graph- > *i (j:Vertices(the_graph). (inr(j) s1) (inl(j) s1) j-the_graph- > *i) dfl-traversal(the_graph;L @ [x];s1) dfl-traversal(the_graph;L @ [x];s2 @ s1);s;x]
THEN
Reduce 0

1	1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. L: Vertices(the_graph) List 4. s: traversal(the_graph) 5. x: Vertices(the_graph) 6. dfl-traversal(the_graph;L;s) 7. j:Vertices(the_graph). (inr(j) s) (inl(j) s) j-the_graph- > *x 8. s1: traversal(the_graph) 9. s2: traversal(the_graph) 10. s3: traversal(the_graph) 11. i: Vertices(the_graph) 12. j: Vertices(the_graph) 13. i-the_graph- > j 14. paren(Vertices(the_graph);s2) 15. k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k 16. paren(Vertices(the_graph);s3) 17. x-the_graph- > *j (j@0:Vertices(the_graph). (inr(j@0) s1) (inl(j@0) s1) j@0-the_graph- > *j) dfl-traversal(the_graph;L @ [x];s1) dfl-traversal(the_graph;L @ [x];s2 @ s1) 18. x-the_graph- > *i (j:Vertices(the_graph). (inr(j) s2 @ s1) (inl(j) s2 @ s1) j-the_graph- > *i) dfl-traversal(the_graph;L @ [x];s2 @ s1) dfl-traversal(the_graph;L @ [x];s3 @ s2 @ s1) 19. x-the_graph- > *i 20. j:Vertices(the_graph). (inr(j) s1) (inl(j) s1) j-the_graph- > *i 21. dfl-traversal(the_graph;L @ [x];s1) dfl-traversal(the_graph;L @ [x];(s3 @ s2) @ s1)	7 steps
2	1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. L: Vertices(the_graph) List 4. s: traversal(the_graph) 5. x: Vertices(the_graph) 6. dfl-traversal(the_graph;L;s) 7. j:Vertices(the_graph). (inr(j) s) (inl(j) s) j-the_graph- > *x 8. s1: traversal(the_graph) 9. s2: traversal(the_graph) 10. i: Vertices(the_graph) 11. (inr(i) s1) 12. (inl(i) s1) 13. paren(Vertices(the_graph);s2) 14. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) 15. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) 16. j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j 17. j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1) 18. x-the_graph- > *i (j:Vertices(the_graph). (inr(j) [inr(i) / s1]) (inl(j) [inr(i) / s1]) j-the_graph- > *i) dfl-traversal(the_graph;L @ [x];[inr(i) / s1]) dfl-traversal(the_graph;L @ [x];s2 @ [inr(i) / s1]) 19. x-the_graph- > *i 20. j:Vertices(the_graph). (inr(j) s1) (inl(j) s1) j-the_graph- > *i 21. dfl-traversal(the_graph;L @ [x];s1) dfl-traversal(the_graph;L @ [x];[inl(i) / ((s2 @ [inr(i)]) @ s1)])	8 steps
3	1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. L: Vertices(the_graph) List 4. s: traversal(the_graph) 5. x: Vertices(the_graph) 6. dfl-traversal(the_graph;L;s) 7. j:Vertices(the_graph). (inr(j) s) (inl(j) s) j-the_graph- > *x 8. s':traversal(the_graph). (x-the_graph- > *x (j:Vertices(the_graph). (inr(j) s) (inl(j) s) j-the_graph- > *x) dfl-traversal(the_graph;L @ [x];s) dfl-traversal(the_graph;L @ [x];s' @ 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') & (j:Vertices(the_graph). (inr(j) s') x-the_graph- > *j) & dfs(the_obj;s;x) = (s' @ s) dfl-traversal(the_graph;L @ [x];dfs(the_obj;s;x))	2 steps

About: