2 | 24. y:Vertices(the_graph). (y [u / v])  i-the_graph- > y 25. s2:traversal(the_graph).
M(s2) < d

member-paren(x,y.the_obj.eq(x,y);i;s2)

( s':traversal(the_graph).
M(s' @ s2) M(s2) & P(i,s2,s') & list_accum(s',x'.dfs(the_obj;s';x');s2;v) = (s' @ s2)) s2:traversal(the_graph). M(s2) < d  member-paren(x,y.the_obj.eq(x,y);i;s2)  ( s':traversal(the_graph). M(s' @ s2) M(s2) & P(i,s2,s') & list_accum(s',x'.dfs(the_obj;s';x');dfs(the_obj;s2;u);v) = (s' @ s2)) | 7 steps |