the_obj:GraphObject(the_graph), s:Traversal, i:V. dfs(the_obj;s;i) 
Traversalthe_obj:GraphObject(the_graph). 
M:(Traversal
). (i:V, s:Traversal. M([inl(i) / s])
M(s)) & (i:V, s:Traversal. 
member-paren(x,y.the_obj.eq(x,y);i;s) 
M([inr(i) / s]) < M(s))t:GraphObject(the_graph), T:Type. t.eacc (TVT)TVT