(6steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

At: depthfirst-df-traversal
For any graph the_obj:GraphObject(the_graph). df-traversal(the_graph;depthfirst(the_obj))
By:
Auto
THEN
Inst Thm* For any graph the_obj:GraphObject(the_graph), P:(TraversalProp). P(nil) (s:Traversal, i:V. P(s) P(dfs(the_obj;s;i))) P(depthfirst(the_obj)) [the_graph;the_obj;s. df-traversal(the_graph;s) & paren(Vertices(the_graph);s)]
Generated subgoals:

11. the_graph: Graph
2. the_obj: GraphObject(the_graph)
df-traversal(the_graph;nil)		1 step
 
21. the_graph: Graph
2. the_obj: GraphObject(the_graph)
paren(Vertices(the_graph);nil)		1 step
 
31. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. s: traversal(the_graph)
4. i: Vertices(the_graph)
5. df-traversal(the_graph;s)
6. paren(Vertices(the_graph);s)
df-traversal(the_graph;dfs(the_obj;s;i))		1 step
 
41. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. s: traversal(the_graph)
4. i: Vertices(the_graph)
5. df-traversal(the_graph;s)
6. paren(Vertices(the_graph);s)
paren(Vertices(the_graph);dfs(the_obj;s;i))		2 steps

About:
nilfunctionpropimpliesandall

(6steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc