1	1. the_graph: Graph df-traversal(the_graph;nil)	3 steps
2	1. the_graph: Graph 2. i: Vertices(the_graph) 3. (inl(i) nil) nil-the_graph- > *i	1 step
3	1. the_graph: Graph 2. i:Vertices(the_graph). nil-the_graph- > *i non-trivial-loop(the_graph;i) 3. L1: Vertices(the_graph) List 4. L2: Vertices(the_graph) List 5. nil = (L1 @ L2) s1,s2:traversal(the_graph). nil = (s2 @ s1) traversal(the_graph) & paren(Vertices(the_graph);s1) & paren(Vertices(the_graph);s2) & (j:Vertices(the_graph). ((inl(j) s1) L1-the_graph- > *j) & ((inl(j) s2) L2-the_graph- > *j & L1-the_graph- > *j))	8 steps

About: