Nuprl - graph_1_3 LEMMAs for depthfirst

Rank	Theorem	Name
15	Thm* For any graph the_obj:GraphObject(the_graph), i:V. (inr(i) depthfirst(the_obj)) & (inl(i) depthfirst(the_obj))	[depthfirst_member]
cites
14	Thm* For any graph the_obj:GraphObject(the_graph), L:V List. (iL.(inr(i) dfsl(the_obj;L)) & (inl(i) dfsl(the_obj;L)))	[dfsl_member]
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]