Metamath Proof Explorer


Table of Contents - 17.3.10. Closed walks as words

In general, a closed walk is an alternating sequence of vertices and edges, as defined in df-clwlks: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n), with p(n) = p(0). Often, it is sufficient to refer to a walk by the (cyclic) sequence of its vertices, i.e omitting its edges in its representation: p(0) p(1) ... p(n-1) p(0), see the corresponding remark on cycles (which are special closed walks) in [Diestel] p. 7. As for "walks as words" in general, the concept of a , see df-word, is also used in Definitions df-clwwlk and df-clwwlkn, and the representation of a closed walk as the sequence of its vertices is called "closed walk as word".

In contrast to "walks as words", the terminating vertex p(n) of a closed walk is omitted in the representation of a closed walk as word, see definitions df-clwwlk, df-clwwlkn and df-clwwlknon, because it is always equal to the first vertex of the closed walk. This represenation has the advantage that the vertices can be cyclically shifted without changing the represented closed walk. Furthermore, the length of a closed walk (i.e. the number of its edges) equals the number of symbols/vertices of the word representing the closed walk.

To avoid to handle the degenerate case of representing a (closed) walk of length 0 by the empty word, this case is excluded within the definition (). This is because a walk of length 0 is anchored at an arbitrary vertex by the general definition for closed walks, see 0clwlkv, which neither can be reflected by the empty word nor by a singleton word with vertex v : represents the walk "", which is a (closed) walk of length 1 (if there is an edge/loop from to ), see loopclwwlkn1b.

Therefore, a closed walk corresponds to a closed walk as word only for walks of length at least 1, see clwlkclwwlk2 or clwlkclwwlken. Although the set of all closed walks of a fixed length as words over the set of vertices is defined as function over , the fixed length is usually not 0, because (see clwwlkn0).

Analogous to , the set of walks of a fixed length between two vertices and , the set of closed walks of a fixed length anchored at a fixed vertex is defined by df-clwwlknon. This definition is also based on instead of , with (see clwwlk0on0). clwwlknon1le1 states that there is at most one (closed) walk of length on a vertex, which would consist of a loop (see clwwlknon1loop). And in a -regular graph, there are closed walks of length on each vertex, see clwwlknon2num.

  1. Closed walks as words
    1. cclwwlk
    2. df-clwwlk
    3. clwwlk
    4. isclwwlk
    5. clwwlkbp
    6. clwwlkgt0
    7. clwwlksswrd
    8. clwwlk1loop
    9. clwwlkccatlem
    10. clwwlkccat
    11. umgrclwwlkge2
    12. clwlkclwwlklem2a1
    13. clwlkclwwlklem2a2
    14. clwlkclwwlklem2a3
    15. clwlkclwwlklem2fv1
    16. clwlkclwwlklem2fv2
    17. clwlkclwwlklem2a4
    18. clwlkclwwlklem2a
    19. clwlkclwwlklem1
    20. clwlkclwwlklem2
    21. clwlkclwwlklem3
    22. clwlkclwwlk
    23. clwlkclwwlk2
    24. clwlkclwwlkflem
    25. clwlkclwwlkf1lem2
    26. clwlkclwwlkf1lem3
    27. clwlkclwwlkfolem
    28. clwlkclwwlkf
    29. clwlkclwwlkfo
    30. clwlkclwwlkf1
    31. clwlkclwwlkf1o
    32. clwlkclwwlken
    33. clwwisshclwwslemlem
    34. clwwisshclwwslem
    35. clwwisshclwws
    36. clwwisshclwwsn
    37. erclwwlkrel
    38. erclwwlkeq
    39. erclwwlkeqlen
    40. erclwwlkref
    41. erclwwlksym
    42. erclwwlktr
    43. erclwwlk
  2. Closed walks of a fixed length as words
    1. cclwwlkn
    2. df-clwwlkn
    3. clwwlkn
    4. isclwwlkn
    5. clwwlkn0
    6. clwwlkneq0
    7. clwwlkclwwlkn
    8. clwwlksclwwlkn
    9. clwwlknlen
    10. clwwlknnn
    11. clwwlknwrd
    12. clwwlknbp
    13. isclwwlknx
    14. clwwlknp
    15. clwwlknwwlksn
    16. clwwlknlbonbgr1
    17. clwwlkinwwlk
    18. clwwlkn1
    19. loopclwwlkn1b
    20. clwwlkn1loopb
    21. clwwlkn2
    22. clwwlknfi
    23. clwwlkel
    24. clwwlkf
    25. clwwlkfv
    26. clwwlkf1
    27. clwwlkfo
    28. clwwlkf1o
    29. clwwlken
    30. clwwlknwwlkncl
    31. clwwlkwwlksb
    32. clwwlknwwlksnb
    33. clwwlkext2edg
    34. wwlksext2clwwlk
    35. wwlksubclwwlk
    36. clwwnisshclwwsn
    37. eleclclwwlknlem1
    38. eleclclwwlknlem2
    39. clwwlknscsh
    40. clwwlknccat
    41. umgr2cwwk2dif
    42. umgr2cwwkdifex
    43. erclwwlknrel
    44. erclwwlkneq
    45. erclwwlkneqlen
    46. erclwwlknref
    47. erclwwlknsym
    48. erclwwlkntr
    49. erclwwlkn
    50. qerclwwlknfi
    51. hashclwwlkn0
    52. eclclwwlkn1
    53. eleclclwwlkn
    54. hashecclwwlkn1
    55. umgrhashecclwwlk
    56. fusgrhashclwwlkn
    57. clwwlkndivn
    58. clwlknf1oclwwlknlem1
    59. clwlknf1oclwwlknlem2
    60. clwlknf1oclwwlknlem3
    61. clwlknf1oclwwlkn
    62. clwlkssizeeq
    63. clwlksndivn
  3. Closed walks on a vertex of a fixed length as words
    1. cclwwlknon
    2. df-clwwlknon
    3. clwwlknonmpo
    4. clwwlknon
    5. isclwwlknon
    6. clwwlk0on0
    7. clwwlknon0
    8. clwwlknonfin
    9. clwwlknonel
    10. clwwlknonccat
    11. clwwlknon1
    12. clwwlknon1loop
    13. clwwlknon1nloop
    14. clwwlknon1sn
    15. clwwlknon1le1
    16. clwwlknon2
    17. clwwlknon2x
    18. s2elclwwlknon2
    19. clwwlknon2num
    20. clwwlknonwwlknonb
    21. clwwlknonex2lem1
    22. clwwlknonex2lem2
    23. clwwlknonex2
    24. clwwlknonex2e
    25. clwwlknondisj
    26. clwwlknun
    27. clwwlkvbij