For any graph
the_obj:GraphObject(the_graph), P:(Traversal
Prop). 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))
the_obj:GraphObject(the_graph). 
L:V List. no_repeats(V;L) & (y:V. (y 
L)) & depthfirst(the_obj) = dfsl(the_obj;L)
[the_graph;the_obj]
l,s. P(s)]
None
About:
| | | | | |
 |  |  |  |  |