traversal(the_graph)traversal(the_graph)Prop
s:traversal(the_graph), i:Vertices(the_graph). (inl(i) 
s) 
(inr(i) s) 
P(i,s,nil)
s1,s2,s3:traversal(the_graph), i,j:Vertices(the_graph).
i-the_graph- > j
paren(Vertices(the_graph);s2)
paren(Vertices(the_graph);s3) P(j,s1,s2) P(i,s2 @ s1,s3) P(i,s1,s3 @ s2)
s1,s2:traversal(the_graph), i:Vertices(the_graph).
(inl(i) s1) (inr(i) s1) P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
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)
((inl(i1) s1) (inr(i1) s1))
((inl(i1) s2) inl(i1) = inr(i1) Vertices(the_graph)+Vertices(the_graph))
| 1 | 15. P(i1,[inr(i1) / s1],s2) 16. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;[inr(i1) / s1]) 17. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) 18. paren(Vertices(the_graph);s2) 19. (inl(i1) s2) (inl(i1) s1) (inr(i1) s1) | 1 step |
| 2 | 15. P(i1,[inr(i1) / s1],s2) 16. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;[inr(i1) / s1]) 17. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) 18. paren(Vertices(the_graph);s2) 19. inl(i1) = inr(i1) Vertices(the_graph)+Vertices(the_graph) (inl(i1) s1) (inr(i1) s1) | 1 step |
About:
 |  |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |