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), 0*Bollobas] p. 4, or "A walk (of length k) in a graph is a nonempty
alternating sequence v _{0} e_{0} v_{1} e_{1} ... e_{(k}-1) v_{k} of vertices and edges in
G such that e_{i} = { v_{i} , v_{i+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):

- Walks
- cewlks
- cwlks
- cwlkson
- df-ewlks
- df-wlks
- df-wlkson
- ewlksfval
- isewlk
- ewlkprop
- ewlkinedg
- ewlkle
- upgrewlkle2
- wkslem1
- wkslem2
- wksfval
- iswlk
- wlkprop
- wlkv
- iswlkg
- wlkf
- wlkcl
- wlkp
- wlkpwrd
- wlklenvp1
- wksv
- wlkn0
- wlklenvm1
- ifpsnprss
- wlkvtxeledg
- wlkvtxiedg
- relwlk
- wlkvv
- wlkop
- wlkcpr
- wlk2f
- wlkcomp
- wlkcompim
- wlkelwrd
- wlkeq
- edginwlk
- upgredginwlk
- iedginwlk
- wlkl1loop
- wlk1walk
- wlk1ewlk
- upgriswlk
- upgrwlkedg
- upgrwlkcompim
- wlkvtxedg
- upgrwlkvtxedg
- uspgr2wlkeq
- uspgr2wlkeq2
- uspgr2wlkeqi
- umgrwlknloop
- wlkRes
- wlkv0
- g0wlk0
- 0wlk0
- wlk0prc
- wlklenvclwlk
- wlklenvclwlkOLD
- wlkson
- iswlkon
- wlkonprop
- wlkpvtx
- wlkepvtx
- wlkoniswlk
- wlkonwlk
- wlkonwlk1l
- wlksoneq1eq2
- wlkonl1iedg
- wlkon2n0
- 2wlklem
- upgr2wlk
- wlkreslem
- wlkres
- redwlklem
- redwlk
- wlkp1lem1
- wlkp1lem2
- wlkp1lem3
- wlkp1lem4
- wlkp1lem5
- wlkp1lem6
- wlkp1lem7
- wlkp1lem8
- wlkp1
- wlkdlem1
- wlkdlem2
- wlkdlem3
- wlkdlem4
- wlkd

- Walks for loop-free graphs
- Trails
- Paths and simple paths
- cpths
- cspths
- cpthson
- cspthson
- df-pths
- df-spths
- df-pthson
- df-spthson
- relpths
- pthsfval
- spthsfval
- ispth
- isspth
- pthistrl
- spthispth
- pthiswlk
- spthiswlk
- pthdivtx
- pthdadjvtx
- 2pthnloop
- upgr2pthnlp
- spthdifv
- spthdep
- pthdepisspth
- upgrwlkdvdelem
- upgrwlkdvde
- upgrspthswlk
- upgrwlkdvspth
- pthsonfval
- spthson
- ispthson
- isspthson
- pthsonprop
- spthonprop
- pthonispth
- pthontrlon
- pthonpth
- isspthonpth
- spthonisspth
- spthonpthon
- spthonepeq
- uhgrwkspthlem1
- uhgrwkspthlem2
- uhgrwkspth
- usgr2wlkneq
- usgr2wlkspthlem1
- usgr2wlkspthlem2
- usgr2wlkspth
- usgr2trlncl
- usgr2trlspth
- usgr2pthspth
- usgr2pthlem
- usgr2pth
- usgr2pth0
- pthdlem1
- pthdlem2lem
- pthdlem2
- pthd

- Closed walks
- Circuits and cycles
- ccrcts
- ccycls
- df-crcts
- df-cycls
- crcts
- cycls
- iscrct
- iscycl
- crctprop
- cyclprop
- crctisclwlk
- crctistrl
- crctiswlk
- cyclispth
- cycliswlk
- cycliscrct
- cyclnspth
- cyclispthon
- lfgrn1cycl
- usgr2trlncrct
- umgrn1cycl
- uspgrn2crct
- usgrn2cycl
- crctcshwlkn0lem1
- crctcshwlkn0lem2
- crctcshwlkn0lem3
- crctcshwlkn0lem4
- crctcshwlkn0lem5
- crctcshwlkn0lem6
- crctcshwlkn0lem7
- crctcshlem1
- crctcshlem2
- crctcshlem3
- crctcshlem4
- crctcshwlkn0
- crctcshwlk
- crctcshtrl
- crctcsh

- Walks as words
- cwwlks
- cwwlksn
- cwwlksnon
- cwwspthsn
- cwwspthsnon
- df-wwlks
- df-wwlksn
- df-wwlksnon
- df-wspthsn
- df-wspthsnon
- wwlks
- iswwlks
- wwlksn
- iswwlksn
- wwlksnprcl
- iswwlksnx
- wwlkbp
- wwlknbp
- wwlknp
- wwlknbp1
- wwlknvtx
- wwlknllvtx
- wwlknlsw
- wspthsn
- iswspthn
- wspthnp
- wwlksnon
- wspthsnon
- iswwlksnon
- wwlksnon0
- wwlksonvtx
- iswspthsnon
- wwlknon
- wspthnon
- wspthnonp
- wspthneq1eq2
- wwlksn0s
- wwlkssswrd
- wwlksn0
- 0enwwlksnge1
- wwlkswwlksn
- wwlkssswwlksn
- wlkiswwlks1
- wlklnwwlkln1
- wlkiswwlks2lem1
- wlkiswwlks2lem2
- wlkiswwlks2lem3
- wlkiswwlks2lem4
- wlkiswwlks2lem5
- wlkiswwlks2lem6
- wlkiswwlks2
- wlkiswwlks
- wlkiswwlksupgr2
- wlkiswwlkupgr
- wlkswwlksf1o
- wlkswwlksen
- wwlksm1edg
- wlklnwwlkln2lem
- wlklnwwlkln2
- wlklnwwlkn
- wlklnwwlklnupgr2
- wlklnwwlknupgr
- wlknewwlksn
- wlknwwlksnbij
- wlknwwlksnen
- wlknwwlksneqs
- wwlkseq
- wwlksnred
- wwlksnext
- wwlksnextbi
- wwlksnredwwlkn
- wwlksnredwwlkn0
- wwlksnextwrd
- wwlksnextfun
- wwlksnextinj
- wwlksnextsurj
- wwlksnextbij0
- wwlksnextbij
- wwlksnexthasheq
- disjxwwlksn
- wwlksnndef
- wwlksnfi
- wlksnfi
- wlksnwwlknvbij
- wwlksnextproplem1
- wwlksnextproplem2
- wwlksnextproplem3
- wwlksnextprop
- disjxwwlkn
- hashwwlksnext
- wwlksnwwlksnon
- wspthsnwspthsnon
- wspthsnonn0vne
- wspthsswwlkn
- wspthnfi
- wwlksnonfi
- wspthsswwlknon
- wspthnonfi
- wspniunwspnon
- wspn0

- Walks/paths of length 2 (as length 3 strings)
- 2wlkdlem1
- 2wlkdlem2
- 2wlkdlem3
- 2wlkdlem4
- 2wlkdlem5
- 2pthdlem1
- 2wlkdlem6
- 2wlkdlem7
- 2wlkdlem8
- 2wlkdlem9
- 2wlkdlem10
- 2wlkd
- 2wlkond
- 2trld
- 2trlond
- 2pthd
- 2spthd
- 2pthond
- 2pthon3v
- umgr2adedgwlklem
- umgr2adedgwlk
- umgr2adedgwlkon
- umgr2adedgwlkonALT
- umgr2adedgspth
- umgr2wlk
- umgr2wlkon
- elwwlks2s3
- midwwlks2s3
- wwlks2onv
- elwwlks2ons3im
- elwwlks2ons3
- s3wwlks2on
- umgrwwlks2on
- wwlks2onsym
- elwwlks2on
- elwspths2on
- wpthswwlks2on
- 2wspdisj
- 2wspiundisj
- usgr2wspthons3
- usgr2wspthon
- elwwlks2
- elwspths2spth

- Walks in regular graphs
- Closed walks as words
- Examples for walks, trails and paths
- 0ewlk
- 1ewlk
- 0wlk
- is0wlk
- 0wlkonlem1
- 0wlkonlem2
- 0wlkon
- 0wlkons1
- 0trl
- is0trl
- 0trlon
- 0pth
- 0spth
- 0pthon
- 0pthon1
- 0pthonv
- 0clwlk
- 0clwlkv
- 0clwlk0
- 0crct
- 0cycl
- 1pthdlem1
- 1pthdlem2
- 1wlkdlem1
- 1wlkdlem2
- 1wlkdlem3
- 1wlkdlem4
- 1wlkd
- 1trld
- 1pthd
- 1pthond
- upgr1wlkdlem1
- upgr1wlkdlem2
- upgr1wlkd
- upgr1trld
- upgr1pthd
- upgr1pthond
- lppthon
- lp1cycl
- 1pthon2v
- 1pthon2ve
- wlk2v2elem1
- wlk2v2elem2
- wlk2v2e
- ntrl2v2e
- 3wlkdlem1
- 3wlkdlem2
- 3wlkdlem3
- 3wlkdlem4
- 3wlkdlem5
- 3pthdlem1
- 3wlkdlem6
- 3wlkdlem7
- 3wlkdlem8
- 3wlkdlem9
- 3wlkdlem10
- 3wlkd
- 3wlkond
- 3trld
- 3trlond
- 3pthd
- 3pthond
- 3spthd
- 3spthond
- 3cycld
- 3cyclpd
- upgr3v3e3cycl
- uhgr3cyclexlem
- uhgr3cyclex
- umgr3cyclex
- umgr3v3e3cycl
- upgr4cycl4dv4e

- Connected graphs