P. 268 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26701-26800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	usgrn2cycl 26701	In a simple graph there are no cycles with length 2 (consisting of two edges). (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 4-Feb-2021.)
|- ( ( G e. USGraph /\ F (Cycles ` G ) P ) -> ( # ` F ) =/= 2 )
Theorem	crctcshwlkn0lem1 26702	Lemma for crctcshwlkn0 26713. (Contributed by AV, 13-Mar-2021.)
|- ( ( A e. RR /\ B e. NN ) -> ( ( A - B ) + 1 ) <_ A )
Theorem	crctcshwlkn0lem2 26703*	Lemma for crctcshwlkn0 26713. (Contributed by AV, 12-Mar-2021.)
|- ( ph -> S e. ( 1..^ N ) )   &    |- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )   =>    |- ( ( ph /\ J e. ( 0 ... ( N - S ) ) ) -> ( Q ` J ) = ( P ` ( J + S ) ) )
Theorem	crctcshwlkn0lem3 26704*	Lemma for crctcshwlkn0 26713. (Contributed by AV, 12-Mar-2021.)
|- ( ph -> S e. ( 1..^ N ) )   &    |- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )   =>    |- ( ( ph /\ J e. ( ( ( N - S ) + 1 ) ... N ) ) -> ( Q ` J ) = ( P ` ( ( J + S ) - N ) ) )
Theorem	crctcshwlkn0lem4 26705*	Lemma for crctcshwlkn0 26713. (Contributed by AV, 12-Mar-2021.)
|- ( ph -> S e. ( 1..^ N ) )   &    |- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )   &    |- H = ( F cyclShift S )   &    |- N = ( # ` F )   &    |- ( ph -> F e. Word A )   &    |- ( ph -> A. i e. ( 0..^ N )if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) )   =>    |- ( ph -> A. j e. ( 0..^ ( N - S ) )if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )
Theorem	crctcshwlkn0lem5 26706*	Lemma for crctcshwlkn0 26713. (Contributed by AV, 12-Mar-2021.)
|- ( ph -> S e. ( 1..^ N ) )   &    |- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )   &    |- H = ( F cyclShift S )   &    |- N = ( # ` F )   &    |- ( ph -> F e. Word A )   &    |- ( ph -> A. i e. ( 0..^ N )if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) )   =>    |- ( ph -> A. j e. ( ( ( N - S ) + 1 )..^ N )if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )
Theorem	crctcshwlkn0lem6 26707*	Lemma for crctcshwlkn0 26713. (Contributed by AV, 12-Mar-2021.)
|- ( ph -> S e. ( 1..^ N ) )   &    |- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )   &    |- H = ( F cyclShift S )   &    |- N = ( # ` F )   &    |- ( ph -> F e. Word A )   &    |- ( ph -> A. i e. ( 0..^ N )if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) )   &    |- ( ph -> ( P ` N ) = ( P ` 0 ) )   =>    |- ( ( ph /\ J = ( N - S ) ) -> if- ( ( Q ` J ) = ( Q ` ( J + 1 ) ) , ( I ` ( H ` J ) ) = { ( Q ` J ) } , { ( Q ` J ) , ( Q ` ( J + 1 ) ) } C_ ( I ` ( H ` J ) ) ) )
Theorem	crctcshwlkn0lem7 26708*	Lemma for crctcshwlkn0 26713. (Contributed by AV, 12-Mar-2021.)
|- ( ph -> S e. ( 1..^ N ) )   &    |- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )   &    |- H = ( F cyclShift S )   &    |- N = ( # ` F )   &    |- ( ph -> F e. Word A )   &    |- ( ph -> A. i e. ( 0..^ N )if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) )   &    |- ( ph -> ( P ` N ) = ( P ` 0 ) )   =>    |- ( ph -> A. j e. ( 0..^ N )if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )
Theorem	crctcshlem1 26709	Lemma for crctcsh 26716. (Contributed by AV, 10-Mar-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Circuits ` G ) P )   &    |- N = ( # ` F )   =>    |- ( ph -> N e. NN0 )
Theorem	crctcshlem2 26710	Lemma for crctcsh 26716. (Contributed by AV, 10-Mar-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Circuits ` G ) P )   &    |- N = ( # ` F )   &    |- ( ph -> S e. ( 0..^ N ) )   &    |- H = ( F cyclShift S )   =>    |- ( ph -> ( # ` H ) = N )
Theorem	crctcshlem3 26711*	Lemma for crctcsh 26716. (Contributed by AV, 10-Mar-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Circuits ` G ) P )   &    |- N = ( # ` F )   &    |- ( ph -> S e. ( 0..^ N ) )   &    |- H = ( F cyclShift S )   &    |- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )   =>    |- ( ph -> ( G e. _V /\ H e. _V /\ Q e. _V ) )
Theorem	crctcshlem4 26712*	Lemma for crctcsh 26716. (Contributed by AV, 10-Mar-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Circuits ` G ) P )   &    |- N = ( # ` F )   &    |- ( ph -> S e. ( 0..^ N ) )   &    |- H = ( F cyclShift S )   &    |- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )   =>    |- ( ( ph /\ S = 0 ) -> ( H = F /\ Q = P ) )
Theorem	crctcshwlkn0 26713*	Cyclically shifting the indices of a circuit <. F , P >. results in a walk <. H , Q >.. (Contributed by AV, 10-Mar-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Circuits ` G ) P )   &    |- N = ( # ` F )   &    |- ( ph -> S e. ( 0..^ N ) )   &    |- H = ( F cyclShift S )   &    |- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )   =>    |- ( ( ph /\ S =/= 0 ) -> H (Walks ` G ) Q )
Theorem	crctcshwlk 26714*	Cyclically shifting the indices of a circuit <. F , P >. results in a walk <. H , Q >.. (Contributed by AV, 10-Mar-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Circuits ` G ) P )   &    |- N = ( # ` F )   &    |- ( ph -> S e. ( 0..^ N ) )   &    |- H = ( F cyclShift S )   &    |- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )   =>    |- ( ph -> H (Walks ` G ) Q )
Theorem	crctcshtrl 26715*	Cyclically shifting the indices of a circuit <. F , P >. results in a trail <. H , Q >.. (Contributed by AV, 14-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Circuits ` G ) P )   &    |- N = ( # ` F )   &    |- ( ph -> S e. ( 0..^ N ) )   &    |- H = ( F cyclShift S )   &    |- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )   =>    |- ( ph -> H (Trails ` G ) Q )
Theorem	crctcsh 26716*	Cyclically shifting the indices of a circuit <. F , P >. results in a circuit <. H , Q >.. (Contributed by AV, 10-Mar-2021.) (Proof shortened by AV, 31-Oct-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Circuits ` G ) P )   &    |- N = ( # ` F )   &    |- ( ph -> S e. ( 0..^ N ) )   &    |- H = ( F cyclShift S )   &    |- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )   =>    |- ( ph -> H (Circuits ` G ) Q )
16.3.7  Walks as words In general, a walk is an alternating sequence of vertices and edges, as defined in df-wlks 26495: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). 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 Word, see df-word 13299, is the appropriate way to define such a sequence (being finite and starting at index 0) of vertices. Therefore, it is used in definitions df-wwlks 26722 and df-wwlksn 26723, 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 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).
Syntax	cwwlks 26717	Extend class notation with walks (in a graph) as word over the set of vertices.
class WWalks
Syntax	cwwlksn 26718	Extend class notation with walks (in a graph) of a fixed length as word over the set of vertices.
class WWalksN
Syntax	cwwlksnon 26719	Extend class notation with walks between two vertices (in a graph) of a fixed length as word over the set of vertices.
class WWalksNOn
Syntax	cwwspthsn 26720	Extend class notation with simple paths (in a graph) of a fixed length as word over the set of vertices.
class WSPathsN
Syntax	cwwspthsnon 26721	Extend class notation with simple paths between two vertices (in a graph) of a fixed length as word over the set of vertices.
class WSPathsNOn
Definition	df-wwlks 26722*	Define the set of all walks (in an undirected graph) as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n-1) p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlks 26495. w = (/) has to be excluded because a walk always consists of at least one vertex, see wlkn0 26516. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)
|- WWalks = ( g e. _V |-> { w e. Word (Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) ) } )
Definition	df-wwlksn 26723*	Define the set of all walks (in an undirected graph) of a fixed length n as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlks 26495. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)
|- WWalksN = ( n e. NN0 , g e. _V |-> { w e. (WWalks ` g ) | ( # ` w ) = ( n + 1 ) } )
Definition	df-wwlksnon 26724*	Define the collection of walks of a fixed length with particular endpoints as word over the set of vertices. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 11-May-2021.)
|- WWalksNOn = ( n e. NN0 , g e. _V |-> ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { w e. ( n WWalksN g ) | ( ( w ` 0 ) = a /\ ( w ` n ) = b ) } ) )
Definition	df-wspthsn 26725*	Define the collection of simple paths of a fixed length as word over the set of vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.)
|- WSPathsN = ( n e. NN0 , g e. _V |-> { w e. ( n WWalksN g ) | E. f f (SPaths ` g ) w } )
Definition	df-wspthsnon 26726*	Define the collection of simple paths of a fixed length with particular endpoints as word over the set of vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.)
|- WSPathsNOn = ( n e. NN0 , g e. _V |-> ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { w e. ( a ( n WWalksNOn g ) b ) | E. f f ( a (SPathsOn ` g ) b ) w } ) )
Theorem	wwlks 26727*	The set of walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- (WWalks ` G ) = { w e. Word V | ( w =/= (/) /\ A. i e. ( 0..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E ) }
Theorem	iswwlks 26728*	A word over the set of vertices representing a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( W e. (WWalks ` G ) <-> ( W =/= (/) /\ W e. Word V /\ A. i e. ( 0..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
Theorem	wwlksn 26729*	The set of walks (in an undirected graph) of a fixed length as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)
|- ( N e. NN0 -> ( N WWalksN G ) = { w e. (WWalks ` G ) | ( # ` w ) = ( N + 1 ) } )
Theorem	iswwlksn 26730	A word over the set of vertices representing a walk of a fixed length (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)
|- ( N e. NN0 -> ( W e. ( N WWalksN G ) <-> ( W e. (WWalks ` G ) /\ ( # ` W ) = ( N + 1 ) ) ) )
Theorem	iswwlksnx 26731*	Properties of a word to represent a walk of a fixed length, definition of WWalks expanded. (Contributed by AV, 28-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( N e. NN0 -> ( W e. ( N WWalksN G ) <-> ( W e. Word V /\ A. i e. ( 0..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ ( # ` W ) = ( N + 1 ) ) ) )
Theorem	wwlkbp 26732	Basic properties of a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 9-Apr-2021.)
|- V = (Vtx ` G )   =>    |- ( W e. (WWalks ` G ) -> ( G e. _V /\ W e. Word V ) )
Theorem	wwlknbp 26733	Basic properties of a walk of a fixed length (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 16-Jul-2018.) (Revised by AV, 9-Apr-2021.) (Proof shortened by AV, 20-May-2021.)
|- V = (Vtx ` G )   =>    |- ( W e. ( N WWalksN G ) -> ( G e. _V /\ N e. NN0 /\ W e. Word V ) )
Theorem	wwlknp 26734*	Properties of a set being a walk of length n (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 9-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( W e. ( N WWalksN G ) -> ( W e. Word V /\ ( # ` W ) = ( N + 1 ) /\ A. i e. ( 0..^ N ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
Theorem	wspthsn 26735*	The set of simple paths of a fixed length as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.)
|- ( N WSPathsN G ) = { w e. ( N WWalksN G ) | E. f f (SPaths ` G ) w }
Theorem	iswspthn 26736*	An element of the set of simple paths of a fixed length as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.)
|- ( W e. ( N WSPathsN G ) <-> ( W e. ( N WWalksN G ) /\ E. f f (SPaths ` G ) W ) )
Theorem	wspthnp 26737*	Properties of a set being a simple path of a fixed length as word. (Contributed by AV, 18-May-2021.)
|- ( W e. ( N WSPathsN G ) -> ( ( N e. NN0 /\ G e. _V ) /\ W e. ( N WWalksN G ) /\ E. f f (SPaths ` G ) W ) )
Theorem	wwlksnon 26738*	The set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 11-May-2021.)
|- V = (Vtx ` G )   =>    |- ( ( N e. NN0 /\ G e. U ) -> ( N WWalksNOn G ) = ( a e. V , b e. V |-> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } ) )
Theorem	wspthsnon 26739*	The set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.)
|- V = (Vtx ` G )   =>    |- ( ( N e. NN0 /\ G e. U ) -> ( N WSPathsNOn G ) = ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a (SPathsOn ` G ) b ) w } ) )
Theorem	iswwlksnon 26740*	The set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 12-May-2021.)
|- V = (Vtx ` G )   =>    |- ( ( A e. V /\ B e. V ) -> ( A ( N WWalksNOn G ) B ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) } )
Theorem	iswspthsnon 26741*	The set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 12-May-2021.)
|- V = (Vtx ` G )   =>    |- ( ( A e. V /\ B e. V ) -> ( A ( N WSPathsNOn G ) B ) = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A (SPathsOn ` G ) B ) w } )
Theorem	wwlknon 26742	An element of the set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 12-May-2021.)
|- V = (Vtx ` G )   =>    |- ( ( A e. V /\ B e. V ) -> ( W e. ( A ( N WWalksNOn G ) B ) <-> ( W e. ( N WWalksN G ) /\ ( W ` 0 ) = A /\ ( W ` N ) = B ) ) )
Theorem	wspthnon 26743*	An element of the set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 12-May-2021.)
|- V = (Vtx ` G )   =>    |- ( ( A e. V /\ B e. V ) -> ( W e. ( A ( N WSPathsNOn G ) B ) <-> ( W e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A (SPathsOn ` G ) B ) W ) ) )
Theorem	wspthnonp 26744*	Properties of a set being a simple path of a fixed length between two vertices as word. (Contributed by AV, 14-May-2021.)
|- V = (Vtx ` G )   =>    |- ( W e. ( A ( N WSPathsNOn G ) B ) -> ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) /\ ( W e. ( A ( N WWalksNOn G ) B ) /\ E. f f ( A (SPathsOn ` G ) B ) W ) ) )
Theorem	wspthneq1eq2 26745	Two simple paths with identical sequences of vertices start and end at the same vertices. (Contributed by AV, 14-May-2021.)
|- ( ( P e. ( A ( N WSPathsNOn G ) B ) /\ P e. ( C ( N WSPathsNOn G ) D ) ) -> ( A = C /\ B = D ) )
Theorem	wwlksn0s 26746*	The set of all walks as words of length 0 is the set of all words of length 1 over the vertices. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 12-Apr-2021.)
|- ( 0 WWalksN G ) = { w e. Word (Vtx ` G ) | ( # ` w ) = 1 }
Theorem	wwlkssswrd 26747	Walks (represented by words) are words. (Contributed by Alexander van der Vekens, 17-Jul-2018.) (Revised by AV, 9-Apr-2021.)
|- V = (Vtx ` G )   =>    |- (WWalks ` G ) C_ Word V
Theorem	wwlksn0 26748*	A walk of length 0 is represented by a singleton word. (Contributed by Alexander van der Vekens, 20-Jul-2018.) (Revised by AV, 9-Apr-2021.) (Proof shortened by AV, 21-May-2021.)
|- V = (Vtx ` G )   =>    |- ( W e. ( 0 WWalksN G ) -> E. v e. V W = <" v "> )
Theorem	0enwwlksnge1 26749	In graphs without edges, there are no walks of length greater than 0. (Contributed by Alexander van der Vekens, 26-Jul-2018.) (Revised by AV, 7-May-2021.)
|- ( ( (Edg ` G ) = (/) /\ N e. NN ) -> ( N WWalksN G ) = (/) )
Theorem	wwlkswwlksn 26750	A walk of a fixed length as word is a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 17-Jul-2018.) (Revised by AV, 12-Apr-2021.)
|- ( W e. ( N WWalksN G ) -> W e. (WWalks ` G ) )
Theorem	wwlkssswwlksn 26751	The walks of a fixed length as words are walks (in an undirected graph) as words. (Contributed by Alexander van der Vekens, 17-Jul-2018.) (Revised by AV, 12-Apr-2021.)
|- ( N WWalksN G ) C_ (WWalks ` G )
Theorem	wwlknbp2 26752	Other basic properties of a set being a walk of length n (represented by a word). (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 12-Apr-2021.)
|- ( W e. ( N WWalksN G ) -> ( W e. Word (Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) )
Theorem	wlkiswwlks1 26753	The sequence of vertices in a walk is a walk as word in a pseudograph. (Contributed by Alexander van der Vekens, 20-Jul-2018.) (Revised by AV, 9-Apr-2021.)
|- ( G e. UPGraph -> ( F (Walks ` G ) P -> P e. (WWalks ` G ) ) )
Theorem	wlklnwwlkln1 26754	The sequence of vertices in a walk of length N is a walk as word of length N in a pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.)
|- ( G e. UPGraph -> ( ( F (Walks ` G ) P /\ ( # ` F ) = N ) -> P e. ( N WWalksN G ) ) )
Theorem	wlkiswwlks2lem1 26755*	Lemma 1 for wlkiswwlks2 26761. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )   =>    |- ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) )
Theorem	wlkiswwlks2lem2 26756*	Lemma 2 for wlkiswwlks2 26761. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )   =>    |- ( ( ( # ` P ) e. NN0 /\ I e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> ( F ` I ) = ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) )
Theorem	wlkiswwlks2lem3 26757*	Lemma 3 for wlkiswwlks2 26761. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )   =>    |- ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> P : ( 0 ... ( # ` F ) ) --> V )
Theorem	wlkiswwlks2lem4 26758*	Lemma 4 for wlkiswwlks2 26761. (Contributed by Alexander van der Vekens, 20-Jul-2018.) (Revised by AV, 10-Apr-2021.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> A. i e. ( 0..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
Theorem	wlkiswwlks2lem5 26759*	Lemma 5 for wlkiswwlks2 26761. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> F e. Word dom E ) )
Theorem	wlkiswwlks2lem6 26760*	Lemma 6 for wlkiswwlks2 26761. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )   &    |- E = (iEdg ` G )   =>    |- ( ( G e. USPGraph /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> ( F e. Word dom E /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
Theorem	wlkiswwlks2 26761*	A walk as word corresponds to the sequence of vertices in a walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.)
|- ( G e. USPGraph -> ( P e. (WWalks ` G ) -> E. f f (Walks ` G ) P ) )
Theorem	wlkiswwlks 26762*	A walk as word corresponds to a walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.)
|- ( G e. USPGraph -> ( E. f f (Walks ` G ) P <-> P e. (WWalks ` G ) ) )
Theorem	wlkiswwlksupgr2 26763*	A walk as word corresponds to the sequence of vertices in a walk in a pseudograph. This variant of wlkiswwlks2 26761 does not require G to be a simple pseudograph, but it requires the Axiom of Choice (ac6 9302) for its proof. Notice that only the existence of a function f can be proven, but, in general, it cannot be "constructed" (as in wlkiswwlks2 26761). (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.)
|- ( G e. UPGraph -> ( P e. (WWalks ` G ) -> E. f f (Walks ` G ) P ) )
Theorem	wlkiswwlkupgr 26764*	A walk as word corresponds to a walk in a pseudograph. This variant of wlkiswwlks 26762 does not require G to be a simple pseudograph, but it requires (indirectly) the Axiom of Choice for its proof. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.)
|- ( G e. UPGraph -> ( E. f f (Walks ` G ) P <-> P e. (WWalks ` G ) ) )
Theorem	wlkpwwlkf1ouspgr 26765*	The mapping of (ordinary) walks to their sequences of vertices is a bijection in a simple pseudograph. (Contributed by AV, 6-May-2021.)
|- F = ( w e. (Walks ` G ) |-> ( 2nd ` w ) )   =>    |- ( G e. USPGraph -> F : (Walks ` G ) -1-1-onto-> (WWalks ` G ) )
Theorem	wlkisowwlkupgr 26766*	The set of walks as words and the set of (ordinary) walks are isomorphic in a simple pseudograph. (Contributed by AV, 6-May-2021.)
|- ( G e. USPGraph -> E. f f : (Walks ` G ) -1-1-onto-> (WWalks ` G ) )
Theorem	wwlksm1edg 26767	Removing the trailing edge from a walk (as word) with at least one edge results in a walk. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 19-Apr-2021.)
|- ( ( W e. (WWalks ` G ) /\ 2 <_ ( # ` W ) ) -> ( W substr <. 0 , ( ( # ` W ) - 1 ) >. ) e. (WWalks ` G ) )
Theorem	wlklnwwlkln2lem 26768*	Lemma for wlklnwwlkln2 26769 and wlklnwwlklnupgr2 26771. Formerly part of proof for wlklnwwlkln2 26769. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.)
|- ( ph -> ( P e. (WWalks ` G ) -> E. f f (Walks ` G ) P ) )   =>    |- ( ph -> ( P e. ( N WWalksN G ) -> E. f ( f (Walks ` G ) P /\ ( # ` f ) = N ) ) )
Theorem	wlklnwwlkln2 26769*	A walk of length N as word corresponds to the sequence of vertices in a walk of length N in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.)
|- ( G e. USPGraph -> ( P e. ( N WWalksN G ) -> E. f ( f (Walks ` G ) P /\ ( # ` f ) = N ) ) )
Theorem	wlklnwwlkn 26770*	A walk of length N as word corresponds to a walk with length N in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.)
|- ( G e. USPGraph -> ( E. f ( f (Walks ` G ) P /\ ( # ` f ) = N ) <-> P e. ( N WWalksN G ) ) )
Theorem	wlklnwwlklnupgr2 26771*	A walk of length N as word corresponds to the sequence of vertices in a walk of length N in a pseudograph. This variant of wlklnwwlkln2 26769 does not require G to be a simple pseudograph, but it requires (indirectly) the Axiom of Choice. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.)
|- ( G e. UPGraph -> ( P e. ( N WWalksN G ) -> E. f ( f (Walks ` G ) P /\ ( # ` f ) = N ) ) )
Theorem	wlklnwwlknupgr 26772*	A walk of length N as word corresponds to a walk with length N in a pseudograph. This variant of wlkiswwlks 40197 does not require G to be a simple pseudograph, but it requires (indirectly) the Axiom of Choice for its proof. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.)
|- ( G e. UPGraph -> ( E. f ( f (Walks ` G ) P /\ ( # ` f ) = N ) <-> P e. ( N WWalksN G ) ) )
Theorem	wlknewwlksn 26773	If a walk in a pseudograph has length N, then the sequence of the vertices of the walk is a word representing the walk as word of length N. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 11-Apr-2021.)
|- ( ( ( G e. UPGraph /\ W e. (Walks ` G ) ) /\ ( N e. NN0 /\ ( # ` ( 1st ` W ) ) = N ) ) -> ( 2nd ` W ) e. ( N WWalksN G ) )
Theorem	wlknwwlksnfun 26774*	Lemma 1 for wlknwwlksnbij2 26778. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 14-Apr-2021.)
|- T = { p e. (Walks ` G ) | ( # ` ( 1st ` p ) ) = N }   &    |- W = ( N WWalksN G )   &    |- F = ( t e. T |-> ( 2nd ` t ) )   =>    |- ( ( G e. UPGraph /\ N e. NN0 ) -> F : T --> W )
Theorem	wlknwwlksninj 26775*	Lemma 2 for wlknwwlksnbij2 26778. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 14-Apr-2021.)
|- T = { p e. (Walks ` G ) | ( # ` ( 1st ` p ) ) = N }   &    |- W = ( N WWalksN G )   &    |- F = ( t e. T |-> ( 2nd ` t ) )   =>    |- ( ( G e. USPGraph /\ N e. NN0 ) -> F : T -1-1-> W )
Theorem	wlknwwlksnsur 26776*	Lemma 3 for wlknwwlksnbij2 26778. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 14-Apr-2021.)
|- T = { p e. (Walks ` G ) | ( # ` ( 1st ` p ) ) = N }   &    |- W = ( N WWalksN G )   &    |- F = ( t e. T |-> ( 2nd ` t ) )   =>    |- ( ( G e. USPGraph /\ N e. NN0 ) -> F : T -onto-> W )
Theorem	wlknwwlksnbij 26777*	Lemma 4 for wlknwwlksnbij2 26778. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 14-Apr-2021.)
|- T = { p e. (Walks ` G ) | ( # ` ( 1st ` p ) ) = N }   &    |- W = ( N WWalksN G )   &    |- F = ( t e. T |-> ( 2nd ` t ) )   =>    |- ( ( G e. USPGraph /\ N e. NN0 ) -> F : T -1-1-onto-> W )
Theorem	wlknwwlksnbij2 26778*	There is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length in a simple pseudograph. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 15-Apr-2021.)
|- ( ( G e. USPGraph /\ N e. NN0 ) -> E. f f : { p e. (Walks ` G ) | ( # ` ( 1st ` p ) ) = N } -1-1-onto-> ( N WWalksN G ) )
Theorem	wlknwwlksnen 26779*	In a simple pseudograph, the set of walks of a fixed length and the set of walks represented by words are equinumerous. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 15-Apr-2021.)
|- ( ( G e. USPGraph /\ N e. NN0 ) -> { p e. (Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ~~ ( N WWalksN G ) )
Theorem	wlknwwlksneqs 26780*	The set of walks of a fixed length and the set of walks represented by words have the same size. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 15-Apr-2021.)
|- ( ( G e. USPGraph /\ N e. NN0 ) -> ( # ` { p e. (Walks ` G ) | ( # ` ( 1st ` p ) ) = N } ) = ( # ` ( N WWalksN G ) ) )
Theorem	wlkwwlkfun 26781*	Lemma 1 for wlkwwlkbij2 26785. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Proof shortened by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 15-Apr-2021.)
|- T = { p e. (Walks ` G ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = P ) }   &    |- W = { w e. ( N WWalksN G ) | ( w ` 0 ) = P }   &    |- F = ( t e. T |-> ( 2nd ` t ) )   =>    |- ( ( G e. UPGraph /\ P e. V /\ N e. NN0 ) -> F : T --> W )
Theorem	wlkwwlkinj 26782*	Lemma 2 for wlkwwlkbij2 26785. (Contributed by Alexander van der Vekens, 23-Jul-2018.) (Proof shortened by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 16-Apr-2021.)
|- T = { p e. (Walks ` G ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = P ) }   &    |- W = { w e. ( N WWalksN G ) | ( w ` 0 ) = P }   &    |- F = ( t e. T |-> ( 2nd ` t ) )   =>    |- ( ( G e. USPGraph /\ P e. V /\ N e. NN0 ) -> F : T -1-1-> W )
Theorem	wlkwwlksur 26783*	Lemma 3 for wlkwwlkbij2 26785. (Contributed by Alexander van der Vekens, 23-Jul-2018.) (Revised by AV, 16-Apr-2021.)
|- T = { p e. (Walks ` G ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = P ) }   &    |- W = { w e. ( N WWalksN G ) | ( w ` 0 ) = P }   &    |- F = ( t e. T |-> ( 2nd ` t ) )   =>    |- ( ( G e. USPGraph /\ P e. V /\ N e. NN0 ) -> F : T -onto-> W )
Theorem	wlkwwlkbij 26784*	Lemma 4 for wlkwwlkbij2 26785. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 16-Apr-2021.)
|- T = { p e. (Walks ` G ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = P ) }   &    |- W = { w e. ( N WWalksN G ) | ( w ` 0 ) = P }   &    |- F = ( t e. T |-> ( 2nd ` t ) )   =>    |- ( ( G e. USPGraph /\ P e. V /\ N e. NN0 ) -> F : T -1-1-onto-> W )
Theorem	wlkwwlkbij2 26785*	There is a bijection between the set of walks of a fixed length, starting at a fixed vertex, and the set of walks represented as words of the same length, starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 16-Apr-2021.)
|- ( ( G e. USPGraph /\ P e. V /\ N e. NN0 ) -> E. f f : { p e. (Walks ` G ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = P ) } -1-1-onto-> { w e. ( N WWalksN G ) | ( w ` 0 ) = P } )
Theorem	wwlkseq 26786*	Equality of two walks (as words). (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.)
|- ( ( W e. (WWalks ` G ) /\ T e. (WWalks ` G ) ) -> ( W = T <-> ( ( # ` W ) = ( # ` T ) /\ A. i e. ( 0..^ ( # ` W ) ) ( W ` i ) = ( T ` i ) ) ) )
Theorem	wwlksnred 26787	Reduction of a walk (as word) by removing the trailing edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.)
|- ( N e. NN0 -> ( W e. ( ( N + 1 ) WWalksN G ) -> ( W substr <. 0 , ( N + 1 ) >. ) e. ( N WWalksN G ) ) )
Theorem	wwlksnext 26788	Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( T e. ( N WWalksN G ) /\ S e. V /\ { ( lastS ` T ) , S } e. E ) -> ( T ++ <" S "> ) e. ( ( N + 1 ) WWalksN G ) )
Theorem	wwlksnextbi 26789	Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by AV, 16-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ W = ( T ++ <" S "> ) /\ { ( lastS ` T ) , S } e. E ) ) -> ( W e. ( ( N + 1 ) WWalksN G ) <-> T e. ( N WWalksN G ) ) )
Theorem	wwlksnredwwlkn 26790*	For each walk (as word) of length at least 1 there is a shorter walk (as word). (Contributed by Alexander van der Vekens, 22-Aug-2018.) (Revised by AV, 18-Apr-2021.)
|- E = (Edg ` G )   =>    |- ( N e. NN0 -> ( W e. ( ( N + 1 ) WWalksN G ) -> E. y e. ( N WWalksN G ) ( ( W substr <. 0 , ( N + 1 ) >. ) = y /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) )
Theorem	wwlksnredwwlkn0 26791*	For each walk (as word) of length at least 1 there is a shorter walk (as word) starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Aug-2018.) (Revised by AV, 18-Apr-2021.)
|- E = (Edg ` G )   =>    |- ( ( N e. NN0 /\ W e. ( ( N + 1 ) WWalksN G ) ) -> ( ( W ` 0 ) = P <-> E. y e. ( N WWalksN G ) ( ( W substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` W ) } e. E ) ) )
Theorem	wwlksnextwrd 26792*	Lemma for wwlksnextbij 26797. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by AV, 18-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- D = { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w substr <. 0 , ( N + 1 ) >. ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) }   =>    |- ( W e. ( N WWalksN G ) -> D = { w e. ( ( N + 1 ) WWalksN G ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } )
Theorem	wwlksnextfun 26793*	Lemma for wwlksnextbij 26797. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- D = { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w substr <. 0 , ( N + 1 ) >. ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) }   &    |- R = { n e. V | { ( lastS ` W ) , n } e. E }   &    |- F = ( t e. D |-> ( lastS ` t ) )   =>    |- ( N e. NN0 -> F : D --> R )
Theorem	wwlksnextinj 26794*	Lemma for wwlksnextbij 26797. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- D = { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w substr <. 0 , ( N + 1 ) >. ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) }   &    |- R = { n e. V | { ( lastS ` W ) , n } e. E }   &    |- F = ( t e. D |-> ( lastS ` t ) )   =>    |- ( N e. NN0 -> F : D -1-1-> R )
Theorem	wwlksnextsur 26795*	Lemma for wwlksnextbij 26797. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- D = { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w substr <. 0 , ( N + 1 ) >. ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) }   &    |- R = { n e. V | { ( lastS ` W ) , n } e. E }   &    |- F = ( t e. D |-> ( lastS ` t ) )   =>    |- ( W e. ( N WWalksN G ) -> F : D -onto-> R )
Theorem	wwlksnextbij0 26796*	Lemma for wwlksnextbij 26797. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- D = { w e. Word V | ( ( # ` w ) = ( N + 2 ) /\ ( w substr <. 0 , ( N + 1 ) >. ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) }   &    |- R = { n e. V | { ( lastS ` W ) , n } e. E }   &    |- F = ( t e. D |-> ( lastS ` t ) )   =>    |- ( W e. ( N WWalksN G ) -> F : D -1-1-onto-> R )
Theorem	wwlksnextbij 26797*	There is a bijection between the extensions of a walk (as word) by an edge and the set of vertices being connected to the trailing vertex of the walk. (Contributed by Alexander van der Vekens, 21-Aug-2018.) (Revised by AV, 18-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( W e. ( N WWalksN G ) -> E. f f : { w e. ( ( N + 1 ) WWalksN G ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } -1-1-onto-> { n e. V | { ( lastS ` W ) , n } e. E } )
Theorem	wwlksnexthasheq 26798*	The number of the extensions of a walk (as word) by an edge equals the number of vertices being connected to the trailing vertex of the walk. (Contributed by Alexander van der Vekens, 23-Aug-2018.) (Revised by AV, 19-Apr-2021.) (Proof shortened by AV, 5-May-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( W e. ( N WWalksN G ) -> ( # ` { w e. ( ( N + 1 ) WWalksN G ) | ( ( w substr <. 0 , ( N + 1 ) >. ) = W /\ { ( lastS ` W ) , ( lastS ` w ) } e. E ) } ) = ( # ` { n e. V | { ( lastS ` W ) , n } e. E } ) )
Theorem	disjxwwlksn 26799*	Sets of walks (as words) extended by an edge are disjunct if each set contains extensions of distinct walks. (Contributed by Alexander van der Vekens, 29-Jul-2018.) (Revised by AV, 19-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- Disj y e. ( N WWalksN G ) { x e. Word V | ( ( x substr <. 0 , N >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. E ) }
Theorem	wwlksnndef 26800	Conditions for WWalksN not being defined. (Contributed by Alexander van der Vekens, 30-Jul-2018.) (Revised by AV, 19-Apr-2021.)
|- ( ( G e/ _V \/ N e/ NN0 ) -> ( N WWalksN G ) = (/) )