1	2. i: Vertices(the_graph) 3. s1: (Vertices(the_graph)+Vertices(the_graph)) List 4. s2: (Vertices(the_graph)+Vertices(the_graph)) List 5. nil = (s1 @ [inr(i)] @ s2) 6. j: Vertices(the_graph) 7. (inr(j) s2) 8. (inl(j) s2) j-the_graph- > *i	1 step
2	2. i: Vertices(the_graph) 3. s1: (Vertices(the_graph)+Vertices(the_graph)) List 4. s2: (Vertices(the_graph)+Vertices(the_graph)) List 5. j:Vertices(the_graph). i-the_graph- > *j non-trivial-loop(the_graph;j) 6. nil = (s1 @ [inl(i)] @ s2) 7. j: Vertices(the_graph) 8. i-the_graph- > *j (inr(j) s2)	1 step

About: