(Vertices(the_graph)+Vertices(the_graph)) List
s2 = s' 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))
(inr(i) s)
(inl(i) s)
s2 = s'
x,y,z:T List. (x @ z) = (y @ z) 
x = y
-1
| 1 | 20. s' = s2 (Vertices(the_graph)+Vertices(the_graph)) List s2 = s' | 1 step |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |
 |