(inr(i) 
s2)
s1,s2@0:(Vertices(G)+Vertices(G)) List. s2 = (s1 @ [inr(i) / s2@0]) (inl(j) s2)
x,y:Vertices(G). Dec(x = y)
i:Vertices(G), s1,s2:traversal(G).
s = (s1 @ [inr(i)] @ s2) traversal(G)
(j:Vertices(G). (inr(j) s2) 
(inl(j) s2) j-G- > *i)
i:Vertices(G), s1,s2:traversal(G).
(j:Vertices(G). i-G- > *j non-trivial-loop(G;j))
s = (s1 @ [inl(i)] @ s2) traversal(G) (j:Vertices(G). i-G- > *j (inr(j) s2))
j:Vertices(G). i-G- > *j non-trivial-loop(G;j)
traversal(G)
j = i
s2)
(inl(j) s2)
(inl(j) s2)
s:T List, z:T. (z s) (s1,s2:T List. s = (s1 @ [z / s2]))
[Vertices(G)+Vertices(G);s2;inr(i)]
| 1 | (inr(i) s2) | 1 step |
| 2 | 18. s1,s2@0:(Vertices(G)+Vertices(G)) List. s2 = (s1 @ [inr(i) / s2@0]) (inl(j) s2) | 15 steps |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |