Nuprl - graph_1_3 LEMMAs for depthfirst

Rank	Theorem	Name
2	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]
cites
1	Thm* For any graph the_obj:GraphObject(the_graph), P:((V List)TraversalProp). P(nil,nil) (L:V List, s:Traversal, i:V. P(L,s) P(L @ [i],dfs(the_obj;s;i))) (L:V List. P(L,dfsl(the_obj;L)))	[dfsl-induction1]
1	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]