traversal(the_graph)traversal(the_graph)Prop
s1,s2:traversal(the_graph), i:Vertices(the_graph).
P(i,s1,s2) 
l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)
s1,s2:traversal(the_graph), i:Vertices(the_graph).
P(i,s1,s2) no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
s:traversal(the_graph), i:Vertices(the_graph). member-paren(x,y.the_obj.eq(x,y);i;s) P(i,s,nil)
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)
s1,s2:traversal(the_graph), i:Vertices(the_graph).
member-paren(x,y.the_obj.eq(x,y);i;s1)
P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
i:Vertices(the_graph), s:traversal(the_graph). M([inl(i) / s])
M(s)
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)
x,y:Vertices(the_graph). the_obj.eq(x,y) 
x = y
T:Type, s:T, x:Vertices(the_graph), f:(TVertices(the_graph)T).
L:Vertices(the_graph) List.
(y:Vertices(the_graph). x-the_graph- > y (y 
L))
& the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L)
T:Type, s:T, f:(TVertices(the_graph)T).
L:Vertices(the_graph) List.
no_repeats(Vertices(the_graph);L)
& (y:Vertices(the_graph). (y L))
& the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L)
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)))
d
member-paren(x,y.the_obj.eq(x,y);i;s)
(y:Vertices(the_graph). (y nil) i-the_graph- > y) (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') & s2 = (s' @ s2) traversal(the_graph)))
None
About:
| | | | | | | | | |
 |  |  |  |  |  |  |  |