# Metamath Proof Explorer

A "walk" in a graph is usually defined for simple graphs, multigraphs or even pseudographs as "alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) where e(i) = x(i-1)x(i), 0Bollobas] p. 4, or "A walk (of length k) in a graph is a nonempty alternating sequence v0 e0 v1 e1 ... e(k-1) vk of vertices and edges in G such that ei = { vi , vi+1 } for all i < k.", see definition of [Diestel] p. 10.

Formalizing these definitions (mainly by representing the indexed vertices and edges by functions), a walk is represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges (e is a third function enumerating the edges within the graph, not within the walk), and p enumerates the vertices, see df-wlks. Hence a walk (of length n) is represented by the following sequence:

p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n).

Alternatively, one could define a walk as a function such that for all , and for all , and .

Based on our definition of , the class of all walks, more restrictive constructs are defined:

* (df-trls): A "walk is called a trail if all its edges are distinct.", see Definition of [Bollobas] p. 5, i.e., f(i) =/= f(j) if i =/= j.

* (df-pths): A path is a walk whose vertices except the first and the last vertex are distinct, i.e., p(i) =/= p(j) if i < j, except possibly when i = 0 and j = n.

* (simple paths, df-spths): A simple path"is a walk with distinct vertices.", see Notation of [Bollobas] p. 5, i.e., p(i) =/= p(j) if i =/= j.

* (closed walks, df-clwlks): A walk whose endvertices coincide is called a closed walk, i.e., p(0) = p(n).

* (df-crcts): "A trail whose endvertices coincide (a closed trail) is called a circuit." (see Definition of [Bollobas] p. 5), i.e., f(i) =/= f(j) if i =/= j and p(0) = p(n). Equivalently, a circuit is a closed walk with distinct edges.

* (df-cycls): A path whose endvertices coincide (a closed path) is called a cycle, i.e., p(i) =/= p(j) if i =/= j, except i = 0 and j = n, and p(0) = p(n). Equivalently, a cycle is a closed walk with distinct vertices.

* (Eulerian paths, df-eupth): An Eulerian path is "a trail containing all edges [of the graph]" (see definition in [Bollobas] p. 16), i.e., f(i) =/= f(j) if i =/= j and for all edges e(x) there is an 1 <= i <= n with e(x) = e(f(i)). Note, however, that an Eulerian path needs not be a path.

* Eulerian circuit: An Eulerian circuit (called Euler tour in the definition in [Diestel] p. 22) is "a circuit in a graph containing all the edges" (see definition in [Bollobas] p. 16), i.e., f(i) =/= f(j) if i =/= j, p(0) = p(n) and for all edges e(x) there is an 1 <= i <= n with e(x) = e(f(i)).

Hierarchy of all kinds of walks (apply ssriv and elopabran to the mentioned theorems to obtain the following subset relationships, as available for clwlkiswlk, see clwlkwlk and clwlkswks):

* Trails are walks (trliswlk):

* Paths are trails (pthistrl):

* Simple paths are paths (spthispth):

* Closed walks are walks (clwlkiswlk):

* Circuits are closed walks (crctisclwlk):

* Circuits are trails (crctistrl):

* Cycles are paths (cyclispth):

* Cycles are circuits (cycliscrct):

* (Non-trivial) cycles are not simple paths (cyclnspth):

* Eulerian paths are trails (eupthistrl):

Often, it is sufficient to refer to a walk by the natural sequence of its vertices, i.e., omitting its edges in its representation: p(0) p(1) ... p(n-1) p(n), see the corresponding remark in [Diestel] p. 6. The concept of a , see df-word, is the appropriate way to define such a sequence (being finite and starting at index 0) of vertices. Therefore, it is used in definition df-wwlks for , and the representation of a walk as sequence of its vertices is called "walk as word".

Only for simple pseudographs, however, the edges can be uniquely reconstructed from such a representation. In this case, the general definitions of walks and the definition of walks as words are equivalent, see wlkiswwlks. In other cases, there could be more than one edge between two adjacent vertices in the walk (in a multigraph), or two adjacent vertices could be connected by two different hyperedges involving additional vertices (in a hypergraph).

Based on this definition of , the class of all walks as word, more restrictive constructs are defined analogously to the general definition of a walk:

* (walks of length N as word, df-wwlksn): n = N

* (simple paths of length N as word, df-wspthsn): p(i) =/= p(j) if i =/= j and n = N

* (closed walks as word, df-clwwlk): p(0) = p(n)

* (closed walks of length N as word, df-clwwlkn): p(0) = p(n) and n = N

Finally, there are a couple of definitions for (special) walks having fixed endpoints and :

* Walks with particular endpoints (df-wlkson):

* Trails with particular endpoints (df-trlson):

* Paths with particular endpoints (df-pthson):

* Simple paths with particular endpoints (df-spthson):

* Walks of a fixed length as words with particular endpoints (df-wwlksnon):

* Simple paths of a fixed length as words with particular endpoints (df-wspthsnon):

* Closed Walks of a fixed length as words anchored at a particular vertex (df-wwlksnon):

1. Walks
2. Walks for loop-free graphs
3. Trails
4. Paths and simple paths
5. Closed walks
6. Circuits and cycles
7. Walks as words
8. Walks/paths of length 2 (as length 3 strings)
9. Walks in regular graphs
10. Closed walks as words
11. Examples for walks, trails and paths
12. Connected graphs