s1,s2:traversal(the_graph), i:Vertices(the_graph).
P(i,s1,s2) 
l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)5.
s1,s2:traversal(the_graph), i:Vertices(the_graph).
P(i,s1,s2) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)6.
s:traversal(the_graph), i:Vertices(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s) P(i,s,nil)7.
s1,s2,s3:traversal(the_graph), i,j:Vertices(the_graph).
i-the_graph- > j P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)8.
s1,s2:traversal(the_graph), i:Vertices(the_graph).
member-paren(x,y.the_obj.eq(x,y);i;s1)
(j:Vertices(the_graph).
i-the_graph- > j j = i (inl(j) 
s2) 
member-paren(x,y.the_obj.eq(x,y);j;s1))
P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])9. M: traversal(the_graph)
10.
i:Vertices(the_graph), s:traversal(the_graph). M([inl(i) / s])
M(s)11.
i:Vertices(the_graph), s:traversal(the_graph).
member-paren(x,y.the_obj.eq(x,y);i;s) M([inr(i) / s]) < M(s)12. d:
13.
d1:.
d1 < d
(s:traversal(the_graph), i:Vertices(the_graph).
M(s)d1 (
s':traversal(the_graph). M(s' @ s)M(s) & P(i,s,s') & dfs(the_obj;s;i) = (s' @ s)))14. s: traversal(the_graph)
15. i: Vertices(the_graph)
16. M(s)
d17.
member-paren(x,y.the_obj.eq(x,y);i;s)
s':traversal(the_graph). M(s' @ s)M(s) & P(i,s,s') & [inl(i) / (the_obj.eacc((
s',j. dfs(the_obj;s';j)),[inr(i) / s],i))] = (s' @ s) traversal(the_graph)
