P. 163 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16201-16300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wlkvtxeledgg 16201*	Each pair of adjacent vertices in a walk is a subset of an edge. (Contributed by AV, 28-Jan-2021.) (Proof shortened by AV, 4-Apr-2021.)
|- I = (iEdg ` G )   =>    |- ( ( G e. W /\ F (Walks ` G ) P ) -> A. k e. ( 0..^ (♯ ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
Theorem	wlkvtxiedg 16202*	The vertices of a walk are connected by indexed edges. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) (Proof shortened by AV, 4-Apr-2021.)
|- I = (iEdg ` G )   =>    |- ( F (Walks ` G ) P -> A. k e. ( 0..^ (♯ ` F ) ) E. e e. ran I { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e )
Theorem	wlkvtxiedgg 16203*	The vertices of a walk are connected by indexed edges. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) (Proof shortened by AV, 4-Apr-2021.)
|- I = (iEdg ` G )   =>    |- ( ( G e. W /\ F (Walks ` G ) P ) -> A. k e. ( 0..^ (♯ ` F ) ) E. e e. ran I { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e )
Theorem	relwlk 16204	The set (Walks ` G ) of all walks on G is a set of pairs by our definition of a walk, and so is a relation. (Contributed by Alexander van der Vekens, 30-Jun-2018.) (Revised by AV, 19-Feb-2021.)
|- Rel (Walks ` G )
Theorem	wlkop 16205	A walk is an ordered pair. (Contributed by Alexander van der Vekens, 30-Jun-2018.) (Revised by AV, 1-Jan-2021.)
|- ( W e. (Walks ` G ) -> W = <. ( 1st ` W ) , ( 2nd ` W ) >. )
Theorem	wlkelvv 16206	A walk is an ordered pair. (Contributed by Jim Kingdon, 2-Feb-2026.)
|- ( W e. (Walks ` G ) -> W e. ( _V X. _V ) )
Theorem	wlkcprim 16207	A walk as class with two components. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) (Revised by Jim Kingdon, 1-Feb-2026.)
|- ( W e. (Walks ` G ) -> ( 1st ` W ) (Walks ` G ) ( 2nd ` W ) )
Theorem	wlk2f 16208*	If there is a walk W there is a pair of functions representing this walk. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
|- ( W e. (Walks ` G ) -> E. f E. p f (Walks ` G ) p )
Theorem	wlkcompim 16209*	Implications for the properties of the components of a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 2-Jan-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- F = ( 1st ` W )   &    |- P = ( 2nd ` W )   =>    |- ( W e. (Walks ` G ) -> ( F e. Word dom I /\ P : ( 0 ... (♯ ` F ) ) --> V /\ A. k e. ( 0..^ (♯ ` F ) )if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )
Theorem	wlkelwrd 16210	The components of a walk are words/functions over a zero based range of integers. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 2-Jan-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- F = ( 1st ` W )   &    |- P = ( 2nd ` W )   =>    |- ( W e. (Walks ` G ) -> ( F e. Word dom I /\ P : ( 0 ... (♯ ` F ) ) --> V ) )
Theorem	wlkeq 16211*	Conditions for two walks (within the same graph) being the same. (Contributed by AV, 1-Jul-2018.) (Revised by AV, 16-May-2019.) (Revised by AV, 14-Apr-2021.)
|- ( ( A e. (Walks ` G ) /\ B e. (Walks ` G ) /\ N = (♯ ` ( 1st ` A ) ) ) -> ( A = B <-> ( N = (♯ ` ( 1st ` B ) ) /\ A. x e. ( 0..^ N ) ( ( 1st ` A ) ` x ) = ( ( 1st ` B ) ` x ) /\ A. x e. ( 0 ... N ) ( ( 2nd ` A ) ` x ) = ( ( 2nd ` B ) ` x ) ) ) )
Theorem	edginwlkd 16212	The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 2-Jan-2021.) (Revised by AV, 9-Dec-2021.) (Revised by Jim Kingdon, 2-Feb-2026.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> F e. Word dom I )   &    |- ( ph -> K e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> G e. V )   =>    |- ( ph -> ( I ` ( F ` K ) ) e. E )
Theorem	upgredginwlk 16213	The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 2-Jan-2021.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. UPGraph /\ F e. Word dom I ) -> ( K e. ( 0..^ (♯ ` F ) ) -> ( I ` ( F ` K ) ) e. E ) )
Theorem	iedginwlk 16214	The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 23-Apr-2021.)
|- I = (iEdg ` G )   =>    |- ( ( Fun I /\ F (Walks ` G ) P /\ X e. ( 0..^ (♯ ` F ) ) ) -> ( I ` ( F ` X ) ) e. ran I )
Theorem	wlkl1loop 16215	A walk of length 1 from a vertex to itself is a loop. (Contributed by AV, 23-Apr-2021.)
|- ( ( ( Fun (iEdg ` G ) /\ F (Walks ` G ) P ) /\ ( (♯ ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> { ( P ` 0 ) } e. (Edg ` G ) )
Theorem	wlk1walkdom 16216*	A walk is a 1-walk "on the edge level" according to Aksoy et al. (Contributed by AV, 30-Dec-2020.)
|- I = (iEdg ` G )   =>    |- ( F (Walks ` G ) P -> A. k e. ( 1..^ (♯ ` F ) ) 1o ~<_ ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) )
Theorem	upgriswlkdc 16217*	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 16218*	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 16219*	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 16220*	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 16221*	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 16222*	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 16223	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 16224	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 16225*	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 16226	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 16227	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 16228	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 16229	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 16230	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 16231	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 16232	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 16233*	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 16234*	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 16235	Lemma for wlkres 16236. (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 16236	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 16237	Extend class notation with trails (within a graph).
class Trails
Definition	df-trls 16238*	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 16239	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 16240*	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 16241	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 16242	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 16243	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 16244	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 16245	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 16246	Lemma for trlres 16247. (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 16247	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 16248	Extend class notation with closed walks (in an undirected graph) as word over the set of vertices.
class ClWWalks
Definition	df-clwwlk 16249*	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 16250*	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 16251*	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 16252	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 16253	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 16254	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 16255	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 16256	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 16257*	Lemma for clwwlkccat 16258: 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 16258	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 16259	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 16260	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 16261*	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 16265. (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 16262*	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 16263	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 16264	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 16265	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 16266	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 16267	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 16268	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 16269	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 16270	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 16271	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 16272	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 16273*	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 16274*	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 16275	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 16276	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 16277*	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 16278	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 16279	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 16280	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 16281	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 16282*	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 16283	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 16284*	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 16285*	(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 16286*	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 16287	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 16288	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 16289*	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 16290	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 16291*	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 16292*	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 16293	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 16294	Lemma 1 for clwwlknonex2 16296: 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 16295*	Lemma 2 for clwwlknonex2 16296: 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 16296	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 16297	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 16298*	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 16299	Extend class notation with Eulerian paths.
class EulerPaths
Definition	df-eupth 16300*	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 ) ) } )