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

At: depthfirst wf 1
1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
the_obj.vacc((s,i. dfs(the_obj;s;i)),nil) traversal(the_graph)
By: Inst Thm* For any graph t:GraphObject(the_graph), T:Type. t.vacc (TVT)TT [the_graph;the_obj;traversal(the_graph)]
Generated subgoals:

None

About:
nillambdaapplyfunctionuniversememberall

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