For any graph the_obj:GraphObject(the_graph), L:V List. (iL.(inr(i) dfsl(the_obj;L)) & (inl(i) dfsl(the_obj;L)))

Auto
THEN
Inst Thm* dfsl-induction2 [the_graph;the_obj;L,s. (iL.(inr(i) s) & (inl(i) s));L]

1	1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. L: Vertices(the_graph) List (inil.(inr(i) nil) & (inl(i) nil))	1 step
2	1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. L: Vertices(the_graph) List 4. L1: Vertices(the_graph) List 5. s: traversal(the_graph) 6. i: Vertices(the_graph) 7. paren(Vertices(the_graph);s) 8. no_repeats(Vertices(the_graph)+Vertices(the_graph);s) 9. (iL1.(inr(i) s) & (inl(i) s)) (i@0L1 @ [i].(inr(i@0) dfs(the_obj;s;i)) & (inl(i@0) dfs(the_obj;s;i)))	9 steps

About: