||s1|| = ||s2|| 
(s1 @ s) = (s2 @ s) (Vertices(the_graph)+Vertices(the_graph)) List s2) 
(inl(i) s) (inr(i) s)
j:Vertices(the_graph). (inr(j) s1) 
i-the_graph- > *j
s) (inl(i) s) s' = nil
(inr(i) s) & (inl(i) s)
(
s2:traversal(the_graph). s' = ([inl(i)] @ s2 @ [inr(i)]) traversal(the_graph))
s2)
s1 = s2
x1,z,x2,x3:T List. ||x1|| = ||z|| (x1 @ x2) = (z @ x3) x1 = z & x2 = x3
[Vertices(the_graph)+Vertices(the_graph);s1;s2;s;s]
| 1 | ||s1|| = ||s2|| | 1 step |
| 2 | (s1 @ s) = (s2 @ s) (Vertices(the_graph)+Vertices(the_graph)) List | 1 step |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |