is mentioned by

Thm* For any graph the_obj:GraphObject(the_graph). paren(V;depthfirst(the_obj)) & no_repeats(V+V;depthfirst(the_obj)) & df-traversal(the_graph;depthfirst(the_obj)) & depthfirst-traversal(the_graph;depthfirst(the_obj)) & (i:V. (inr(i) depthfirst(the_obj)) & (inl(i) depthfirst(the_obj)))	[depthfirst-properties]
Thm* For any graph the_obj:GraphObject(the_graph). df-traversal(the_graph;depthfirst(the_obj))	[depthfirst-df-traversal]
Thm* For any graph the_obj:GraphObject(the_graph), i:V. (inr(i) depthfirst(the_obj)) & (inl(i) depthfirst(the_obj))	[depthfirst_member]
Thm* For any graph the_obj:GraphObject(the_graph). paren(V;depthfirst(the_obj)) & no_repeats(V+V;depthfirst(the_obj))	[depthfirst_paren]
Thm* For any graph the_obj:GraphObject(the_graph), P:(TraversalProp). P(nil) (s:Traversal, i:V. paren(V;s) no_repeats(V+V;s) P(s) P(dfs(the_obj;s;i))) paren(V;depthfirst(the_obj)) & no_repeats(V+V;depthfirst(the_obj)) & P(depthfirst(the_obj))	[depthfirst_induction2]
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))	[depthfirst_induction]
Thm* For any graph the_obj:GraphObject(the_graph). L:V List. no_repeats(V;L) & (y:V. (y L)) & depthfirst(the_obj) = dfsl(the_obj;L)	[depthfirst-dfsl]
Def topsort(G) == mapoutl(depthfirst(G))	[topsort]

Try larger context: Graphs