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

At: depthfirst-df-traversal 3
1. 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))
By:
BackThru Thm* For any graph the_obj:GraphObject(the_graph), s:Traversal, i:V. df-traversal(the_graph;s) (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *i) df-traversal(the_graph;dfs(the_obj;s;i))
THEN
FwdThru Thm* s':(T+T) List. paren(T;s') (i:T. (inr(i) s') (inl(i) s')) [-4;-2]
Generated subgoals:

None

About:
listunioninlinruniverseimpliesall

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