Vertices(the_graph)+Vertices(the_graph)
j = i
j:Vertices(the_graph). (inr(j) s) 
(inl(j) s) j-the_graph- > *i
i:Vertices(the_graph), s1,s2:traversal(the_graph).
s = (s1 @ [inr(i)] @ s2) traversal(the_graph)
(j:Vertices(the_graph). (inr(j) s2) (inl(j) s2) j-the_graph- > *i)
j:Vertices(the_graph). (inr(j) s) L-the_graph- > *j
i:Vertices(the_graph), s1,s2:traversal(the_graph).
(j:Vertices(the_graph). i-the_graph- > *j non-trivial-loop(the_graph;j))
s = (s1 @ [inl(i)] @ s2) traversal(the_graph) L-the_graph- > *i
[inr(i) / s])
L-the_graph- > *j
l:T List, a,x:T. (x [a / l]) 
x = a 
(x l)
-1
| 1 | 11. inr(j) = inr(i) Vertices(the_graph)+Vertices(the_graph) j = i | 1 step |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |