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)
is mentioned by
| Thm* For any graph
L:V List, i:V, s:Traversal. (inr(i) s) dfl-traversal(the_graph;L;s) dfl-traversal(the_graph;L;[inl(i) / s]) | [dfl-traversal-consl] |
| Thm* For any graph
L:V List, i:V, s:Traversal. (j:V. (inr(j) s) (inl(j) s) j-the_graph- > *i) L-- > *i dfl-traversal(the_graph;L;s) dfl-traversal(the_graph;L;[inr(i) / s]) | [dfl-traversal-consr] |
| Thm* For any graph
L1,L2:V List, s:Traversal. L1-- > *L2 dfl-traversal(the_graph;L2;s) dfl-traversal(the_graph;L1;s) | [dfl-traversal-connect] |
Try larger context:
Graphs