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

At: depthfirst wf

For any graph the_obj:GraphObject(the_graph). depthfirst(the_obj) Traversal

By: Unfold `depthfirst` 0

Generated subgoal:

11. the_graph: Graph
2. the_obj: GraphObject(the_graph)
the_obj.vacc((s,i. dfs(the_obj;s;i)),nil) traversal(the_graph)
1 step

About:
nillambdaapplymemberall

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