i:Vertices(the_graph). (inl(i) 
s) 
L1-the_graph- > *i
i:Vertices(the_graph). L1-the_graph- > *i 
non-trivial-loop(the_graph;i))
(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))))
(inl(i) s)
(inr(i) s2)
j:Vertices(the_graph). (inr(j) s2) i-the_graph- > *j
i@0:Vertices(the_graph). (inl(i@0) ([inl(i)] @ s2 @ [inr(i)]) @ s) L1 @ [i]-the_graph- > *i@0
x:T, l1,l2:T List. (x l1 @ l2) (x l1) 
(x l2)
0
a,x:T. (x [a]) x = a
0
A,B:V List, i:V. A @ B-- > *i A-- > *i B-- > *i
0
| 1 | 20. i@0: Vertices(the_graph) 21. inl(i@0) = inl(i) Vertices(the_graph)+Vertices(the_graph) L1-the_graph- > *i@0 [i]-the_graph- > *i@0 | 4 steps |
| 2 | 20. i@0: Vertices(the_graph) 21. (inl(i@0) s2) L1-the_graph- > *i@0 [i]-the_graph- > *i@0 | 4 steps |
| 3 | 20. i@0: Vertices(the_graph) 21. inl(i@0) = inr(i) Vertices(the_graph)+Vertices(the_graph) L1-the_graph- > *i@0 [i]-the_graph- > *i@0 | 1 step |
| 4 | 20. i@0: Vertices(the_graph) 21. (inl(i@0) s) L1-the_graph- > *i@0 [i]-the_graph- > *i@0 | 1 step |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |
 |