For any graph
the_obj:GraphObject(the_graph), P:((V List)
TraversalProp). P(nil,nil) 
(L:V List, s:Traversal, i:V. paren(V;s) no_repeats(V+V;s) P(L,s) P(L @ [i],dfs(the_obj;s;i))) (L:V List. paren(V;dfsl(the_obj;L)) & no_repeats(V+V;dfsl(the_obj;L)) & P(L,dfsl(the_obj;L)))
l,s. paren(Vertices(the_graph);s) & no_repeats(Vertices(the_graph)+Vertices(the_graph);s) & P(l,s)]
s',s3:(T+T) List. paren(T;s') paren(T;s3) paren(T;s3 @ s'))
l1,l2:T List. no_repeats(T;l1 @ l2) 
l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2)
0)
None
About:
| | | | | | | |
 |  |  |  |  |  |  |