For any graph the_obj:GraphObject(the_graph), L:V List. paren(V;dfsl(the_obj;L)) & no_repeats(V+V;dfsl(the_obj;L)) & dfsl-traversal(the_graph;L;dfsl(the_obj;L)) & (i:V. (i L) (inr(i) dfsl(the_obj;L)) & (inl(i) dfsl(the_obj;L)))

UnivCD
THEN
Inst Thm* dfsl-induction2 [the_graph;the_obj;L,s. dfsl-traversal(the_graph;L;s)]

1	1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. L: Vertices(the_graph) List dfsl-traversal(the_graph;nil;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. dfsl-traversal(the_graph;L1;s) dfsl-traversal(the_graph;L1 @ [i];dfs(the_obj;s;i))	155 steps
3	1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. L: Vertices(the_graph) List 4. L:Vertices(the_graph) List. paren(Vertices(the_graph);dfsl(the_obj;L)) & no_repeats(Vertices(the_graph)+Vertices(the_graph);dfsl(the_obj;L)) & dfsl-traversal(the_graph;L;dfsl(the_obj;L)) paren(Vertices(the_graph);dfsl(the_obj;L)) & no_repeats(Vertices(the_graph)+Vertices(the_graph);dfsl(the_obj;L)) & dfsl-traversal(the_graph;L;dfsl(the_obj;L)) & (i:Vertices(the_graph). (i L) (inr(i) dfsl(the_obj;L)) & (inl(i) dfsl(the_obj;L)))	1 step

About: