P. 167 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16601-16700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	upgriswlkdc 16601*	Properties of a pair of functions to be a walk in a pseudograph. (Contributed by AV, 2-Jan-2021.) (Revised by AV, 28-Oct-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( G e. UPGraph -> ( F (Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... (♯ ` F ) ) --> V /\ A. k e. ( 0..^ (♯ ` F ) ) (DECID ( P ` k ) = ( P ` ( k + 1 ) ) /\ ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) ) )
Theorem	upgrwlkedg 16602*	The edges of a walk in a pseudograph join exactly the two corresponding adjacent vertices in the walk. (Contributed by AV, 27-Feb-2021.)
|- I = (iEdg ` G )   =>    |- ( ( G e. UPGraph /\ F (Walks ` G ) P ) -> A. k e. ( 0..^ (♯ ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
Theorem	upgrwlkcompim 16603*	Implications for the properties of the components of a walk in a pseudograph. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 14-Apr-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- F = ( 1st ` W )   &    |- P = ( 2nd ` W )   =>    |- ( ( G e. UPGraph /\ W e. (Walks ` G ) ) -> ( F e. Word dom I /\ P : ( 0 ... (♯ ` F ) ) --> V /\ A. k e. ( 0..^ (♯ ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
Theorem	wlkvtxedg 16604*	The vertices of a walk are connected by edges. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.)
|- E = (Edg ` G )   =>    |- ( F (Walks ` G ) P -> A. k e. ( 0..^ (♯ ` F ) ) E. e e. E { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e )
Theorem	upgrwlkvtxedg 16605*	The pairs of connected vertices of a walk are edges in a pseudograph. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.)
|- E = (Edg ` G )   =>    |- ( ( G e. UPGraph /\ F (Walks ` G ) P ) -> A. k e. ( 0..^ (♯ ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } e. E )
Theorem	uspgr2wlkeq 16606*	Conditions for two walks within the same simple pseudograph being the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 3-Jul-2018.) (Revised by AV, 14-Apr-2021.)
|- ( ( G e. USPGraph /\ ( A e. (Walks ` G ) /\ B e. (Walks ` G ) ) /\ N = (♯ ` ( 1st ` A ) ) ) -> ( A = B <-> ( N = (♯ ` ( 1st ` B ) ) /\ A. y e. ( 0 ... N ) ( ( 2nd ` A ) ` y ) = ( ( 2nd ` B ) ` y ) ) ) )
Theorem	uspgr2wlkeq2 16607	Conditions for two walks within the same simple pseudograph to be identical. It is sufficient that the vertices (in the same order) are identical. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 14-Apr-2021.)
|- ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. (Walks ` G ) /\ (♯ ` ( 1st ` A ) ) = N ) /\ ( B e. (Walks ` G ) /\ (♯ ` ( 1st ` B ) ) = N ) ) -> ( ( 2nd ` A ) = ( 2nd ` B ) -> A = B ) )
Theorem	uspgr2wlkeqi 16608	Conditions for two walks within the same simple pseudograph to be identical. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 6-May-2021.)
|- ( ( G e. USPGraph /\ ( A e. (Walks ` G ) /\ B e. (Walks ` G ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> A = B )
Theorem	umgrwlknloop 16609*	In a multigraph, each walk has no loops! (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 3-Jan-2021.)
|- ( ( G e. UMGraph /\ F (Walks ` G ) P ) -> A. k e. ( 0..^ (♯ ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
Theorem	wlkv0 16610	If there is a walk in the null graph (a class without vertices), it would be the pair consisting of empty sets. (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.)
|- ( ( (Vtx ` G ) = (/) /\ W e. (Walks ` G ) ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) )
Theorem	g0wlk0 16611	There is no walk in a null graph (a class without vertices). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.)
|- ( (Vtx ` G ) = (/) -> (Walks ` G ) = (/) )
Theorem	0wlk0 16612	There is no walk for the empty set, i.e. in a null graph. (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.)
|- (Walks ` (/) ) = (/)
Theorem	wlk0prc 16613	There is no walk in a null graph (a class without vertices). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.)
|- ( ( S e/ _V /\ (Vtx ` S ) = (Vtx ` G ) ) -> (Walks ` G ) = (/) )
Theorem	wlklenvclwlk 16614	The number of vertices in a walk equals the length of the walk after it is "closed" (i.e. enhanced by an edge from its last vertex to its first vertex). (Contributed by Alexander van der Vekens, 29-Jun-2018.) (Revised by AV, 2-May-2021.) (Revised by JJ, 14-Jan-2024.)
|- ( W e. Word (Vtx ` G ) -> ( <. F , ( W ++ <" ( W ` 0 ) "> ) >. e. (Walks ` G ) -> (♯ ` F ) = (♯ ` W ) ) )
Theorem	wlkpvtx 16615	A walk connects vertices. (Contributed by AV, 22-Feb-2021.)
|- V = (Vtx ` G )   =>    |- ( F (Walks ` G ) P -> ( N e. ( 0 ... (♯ ` F ) ) -> ( P ` N ) e. V ) )
Theorem	wlkepvtx 16616	The endpoints of a walk are vertices. (Contributed by AV, 31-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( F (Walks ` G ) P -> ( ( P ` 0 ) e. V /\ ( P ` (♯ ` F ) ) e. V ) )
Theorem	2wlklem 16617*	Lemma for theorems for walks of length 2. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
|- ( A. k e. { 0 , 1 } ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( ( E ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( E ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
Theorem	upgr2wlkdc 16618*	Properties of a pair of functions to be a walk of length 2 in a pseudograph. Note that the vertices need not to be distinct and the edges can be loops or multiedges. (Contributed by Alexander van der Vekens, 16-Feb-2018.) (Revised by AV, 3-Jan-2021.) (Revised by AV, 28-Oct-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( G e. UPGraph -> ( ( F (Walks ` G ) P /\ F ~~ 2o ) <-> ( ( F : ( 0..^ 2 ) --> dom I /\ P : ( 0 ... 2 ) --> V /\ A. k e. { 0 , 1 }DECID ( P ` k ) = ( P ` ( k + 1 ) ) ) /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) )
Theorem	wlkreslem 16619	Lemma for wlkres 16620. (Contributed by AV, 5-Mar-2021.) (Revised by AV, 30-Nov-2022.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Walks ` G ) P )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> (Vtx ` S ) = V )   =>    |- ( ph -> S e. _V )
Theorem	wlkres 16620	The restriction <. H , Q >. of a walk <. F , P >. to an initial segment of the walk (of length N) forms a walk on the subgraph S consisting of the edges in the initial segment. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 5-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Walks ` G ) P )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> (Vtx ` S ) = V )   &    |- ( ph -> (iEdg ` S ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- H = ( F prefix N )   &    |- Q = ( P |` ( 0 ... N ) )   =>    |- ( ph -> H (Walks ` S ) Q )
12.3.2  Trails
Syntax	ctrls 16621	Extend class notation with trails (within a graph).
class Trails
Definition	df-trls 16622*	Define the set of all Trails (in an undirected graph). According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A trail is a walk in which all edges are distinct. According to Bollobas: "... walk is called a trail if all its edges are distinct.", see Definition of [Bollobas] p. 5. Therefore, a trail can be represented by an injective mapping f from { 1 , ... , n } and a mapping p from { 0 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the trail is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.)
|- Trails = ( g e. _V |-> { <. f , p >. | ( f (Walks ` g ) p /\ Fun `' f ) } )
Theorem	reltrls 16623	The set (Trails ` G ) of all trails on G is a set of pairs by our definition of a trail, and so is a relation. (Contributed by AV, 29-Oct-2021.)
|- Rel (Trails ` G )
Theorem	trlsfvalg 16624*	The set of trails (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Revised by AV, 29-Oct-2021.)
|- ( G e. V -> (Trails ` G ) = { <. f , p >. | ( f (Walks ` G ) p /\ Fun `' f ) } )
Theorem	trlsv 16625	The classes involved in a trail are sets. (Contributed by Jim Kingdon, 7-Feb-2026.)
|- ( F (Trails ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
Theorem	istrl 16626	Conditions for a pair of classes/functions to be a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Revised by AV, 29-Oct-2021.)
|- ( F (Trails ` G ) P <-> ( F (Walks ` G ) P /\ Fun `' F ) )
Theorem	trliswlk 16627	A trail is a walk. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 29-Oct-2021.)
|- ( F (Trails ` G ) P -> F (Walks ` G ) P )
Theorem	trlsex 16628	The class of trails on a graph is a set. (Contributed by Jim Kingdon, 14-Mar-2026.)
|- ( G e. V -> (Trails ` G ) e. _V )
Theorem	trlf1 16629	The enumeration F of a trail <. F , P >. is injective. (Contributed by AV, 20-Feb-2021.) (Proof shortened by AV, 29-Oct-2021.)
|- I = (iEdg ` G )   =>    |- ( F (Trails ` G ) P -> F : ( 0..^ (♯ ` F ) ) -1-1-> dom I )
Theorem	trlreslem 16630	Lemma for trlres 16631. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 6-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- H = ( F prefix N )   =>    |- ( ph -> H : ( 0..^ (♯ ` H ) ) -1-1-onto-> dom ( I |` ( F " ( 0..^ N ) ) ) )
Theorem	trlres 16631	The restriction <. H , Q >. of a trail <. F , P >. to an initial segment of the trail (of length N) forms a trail on the subgraph S consisting of the edges in the initial segment. (Contributed by AV, 6-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- H = ( F prefix N )   &    |- ( ph -> (Vtx ` S ) = V )   &    |- ( ph -> (iEdg ` S ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- Q = ( P |` ( 0 ... N ) )   =>    |- ( ph -> H (Trails ` S ) Q )
12.3.3  Closed walks as words
12.3.3.1  Closed walks as words
Syntax	cclwwlk 16632	Extend class notation with closed walks (in an undirected graph) as word over the set of vertices.
class ClWWalks
Definition	df-clwwlk 16633*	Define the set of all closed 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) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined elsewhere. Notice that the word does not contain the terminating vertex p(n) of the walk, because it is always equal to the first vertex of the closed walk. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.)
|- ClWWalks = ( g e. _V |-> { w e. Word (Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) /\ { (lastS ` w ) , ( w ` 0 ) } e. (Edg ` g ) ) } )
Theorem	clwwlkg 16634*	The set of closed walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. W -> (ClWWalks ` G ) = { w e. Word V | ( w =/= (/) /\ A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { (lastS ` w ) , ( w ` 0 ) } e. E ) } )
Theorem	isclwwlk 16635*	Properties of a word to represent a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( W e. (ClWWalks ` G ) <-> ( ( W e. Word V /\ W =/= (/) ) /\ A. i e. ( 0..^ ( (♯ ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { (lastS ` W ) , ( W ` 0 ) } e. E ) )
Theorem	clwwlkbp 16636	Basic properties of a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.)
|- V = (Vtx ` G )   =>    |- ( W e. (ClWWalks ` G ) -> ( G e. _V /\ W e. Word V /\ W =/= (/) ) )
Theorem	clwwlkgt0 16637	There is no empty closed walk (i.e. a closed walk without any edge) represented by a word of vertices. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 24-Apr-2021.)
|- ( W e. (ClWWalks ` G ) -> 0 < (♯ ` W ) )
Theorem	clwwlksswrd 16638	Closed walks (represented by words) are words. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 25-Apr-2021.)
|- (ClWWalks ` G ) C_ Word (Vtx ` G )
Theorem	clwwlkex 16639	Existence of the set of closed walks (represented by words). (Contributed by Jim Kingdon, 21-Feb-2026.)
|- ( G e. V -> (ClWWalks ` G ) e. _V )
Theorem	clwwlk1loop 16640	A closed walk of length 1 is a loop. (Contributed by AV, 24-Apr-2021.)
|- ( ( W e. (ClWWalks ` G ) /\ (♯ ` W ) = 1 ) -> { ( W ` 0 ) , ( W ` 0 ) } e. (Edg ` G ) )
Theorem	clwwlkccatlem 16641*	Lemma for clwwlkccat 16642: index j is shifted up by (♯ ` A ), and the case i = ( (♯ ` A ) - 1 ) is covered by the "bridge" { (lastS ` A ) , ( B ` 0 ) } = { (lastS ` A ) , ( A ` 0 ) } e. (Edg ` G ). (Contributed by AV, 23-Apr-2022.)
|- ( ( ( ( A e. Word (Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0..^ ( (♯ ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. (Edg ` G ) /\ { (lastS ` A ) , ( A ` 0 ) } e. (Edg ` G ) ) /\ ( ( B e. Word (Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0..^ ( (♯ ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. (Edg ` G ) /\ { (lastS ` B ) , ( B ` 0 ) } e. (Edg ` G ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> A. i e. ( 0..^ ( (♯ ` ( A ++ B ) ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. (Edg ` G ) )
Theorem	clwwlkccat 16642	The concatenation of two words representing closed walks anchored at the same vertex represents a closed walk. The resulting walk is a "double loop", starting at the common vertex, coming back to the common vertex by the first walk, following the second walk and finally coming back to the common vertex again. (Contributed by AV, 23-Apr-2022.)
|- ( ( A e. (ClWWalks ` G ) /\ B e. (ClWWalks ` G ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A ++ B ) e. (ClWWalks ` G ) )
Theorem	umgrclwwlkge2 16643	A closed walk in a multigraph has a length of at least 2 (because it cannot have a loop). (Contributed by Alexander van der Vekens, 16-Sep-2018.) (Revised by AV, 24-Apr-2021.)
|- ( G e. UMGraph -> ( P e. (ClWWalks ` G ) -> 2 <_ (♯ ` P ) ) )
12.3.3.2  Closed walks of a fixed length as words
Syntax	cclwwlkn 16644	Extend class notation with closed walks (in an undirected graph) of a fixed length as word over the set of vertices.
class ClWWalksN
Definition	df-clwwlkn 16645*	Define the set of all closed walks of a fixed length n as words over the set of vertices in a graph g. If 0 < n, such a word corresponds to the sequence p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) . For n = 0, the set is empty, see clwwlkn0 16649. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.)
|- ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )
Theorem	clwwlkng 16646*	The set of closed walks of a fixed length N as words over the set of vertices in a graph G. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.)
|- ( ( N e. NN0 /\ G e. V ) -> ( N ClWWalksN G ) = { w e. (ClWWalks ` G ) | (♯ ` w ) = N } )
Theorem	isclwwlkng 16647	A word over the set of vertices representing a closed walk of a fixed length. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.)
|- ( N e. NN0 -> ( W e. ( N ClWWalksN G ) <-> ( W e. (ClWWalks ` G ) /\ (♯ ` W ) = N ) ) )
Theorem	isclwwlkni 16648	A word over the set of vertices representing a closed walk of a fixed length. (Contributed by Jim Kingdon, 22-Feb-2026.)
|- ( W e. ( N ClWWalksN G ) -> ( W e. (ClWWalks ` G ) /\ (♯ ` W ) = N ) )
Theorem	clwwlkn0 16649	There is no closed walk of length 0 (i.e. a closed walk without any edge) represented by a word of vertices. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 24-Apr-2021.)
|- ( 0 ClWWalksN G ) = (/)
Theorem	clwwlkclwwlkn 16650	A closed walk of a fixed length as word is a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.)
|- ( W e. ( N ClWWalksN G ) -> W e. (ClWWalks ` G ) )
Theorem	clwwlksclwwlkn 16651	The closed walks of a fixed length as words are closed walks (in an undirected graph) as words. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 12-Apr-2021.)
|- ( N ClWWalksN G ) C_ (ClWWalks ` G )
Theorem	clwwlknlen 16652	The length of a word representing a closed walk of a fixed length is this fixed length. (Contributed by AV, 22-Mar-2022.)
|- ( W e. ( N ClWWalksN G ) -> (♯ ` W ) = N )
Theorem	clwwlknnn 16653	The length of a closed walk of a fixed length as word is a positive integer. (Contributed by AV, 22-Mar-2022.)
|- ( W e. ( N ClWWalksN G ) -> N e. NN )
Theorem	isclwwlkn 16654	A word over the set of vertices representing a closed walk of a fixed length. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.)
|- ( W e. ( N ClWWalksN G ) <-> ( W e. (ClWWalks ` G ) /\ (♯ ` W ) = N ) )
Theorem	clwwlknwrd 16655	A closed walk of a fixed length as word is a word over the vertices. (Contributed by AV, 30-Apr-2021.)
|- V = (Vtx ` G )   =>    |- ( W e. ( N ClWWalksN G ) -> W e. Word V )
Theorem	clwwlknbp 16656	Basic properties of a closed walk of a fixed length as word. (Contributed by AV, 30-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.)
|- V = (Vtx ` G )   =>    |- ( W e. ( N ClWWalksN G ) -> ( W e. Word V /\ (♯ ` W ) = N ) )
Theorem	isclwwlknx 16657*	Characterization of a word representing a closed walk of a fixed length, definition of ClWWalks expanded. (Contributed by AV, 25-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( N e. NN -> ( W e. ( N ClWWalksN G ) <-> ( ( W e. Word V /\ A. i e. ( 0..^ ( (♯ ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { (lastS ` W ) , ( W ` 0 ) } e. E ) /\ (♯ ` W ) = N ) ) )
Theorem	clwwlknp 16658*	Properties of a set being a closed walk (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 24-Apr-2021.) (Proof shortened by AV, 23-Mar-2022.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( W e. ( N ClWWalksN G ) -> ( ( W e. Word V /\ (♯ ` W ) = N ) /\ A. i e. ( 0..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { (lastS ` W ) , ( W ` 0 ) } e. E ) )
Theorem	clwwlkn1 16659	A closed walk of length 1 represented as word is a word consisting of 1 symbol representing a vertex connected to itself by (at least) one edge, that is, a loop. (Contributed by AV, 24-Apr-2021.) (Revised by AV, 11-Feb-2022.)
|- ( W e. ( 1 ClWWalksN G ) <-> ( (♯ ` W ) = 1 /\ W e. Word (Vtx ` G ) /\ { ( W ` 0 ) } e. (Edg ` G ) ) )
Theorem	loopclwwlkn1b 16660	The singleton word consisting of a vertex V represents a closed walk of length 1 iff there is a loop at vertex V. (Contributed by AV, 11-Feb-2022.)
|- ( V e. (Vtx ` G ) -> ( { V } e. (Edg ` G ) <-> <" V "> e. ( 1 ClWWalksN G ) ) )
Theorem	clwwlkn1loopb 16661*	A word represents a closed walk of length 1 iff this word is a singleton word consisting of a vertex with an attached loop. (Contributed by AV, 11-Feb-2022.)
|- ( W e. ( 1 ClWWalksN G ) <-> E. v e. (Vtx ` G ) ( W = <" v "> /\ { v } e. (Edg ` G ) ) )
Theorem	clwwlkn2 16662	A closed walk of length 2 represented as word is a word consisting of 2 symbols representing (not necessarily different) vertices connected by (at least) one edge. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 25-Apr-2021.)
|- ( W e. ( 2 ClWWalksN G ) <-> ( (♯ ` W ) = 2 /\ W e. Word (Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. (Edg ` G ) ) )
Theorem	clwwlkext2edg 16663	If a word concatenated with a vertex represents a closed walk (in a graph), there is an edge between this vertex and the last vertex of the word, and between this vertex and the first vertex of the word. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 27-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( W ++ <" Z "> ) e. ( N ClWWalksN G ) ) -> ( { (lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) )
Theorem	clwwlknccat 16664	The concatenation of two words representing closed walks anchored at the same vertex represents a closed walk with a length which is the sum of the lengths of the two walks. The resulting walk is a "double loop", starting at the common vertex, coming back to the common vertex by the first walk, following the second walk and finally coming back to the common vertex again. (Contributed by AV, 24-Apr-2022.)
|- ( ( A e. ( M ClWWalksN G ) /\ B e. ( N ClWWalksN G ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A ++ B ) e. ( ( M + N ) ClWWalksN G ) )
Theorem	umgr2cwwk2dif 16665	If a word represents a closed walk of length at least 2 in a multigraph, the first two symbols of the word must be different. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 30-Apr-2021.)
|- ( ( G e. UMGraph /\ N e. ( ZZ>= ` 2 ) /\ W e. ( N ClWWalksN G ) ) -> ( W ` 1 ) =/= ( W ` 0 ) )
Theorem	umgr2cwwkdifex 16666*	If a word represents a closed walk of length at least 2 in a undirected simple graph, there must be a symbol different from the first symbol of the word. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 30-Apr-2021.)
|- ( ( G e. UMGraph /\ N e. ( ZZ>= ` 2 ) /\ W e. ( N ClWWalksN G ) ) -> E. i e. ( 0..^ N ) ( W ` i ) =/= ( W ` 0 ) )
12.3.3.3  Closed walks on a vertex of a fixed length as words
Syntax	cclwwlknon 16667	Extend class notation with closed walks (in an undirected graph) anchored at a fixed vertex and of a fixed length as word over the set of vertices.
class ClWWalksNOn
Definition	df-clwwlknon 16668*	Define the set of all closed walks a graph g, anchored at a fixed vertex v (i.e., a walk starting and ending at the fixed vertex v, also called "a closed walk on vertex v") and having a fixed length n as words over the set of vertices. Such a word corresponds to the sequence v=p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0)=v . The set ( ( v (ClWWalksNOn ` g ) n ) corresponds to the set of "walks from v to v of length n" in a statement of [Huneke] p. 2. (Contributed by AV, 24-Feb-2022.)
|- ClWWalksNOn = ( g e. _V |-> ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )
Theorem	clwwlknonmpo 16669*	(ClWWalksNOn ` G ) is an operator mapping a vertex v and a nonnegative integer n to the set of closed walks on v of length n as words over the set of vertices in a graph G. (Contributed by AV, 25-Feb-2022.) (Proof shortened by AV, 2-Mar-2024.)
|- (ClWWalksNOn ` G ) = ( v e. (Vtx ` G ) , n e. NN0 |-> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } )
Theorem	clwwlknon 16670*	The set of closed walks on vertex X of length N in a graph G as words over the set of vertices. (Contributed by Alexander van der Vekens, 14-Sep-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 24-Mar-2022.)
|- ( X (ClWWalksNOn ` G ) N ) = { w e. ( N ClWWalksN G ) | ( w ` 0 ) = X }
Theorem	isclwwlknon 16671	A word over the set of vertices representing a closed walk on vertex X of length N in a graph G. (Contributed by AV, 25-Feb-2022.) (Revised by AV, 24-Mar-2022.)
|- ( W e. ( X (ClWWalksNOn ` G ) N ) <-> ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) )
Theorem	clwwlk0on0 16672	There is no word over the set of vertices representing a closed walk on vertex X of length 0 in a graph G. (Contributed by AV, 17-Feb-2022.) (Revised by AV, 25-Feb-2022.)
|- ( X (ClWWalksNOn ` G ) 0 ) = (/)
Theorem	clwwlknonel 16673*	Characterization of a word over the set of vertices representing a closed walk on vertex X of (nonzero) length N in a graph G. This theorem would not hold for N = 0 if W = X = (/). (Contributed by Alexander van der Vekens, 20-Sep-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 24-Mar-2022.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( N =/= 0 -> ( W e. ( X (ClWWalksNOn ` G ) N ) <-> ( ( W e. Word V /\ A. i e. ( 0..^ ( (♯ ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { (lastS ` W ) , ( W ` 0 ) } e. E ) /\ (♯ ` W ) = N /\ ( W ` 0 ) = X ) ) )
Theorem	clwwlknonccat 16674	The concatenation of two words representing closed walks on a vertex X represents a closed walk on vertex X. The resulting walk is a "double loop", starting at vertex X, coming back to X by the first walk, following the second walk and finally coming back to X again. (Contributed by AV, 24-Apr-2022.)
|- ( ( A e. ( X (ClWWalksNOn ` G ) M ) /\ B e. ( X (ClWWalksNOn ` G ) N ) ) -> ( A ++ B ) e. ( X (ClWWalksNOn ` G ) ( M + N ) ) )
Theorem	clwwlknon2 16675*	The set of closed walks on vertex X of length 2 in a graph G as words over the set of vertices. (Contributed by AV, 5-Mar-2022.) (Revised by AV, 25-Mar-2022.)
|- C = (ClWWalksNOn ` G )   =>    |- ( X C 2 ) = { w e. ( 2 ClWWalksN G ) | ( w ` 0 ) = X }
Theorem	clwwlknon2x 16676*	The set of closed walks on vertex X of length 2 in a graph G as words over the set of vertices, definition of ClWWalksN expanded. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 25-Mar-2022.)
|- C = (ClWWalksNOn ` G )   &    |- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( X C 2 ) = { w e. Word V | ( (♯ ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. E /\ ( w ` 0 ) = X ) }
Theorem	s2elclwwlknon2 16677	Sufficient conditions of a doubleton word to represent a closed walk on vertex X of length 2. (Contributed by AV, 11-May-2022.)
|- C = (ClWWalksNOn ` G )   &    |- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( X e. V /\ Y e. V /\ { X , Y } e. E ) -> <" X Y "> e. ( X C 2 ) )
Theorem	clwwlknonex2lem1 16678	Lemma 1 for clwwlknonex2 16680: Transformation of a special half-open integer range into a union of a smaller half-open integer range and an unordered pair. This Lemma would not hold for N = 2, i.e., (♯ ` W ) = 0, because ( 0..^ ( ( (♯ ` W ) + 2 ) - 1 ) ) = ( 0..^ ( ( 0 + 2 ) - 1 ) ) = ( 0..^ 1 ) = { 0 } =/= { -u 1 , 0 } = ( (/) u. { -u 1 , 0 } ) = ( ( 0..^ ( 0 - 1 ) ) u. { ( 0 - 1 ) , 0 } ) = ( ( 0..^ ( (♯ ` W ) - 1 ) ) u. { ( (♯ ` W ) - 1 ) , (♯ ` W ) } ). (Contributed by AV, 22-Sep-2018.) (Revised by AV, 26-Jan-2022.)
|- ( ( N e. ( ZZ>= ` 3 ) /\ (♯ ` W ) = ( N - 2 ) ) -> ( 0..^ ( ( (♯ ` W ) + 2 ) - 1 ) ) = ( ( 0..^ ( (♯ ` W ) - 1 ) ) u. { ( (♯ ` W ) - 1 ) , (♯ ` W ) } ) )
Theorem	clwwlknonex2lem2 16679*	Lemma 2 for clwwlknonex2 16680: Transformation of a walk and two edges into a walk extended by two vertices/edges. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 27-Jan-2022.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0..^ ( (♯ ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { (lastS ` W ) , ( W ` 0 ) } e. E ) /\ (♯ ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> A. i e. ( ( 0..^ ( (♯ ` W ) - 1 ) ) u. { ( (♯ ` W ) - 1 ) , (♯ ` W ) } ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E )
Theorem	clwwlknonex2 16680	Extending a closed walk W on vertex X by an additional edge (forth and back) results in a closed walk. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 28-Mar-2022.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ { X , Y } e. E /\ W e. ( X (ClWWalksNOn ` G ) ( N - 2 ) ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( N ClWWalksN G ) )
Theorem	clwwlknonex2e 16681	Extending a closed walk W on vertex X by an additional edge (forth and back) results in a closed walk on vertex X. (Contributed by AV, 17-Apr-2022.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ { X , Y } e. E /\ W e. ( X (ClWWalksNOn ` G ) ( N - 2 ) ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( X (ClWWalksNOn ` G ) N ) )
Theorem	clwwlknun 16682*	The set of closed walks of fixed length N in a simple graph G is the union of the closed walks of the fixed length N on each of the vertices of graph G. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 3-Mar-2022.) (Proof shortened by AV, 28-Mar-2022.)
|- V = (Vtx ` G )   =>    |- ( G e. USGraph -> ( N ClWWalksN G ) = U_ x e. V ( x (ClWWalksNOn ` G ) N ) )
12.4  Eulerian paths and the Konigsberg Bridge problem
12.4.1  Eulerian paths According to Wikipedia ("Eulerian path", 9-Mar-2021, https://en.wikipedia.org/wiki/Eulerian_path): "In graph theory, an Eulerian trail (or Eulerian path) is a trail in a finite graph that visits every edge exactly once (allowing for revisiting vertices). Similarly, an Eulerian circuit or Eulerian cycle is an Eulerian trail that starts and ends on the same vertex. ... The term Eulerian graph has two common meanings in graph theory. One meaning is a graph with an Eulerian circuit, and the other is a graph with every vertex of even degree. These definitions coincide for connected graphs. ... A graph that has an Eulerian trail but not an Eulerian circuit is called semi-Eulerian."
Syntax	ceupth 16683	Extend class notation with Eulerian paths.
class EulerPaths
Definition	df-eupth 16684*	Define the set of all Eulerian paths on an arbitrary graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
|- EulerPaths = ( g e. _V |-> { <. f , p >. | ( f (Trails ` g ) p /\ f : ( 0..^ (♯ ` f ) ) -onto-> dom (iEdg ` g ) ) } )
Theorem	releupth 16685	The set (EulerPaths ` G ) of all Eulerian paths on G is a set of pairs by our definition of an Eulerian path, and so is a relation. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
|- Rel (EulerPaths ` G )
Theorem	eupthsg 16686*	The Eulerian paths on the graph G. (Contributed by AV, 18-Feb-2021.) (Revised by AV, 29-Oct-2021.)
|- I = (iEdg ` G )   =>    |- ( G e. V -> (EulerPaths ` G ) = { <. f , p >. | ( f (Trails ` G ) p /\ f : ( 0..^ (♯ ` f ) ) -onto-> dom I ) } )
Theorem	eupthv 16687	The classes involved in a Eulerian path are sets. (Contributed by Jim Kingdon, 13-Mar-2026.)
|- ( F (EulerPaths ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
Theorem	iseupth 16688	The property " <. F , P >. is an Eulerian path on the graph G". An Eulerian path is defined as bijection F from the edges to a set 0 ... ( N - 1 ) and a function P : ( 0 ... N ) --> V into the vertices such that for each 0 <_ k < N, F ( k ) is an edge from P ( k ) to P ( k + 1 ). (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 18-Feb-2021.) (Revised by AV, 30-Oct-2021.)
|- I = (iEdg ` G )   =>    |- ( F (EulerPaths ` G ) P <-> ( F (Trails ` G ) P /\ F : ( 0..^ (♯ ` F ) ) -onto-> dom I ) )
Theorem	iseupthf1o 16689	The property " <. F , P >. is an Eulerian path on the graph G". An Eulerian path is defined as bijection F from the edges to a set 0 ... ( N - 1 ) and a function P : ( 0 ... N ) --> V into the vertices such that for each 0 <_ k < N, F ( k ) is an edge from P ( k ) to P ( k + 1 ). (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 18-Feb-2021.) (Revised by AV, 30-Oct-2021.)
|- I = (iEdg ` G )   =>    |- ( F (EulerPaths ` G ) P <-> ( F (Walks ` G ) P /\ F : ( 0..^ (♯ ` F ) ) -1-1-onto-> dom I ) )
Theorem	eupthi 16690	Properties of an Eulerian path. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.)
|- I = (iEdg ` G )   =>    |- ( F (EulerPaths ` G ) P -> ( F (Walks ` G ) P /\ F : ( 0..^ (♯ ` F ) ) -1-1-onto-> dom I ) )
Theorem	eupthf1o 16691	The F function in an Eulerian path is a bijection from a half-open range of nonnegative integers to the set of edges. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
|- I = (iEdg ` G )   =>    |- ( F (EulerPaths ` G ) P -> F : ( 0..^ (♯ ` F ) ) -1-1-onto-> dom I )
Theorem	eupthfi 16692	Any graph with an Eulerian path is of finite size, i.e. with a finite number of edges. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 18-Feb-2021.)
|- I = (iEdg ` G )   =>    |- ( F (EulerPaths ` G ) P -> dom I e. Fin )
Theorem	eupthseg 16693	The N-th edge in an eulerian path is the edge having P ( N ) and P ( N + 1 ) as endpoints . (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
|- I = (iEdg ` G )   =>    |- ( ( F (EulerPaths ` G ) P /\ N e. ( 0..^ (♯ ` F ) ) ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) )
Theorem	eupthcl 16694	An Eulerian path has length ♯ ( F ), which is an integer. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
|- ( F (EulerPaths ` G ) P -> (♯ ` F ) e. NN0 )
Theorem	eupthistrl 16695	An Eulerian path is a trail. (Contributed by Alexander van der Vekens, 24-Nov-2017.) (Revised by AV, 18-Feb-2021.)
|- ( F (EulerPaths ` G ) P -> F (Trails ` G ) P )
Theorem	eupthiswlk 16696	An Eulerian path is a walk. (Contributed by AV, 6-Apr-2021.)
|- ( F (EulerPaths ` G ) P -> F (Walks ` G ) P )
Theorem	eupthpf 16697	The P function in an Eulerian path is a function from a finite sequence of nonnegative integers to the vertices. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
|- ( F (EulerPaths ` G ) P -> P : ( 0 ... (♯ ` F ) ) --> (Vtx ` G ) )
Theorem	eupthres 16698	The restriction <. H , Q >. of an Eulerian path <. F , P >. to an initial segment of the path (of length N) forms an Eulerian path on the subgraph S consisting of the edges in the initial segment. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 6-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (EulerPaths ` G ) P )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> (iEdg ` S ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- H = ( F prefix N )   &    |- Q = ( P |` ( 0 ... N ) )   &    |- (Vtx ` S ) = V   =>    |- ( ph -> H (EulerPaths ` S ) Q )
Theorem	eupth2lem1 16699	Lemma for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015.)
|- ( U e. V -> ( U e. if ( A = B , (/) , { A , B } ) <-> ( A =/= B /\ ( U = A \/ U = B ) ) ) )
Theorem	eupth2lem2dc 16700	Lemma for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015.)
|- ( ph -> B e. X )   &    |- ( ph -> DECID A = B )   &    |- ( ph -> B =/= C )   &    |- ( ph -> B = U )   =>    |- ( ph -> ( -. U e. if ( A = B , (/) , { A , B } ) <-> U e. if ( A = C , (/) , { A , C } ) ) )