At:
depthfirst-dfsl
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)
By:
RepeatFor 2 (Analyze 0)
THEN
Unfolds [`depthfirst`;`dfsl`] 0
THEN
Inst
Thm* graphobj-properties
[the_graph;the_obj]
THEN
Analyze -1
THEN
Analyze -1
THEN
InstHyp [traversal(the_graph);nil;
s,i. dfs(the_obj;s;i)] -1
THEN
ReduceSOAps -1
THEN
NthHyp -1
Generated subgoals:
None
About:
