L1-the_graph- > *j1 
i-the_graph- > *j1
i:Vertices(the_graph). (inl(i) 
s) 
L1-the_graph- > *i
(inl(i) s)
(inr(i) s2)
j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j
i@0:Vertices(the_graph), s1,s2@0:traversal(the_graph).
(([inl(i)] @ s2 @ [inr(i)]) @ s) = (s1 @ [inr(i@0)] @ s2@0) traversal(the_graph)
(j:Vertices(the_graph). (inr(j) s2@0) (inl(j) s2@0) j-the_graph- > *i@0)
i@0:Vertices(the_graph), s1,s2@0:traversal(the_graph).
(j:Vertices(the_graph). i@0-the_graph- > *j non-trivial-loop(the_graph;j))
(([inl(i)] @ s2 @ [inr(i)]) @ s) = (s1 @ [inl(i@0)] @ s2@0) traversal(the_graph)
(j:Vertices(the_graph). i@0-the_graph- > *j (inr(j) s2@0))
i@0:Vertices(the_graph). L1 @ [i]-the_graph- > *i@0 non-trivial-loop(the_graph;i@0)
L1@0,L2:Vertices(the_graph) List.
L1 = (L1@0 @ L2)
(
s1,s2:traversal(the_graph).
s = (s2 @ s1) traversal(the_graph)
& paren(Vertices(the_graph);s1) & paren(Vertices(the_graph);s2)
& (j:Vertices(the_graph).
((inl(j) s1) 
L1@0-the_graph- > *j)
& ((inl(j) s2) L2-the_graph- > *j & L1@0-the_graph- > *j)))
i:Vertices(the_graph). (inl(i) s) L1-the_graph- > *i
non-trivial-loop(the_graph;j1)
A,B:V List, i:V. A @ B-- > *i A-- > *i B-- > *i
0
i,j:V. [i]-- > *j i-the_graph- > *j
0
| 1 | L1-the_graph- > *j1 i-the_graph- > *j1 | 1 step |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |