l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;[inr(i1)]) no_repeats(Vertices(the_graph)+Vertices(the_graph);[inr(i1)]) 
((inl(i1) 
s2) 
inl(i1) = inr(i1) Vertices(the_graph)+Vertices(the_graph))
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)
(k:Vertices(the_graph). (inr(k) s2) j-the_graph- > *k)
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).
(inr(i) s1)
(inl(i) s1)
paren(Vertices(the_graph);s2)
l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1)
no_repeats(Vertices(the_graph)+Vertices(the_graph);s2)
(j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j)
(j:Vertices(the_graph). i-the_graph- > j j = i (inl(j) s2) (inl(j) s1) (inr(j) s1))
P(i,[inr(i) / s1],s2) P(i,s1,[inl(i) / (s2 @ [inr(i)])])
member-paren(x,y.the_obj.eq(x,y);i1;s1)
j:Vertices(the_graph).
i1-the_graph- > j j = i1 (inl(j) s2) member-paren(x,y.the_obj.eq(x,y);j;s1)
j:Vertices(the_graph). (inr(j) s2) i1-the_graph- > *j
no_repeats(Vertices(the_graph)+Vertices(the_graph);[inl(i1) / (s2 @ [inr(i1)])])
l:T List, x:T. no_repeats(T;[x / l]) 
no_repeats(T;l) & (x l)
0
l1,l2:T List. no_repeats(T;l1 @ l2) l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2)
0)
x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2)
0)
a,x:T. (x [a]) x = a
0)
| 1 | l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;[inr(i1)]) | 2 steps |
| 2 | no_repeats(Vertices(the_graph)+Vertices(the_graph);[inr(i1)]) | 1 step |
| 3 | ((inl(i1) s2) inl(i1) = inr(i1) Vertices(the_graph)+Vertices(the_graph)) | 3 steps |
About:
 |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |