P. 162 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16101-16200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	vtxlpfi 16101*	In a finite graph, the number of loops from a given vertex is finite. (Contributed by Jim Kingdon, 16-Feb-2026.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- A = dom I   &    |- ( ph -> A e. Fin )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> U e. V )   &    |- ( ph -> G e. UPGraph )   =>    |- ( ph -> { x e. A | ( I ` x ) = { U } } e. Fin )
Theorem	vtxdgfifival 16102*	The degree of a vertex for graphs with finite vertex and edge sets. (Contributed by Jim Kingdon, 10-Feb-2026.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- A = dom I   &    |- ( ph -> A e. Fin )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> U e. V )   &    |- ( ph -> G e. UPGraph )   =>    |- ( ph -> ( (VtxDeg ` G ) ` U ) = ( (♯ ` { x e. A | U e. ( I ` x ) } ) + (♯ ` { x e. A | ( I ` x ) = { U } } ) ) )
Theorem	vtxdgop 16103	The vertex degree expressed as operation. (Contributed by AV, 12-Dec-2021.)
|- ( G e. W -> (VtxDeg ` G ) = ( (Vtx ` G )VtxDeg (iEdg ` G ) ) )
Theorem	vtxdgfif 16104	In a finite graph, the vertex degree function is a function from vertices to nonnegative integers. (Contributed by Jim Kingdon, 17-Feb-2026.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- A = dom I   &    |- ( ph -> A e. Fin )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> G e. UPGraph )   =>    |- ( ph -> (VtxDeg ` G ) : V --> NN0 )
Theorem	vtxdg0v 16105	The degree of a vertex in the null graph is zero (or anything else), because there are no vertices. (Contributed by AV, 11-Dec-2020.)
|- V = (Vtx ` G )   =>    |- ( ( G = (/) /\ U e. V ) -> ( (VtxDeg ` G ) ` U ) = 0 )
Theorem	vtxdgfi0e 16106	The degree of a vertex in an empty graph is zero, because there are no edges. This is the base case for the induction for calculating the degree of a vertex, for example in a Königsberg graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.) (Revised by AV, 22-Mar-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> U e. V )   &    |- ( ph -> I = (/) )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> G e. UPGraph )   =>    |- ( ph -> ( (VtxDeg ` G ) ` U ) = 0 )
Theorem	vtxdeqd 16107	Equality theorem for the vertex degree: If two graphs are structurally equal, their vertex degree functions are equal. (Contributed by AV, 26-Feb-2021.)
|- ( ph -> G e. X )   &    |- ( ph -> H e. Y )   &    |- ( ph -> (Vtx ` H ) = (Vtx ` G ) )   &    |- ( ph -> (iEdg ` H ) = (iEdg ` G ) )   =>    |- ( ph -> (VtxDeg ` H ) = (VtxDeg ` G ) )
Theorem	vtxdfifiun 16108	The degree of a vertex in the union of two pseudographs of finite size on the same finite vertex set is the sum of the degrees of the vertex in each pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 19-Feb-2021.)
|- I = (iEdg ` G )   &    |- J = (iEdg ` H )   &    |- V = (Vtx ` G )   &    |- ( ph -> (Vtx ` H ) = V )   &    |- ( ph -> (Vtx ` U ) = V )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> G e. UPGraph )   &    |- ( ph -> H e. UPGraph )   &    |- ( ph -> ( dom I i^i dom J ) = (/) )   &    |- ( ph -> Fun I )   &    |- ( ph -> Fun J )   &    |- ( ph -> N e. V )   &    |- ( ph -> (iEdg ` U ) = ( I u. J ) )   &    |- ( ph -> dom I e. Fin )   &    |- ( ph -> dom J e. Fin )   =>    |- ( ph -> ( (VtxDeg ` U ) ` N ) = ( ( (VtxDeg ` G ) ` N ) + ( (VtxDeg ` H ) ` N ) ) )
Theorem	vtxdumgrfival 16109*	The value of the vertex degree function for a finite multigraph. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 23-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- A = dom I   &    |- D = (VtxDeg ` G )   &    |- ( ph -> G e. UMGraph )   &    |- ( ph -> U e. V )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> V e. Fin )   =>    |- ( ph -> ( D ` U ) = (♯ ` { x e. A | U e. ( I ` x ) } ) )
Theorem	vtxd0nedgbfi 16110*	A vertex has degree 0 iff there is no edge incident with the vertex. (Contributed by AV, 24-Dec-2020.) (Revised by AV, 22-Mar-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- D = (VtxDeg ` G )   &    |- ( ph -> dom I e. Fin )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> U e. V )   &    |- ( ph -> G e. UPGraph )   =>    |- ( ph -> ( ( D ` U ) = 0 <-> -. E. i e. dom I U e. ( I ` i ) ) )
Theorem	vtxduspgrfvedgfilem 16111*	Lemma for vtxduspgrfvedgfi 16112 and vtxdusgrfvedgfi 16113. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- ( ph -> dom (iEdg ` G ) e. Fin )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> U e. V )   &    |- ( ph -> G e. USPGraph )   =>    |- ( ph -> (♯ ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) = (♯ ` { e e. E | U e. e } ) )
Theorem	vtxduspgrfvedgfi 16112*	The value of the vertex degree function for a simple pseudograph. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- ( ph -> dom (iEdg ` G ) e. Fin )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> U e. V )   &    |- ( ph -> G e. USPGraph )   &    |- D = (VtxDeg ` G )   =>    |- ( ph -> ( D ` U ) = ( (♯ ` { e e. E | U e. e } ) + (♯ ` { e e. E | e = { U } } ) ) )
Theorem	vtxdusgrfvedgfi 16113*	The value of the vertex degree function for a simple graph. (Contributed by AV, 12-Dec-2020.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   &    |- ( ph -> dom (iEdg ` G ) e. Fin )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> U e. V )   &    |- ( ph -> G e. USGraph )   &    |- D = (VtxDeg ` G )   =>    |- ( ph -> ( D ` U ) = (♯ ` { e e. E | U e. e } ) )
Theorem	1loopgruspgr 16114	A graph with one edge which is a loop is a simple pseudograph. (Contributed by AV, 21-Feb-2021.)
|- ( ph -> (Vtx ` G ) = V )   &    |- ( ph -> A e. X )   &    |- ( ph -> N e. V )   &    |- ( ph -> (iEdg ` G ) = { <. A , { N } >. } )   =>    |- ( ph -> G e. USPGraph )
Theorem	1loopgredg 16115	The set of edges in a graph (simple pseudograph) with one edge which is a loop is a singleton of a singleton. (Contributed by AV, 17-Dec-2020.) (Revised by AV, 21-Feb-2021.)
|- ( ph -> (Vtx ` G ) = V )   &    |- ( ph -> A e. X )   &    |- ( ph -> N e. V )   &    |- ( ph -> (iEdg ` G ) = { <. A , { N } >. } )   =>    |- ( ph -> (Edg ` G ) = { { N } } )
Theorem	1loopgrvd2fi 16116	The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. I. e. in a graph (simple pseudograph) with one edge which is a loop, the vertex connected with itself by the loop has degree 2. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.)
|- ( ph -> (Vtx ` G ) = V )   &    |- ( ph -> A e. X )   &    |- ( ph -> N e. V )   &    |- ( ph -> (iEdg ` G ) = { <. A , { N } >. } )   &    |- ( ph -> V e. Fin )   =>    |- ( ph -> ( (VtxDeg ` G ) ` N ) = 2 )
Theorem	1loopgrvd0fi 16117	The vertex degree of a one-edge graph, case 1 (for a loop): a loop at a vertex other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 21-Feb-2021.)
|- ( ph -> (Vtx ` G ) = V )   &    |- ( ph -> A e. X )   &    |- ( ph -> N e. V )   &    |- ( ph -> (iEdg ` G ) = { <. A , { N } >. } )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> K e. ( V \ { N } ) )   =>    |- ( ph -> ( (VtxDeg ` G ) ` K ) = 0 )
Theorem	1hevtxdg0fi 16118	The vertex degree of vertex D in a finite pseudograph G with only one edge E is 0 if D is not incident with the edge E. (Contributed by AV, 2-Mar-2021.) (Revised by Jim Kingdon, 13-Mar-2026.)
|- ( ph -> (iEdg ` G ) = { <. A , E >. } )   &    |- ( ph -> (Vtx ` G ) = V )   &    |- ( ph -> A e. X )   &    |- ( ph -> D e. V )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> G e. UPGraph )   &    |- ( ph -> E e. Y )   &    |- ( ph -> D e/ E )   =>    |- ( ph -> ( (VtxDeg ` G ) ` D ) = 0 )
Theorem	1hevtxdg1en 16119	The vertex degree of vertex D in a multigraph G with only one edge E is 1 if D is incident with the edge E. (Contributed by AV, 2-Mar-2021.) (Proof shortened by AV, 17-Apr-2021.)
|- ( ph -> (iEdg ` G ) = { <. A , E >. } )   &    |- ( ph -> (Vtx ` G ) = V )   &    |- ( ph -> A e. X )   &    |- ( ph -> D e. V )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> G e. UMGraph )   &    |- ( ph -> E e. ~P V )   &    |- ( ph -> D e. E )   &    |- ( ph -> E ~~ 2o )   =>    |- ( ph -> ( (VtxDeg ` G ) ` D ) = 1 )
Theorem	1hegrvtxdg1fi 16120	The vertex degree of a multigraph with one edge, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 23-Feb-2021.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> B =/= C )   &    |- ( ph -> E e. ~P V )   &    |- ( ph -> (iEdg ` G ) = { <. A , E >. } )   &    |- ( ph -> { B , C } C_ E )   &    |- ( ph -> (Vtx ` G ) = V )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> G e. UMGraph )   =>    |- ( ph -> ( (VtxDeg ` G ) ` B ) = 1 )
Theorem	1hegrvtxdg1rfi 16121	The vertex degree of a graph with one hyperedge, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 23-Feb-2021.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> B =/= C )   &    |- ( ph -> E e. ~P V )   &    |- ( ph -> (iEdg ` G ) = { <. A , E >. } )   &    |- ( ph -> { B , C } C_ E )   &    |- ( ph -> (Vtx ` G ) = V )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> G e. UMGraph )   =>    |- ( ph -> ( (VtxDeg ` G ) ` C ) = 1 )
Theorem	p1evtxdeqfilem 16122	Lemma for p1evtxdeqfi 16123 and p1evtxdp1fi 16124. (Contributed by AV, 3-Mar-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> (Vtx ` F ) = V )   &    |- ( ph -> (iEdg ` F ) = ( I u. { <. K , E >. } ) )   &    |- ( ph -> K e. X )   &    |- ( ph -> K e/ dom I )   &    |- ( ph -> U e. V )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> G e. UPGraph )   &    |- ( ph -> dom I e. Fin )   &    |- ( ph -> E e. ~P V )   &    |- ( ph -> E ~~ 2o )   &    |- ( ph -> E e. Y )   =>    |- ( ph -> ( (VtxDeg ` F ) ` U ) = ( ( (VtxDeg ` G ) ` U ) + ( (VtxDeg ` <. V , { <. K , E >. } >. ) ` U ) ) )
Theorem	p1evtxdeqfi 16123	If an edge E which does not contain vertex U is added to a graph G (yielding a graph F), the degree of U is the same in both graphs. (Contributed by AV, 2-Mar-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> (Vtx ` F ) = V )   &    |- ( ph -> (iEdg ` F ) = ( I u. { <. K , E >. } ) )   &    |- ( ph -> K e. X )   &    |- ( ph -> K e/ dom I )   &    |- ( ph -> U e. V )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> G e. UPGraph )   &    |- ( ph -> dom I e. Fin )   &    |- ( ph -> E e. ~P V )   &    |- ( ph -> E ~~ 2o )   &    |- ( ph -> E e. Y )   &    |- ( ph -> U e/ E )   =>    |- ( ph -> ( (VtxDeg ` F ) ` U ) = ( (VtxDeg ` G ) ` U ) )
Theorem	p1evtxdp1fi 16124	If an edge E (not being a loop) which contains vertex U is added to a graph G (yielding a graph F), the degree of U is increased by 1. (Contributed by AV, 3-Mar-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> (Vtx ` F ) = V )   &    |- ( ph -> (iEdg ` F ) = ( I u. { <. K , E >. } ) )   &    |- ( ph -> K e. X )   &    |- ( ph -> K e/ dom I )   &    |- ( ph -> U e. V )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> G e. UPGraph )   &    |- ( ph -> dom I e. Fin )   &    |- ( ph -> E e. ~P V )   &    |- ( ph -> E ~~ 2o )   &    |- ( ph -> U e. E )   =>    |- ( ph -> ( (VtxDeg ` F ) ` U ) = ( ( (VtxDeg ` G ) ` U ) + 1 ) )
Theorem	vdegp1aid 16125*	The induction step for a vertex degree calculation. If the degree of U in the edge set E is P, then adding { X , Y } to the edge set, where X =/= U =/= Y, yields degree P as well. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.)
|- V = (Vtx ` G )   &    |- ( ph -> U e. V )   &    |- I = (iEdg ` G )   &    |- ( ph -> I e. Word { x e. ~P V | ( x ~~ 1o \/ x ~~ 2o ) } )   &    |- ( ph -> ( (VtxDeg ` G ) ` U ) = P )   &    |- ( ph -> (Vtx ` F ) = V )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> X e. V )   &    |- ( ph -> X =/= U )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Y =/= U )   &    |- ( ph -> X =/= Y )   &    |- ( ph -> (iEdg ` F ) = ( I ++ <" { X , Y } "> ) )   =>    |- ( ph -> ( (VtxDeg ` F ) ` U ) = P )
Theorem	vdegp1bid 16126*	The induction step for a vertex degree calculation, for example in the Königsberg graph. If the degree of U in the edge set E is P, then adding { U , X } to the edge set, where X =/= U, yields degree P + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.)
|- V = (Vtx ` G )   &    |- ( ph -> U e. V )   &    |- I = (iEdg ` G )   &    |- ( ph -> I e. Word { x e. ~P V | ( x ~~ 1o \/ x ~~ 2o ) } )   &    |- ( ph -> ( (VtxDeg ` G ) ` U ) = P )   &    |- ( ph -> (Vtx ` F ) = V )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> X e. V )   &    |- ( ph -> X =/= U )   &    |- ( ph -> (iEdg ` F ) = ( I ++ <" { U , X } "> ) )   =>    |- ( ph -> ( (VtxDeg ` F ) ` U ) = ( P + 1 ) )
Theorem	vdegp1cid 16127*	The induction step for a vertex degree calculation, for example in the Königsberg graph. If the degree of U in the edge set E is P, then adding { X , U } to the edge set, where X =/= U, yields degree P + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.)
|- V = (Vtx ` G )   &    |- ( ph -> U e. V )   &    |- I = (iEdg ` G )   &    |- ( ph -> I e. Word { x e. ~P V | ( x ~~ 1o \/ x ~~ 2o ) } )   &    |- ( ph -> ( (VtxDeg ` G ) ` U ) = P )   &    |- ( ph -> (Vtx ` F ) = V )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> X e. V )   &    |- ( ph -> X =/= U )   &    |- ( ph -> (iEdg ` F ) = ( I ++ <" { X , U } "> ) )   =>    |- ( ph -> ( (VtxDeg ` F ) ` U ) = ( P + 1 ) )
12.3  Walks, paths and cycles
12.3.1  Walks
Syntax	cwlks 16128	Extend class notation with walks (i.e. 1-walks) (of a hypergraph).
class Walks
Definition	df-wlks 16129*	Define the set of all walks (in a hypergraph). Such walks correspond to the s-walks "on the vertex level" (with s = 1), and also to 1-walks "on the edge level" (see wlk1walkdom 16170) discussed in Aksoy et al. The predicate F (Walks ` G ) P can be read as "The pair <. F , P >. represents a walk in a graph G", see also iswlk 16134. The condition { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( (iEdg ` g ) ` ( f ` k ) ) (hereinafter referred to as C) would not be sufficient, because the repetition of a vertex in a walk (i.e. ( p ` k ) = ( p ` ( k + 1 ) ) should be allowed only if there is a loop at ( p ` k ). Otherwise, C would be fulfilled by each edge containing ( p ` k ). According to the definition of [Bollobas] p. 4.: "A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) ...", a walk can be represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices. So the walk is 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 AV, 30-Dec-2020.)
|- Walks = ( g e. _V |-> { <. f , p >. | ( f e. Word dom (iEdg ` g ) /\ p : ( 0 ... (♯ ` f ) ) --> (Vtx ` g ) /\ A. k e. ( 0..^ (♯ ` f ) )if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( (iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( (iEdg ` g ) ` ( f ` k ) ) ) ) } )
Theorem	wlkmex 16130	If there are walks on a graph, the graph is a set. (Contributed by Jim Kingdon, 1-Feb-2026.)
|- ( W e. (Walks ` G ) -> G e. _V )
Theorem	wkslem1 16131	Lemma 1 for walks to substitute the index of the condition for vertices and edges in a walk. (Contributed by AV, 23-Apr-2021.)
|- ( A = B -> (if- ( ( P ` A ) = ( P ` ( A + 1 ) ) , ( I ` ( F ` A ) ) = { ( P ` A ) } , { ( P ` A ) , ( P ` ( A + 1 ) ) } C_ ( I ` ( F ` A ) ) ) <-> if- ( ( P ` B ) = ( P ` ( B + 1 ) ) , ( I ` ( F ` B ) ) = { ( P ` B ) } , { ( P ` B ) , ( P ` ( B + 1 ) ) } C_ ( I ` ( F ` B ) ) ) ) )
Theorem	wkslem2 16132	Lemma 2 for walks to substitute the index of the condition for vertices and edges in a walk. (Contributed by AV, 23-Apr-2021.)
|- ( ( A = B /\ ( A + 1 ) = C ) -> (if- ( ( P ` A ) = ( P ` ( A + 1 ) ) , ( I ` ( F ` A ) ) = { ( P ` A ) } , { ( P ` A ) , ( P ` ( A + 1 ) ) } C_ ( I ` ( F ` A ) ) ) <-> if- ( ( P ` B ) = ( P ` C ) , ( I ` ( F ` B ) ) = { ( P ` B ) } , { ( P ` B ) , ( P ` C ) } C_ ( I ` ( F ` B ) ) ) ) )
Theorem	wksfval 16133*	The set of walks (in an undirected graph). (Contributed by AV, 30-Dec-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( G e. W -> (Walks ` G ) = { <. f , p >. | ( 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	iswlk 16134*	Properties of a pair of functions to be/represent a walk. (Contributed by AV, 30-Dec-2020.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ( G e. W /\ F e. U /\ P e. Z ) -> ( F (Walks ` G ) P <-> ( 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	wlkpropg 16135*	Properties of a walk. (Contributed by AV, 5-Nov-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ( G e. W /\ F (Walks ` G ) P ) -> ( 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	wlkex 16136	The class of walks on a graph is a set. (Contributed by Jim Kingdon, 7-Feb-2026.)
|- ( G e. V -> (Walks ` G ) e. _V )
Theorem	wlkv 16137	The classes involved in a walk are sets. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 3-Feb-2021.)
|- ( F (Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
Theorem	wlkprop 16138*	Properties of a walk. (Contributed by AV, 5-Nov-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( F (Walks ` G ) P -> ( 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	wlkvg 16139	The classes involved in a walk are sets. Now that we have wlkv 16137 there is no reason to use this theorem in new proofs and using wlkv 16137 is encouraged for consistency with the Metamath Proof Explorer. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 3-Feb-2021.) (New usage is discouraged.)
|- ( ( G e. W /\ F (Walks ` G ) P ) -> ( F e. _V /\ P e. _V ) )
Theorem	iswlkg 16140*	Generalization of iswlk 16134: Conditions for two classes to represent a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 1-Jan-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( G e. W -> ( F (Walks ` G ) P <-> ( 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	wlkf 16141	The mapping enumerating the (indices of the) edges of a walk is a word over the indices of the edges of the graph. (Contributed by AV, 5-Apr-2021.)
|- I = (iEdg ` G )   =>    |- ( F (Walks ` G ) P -> F e. Word dom I )
Theorem	wlkfg 16142	The mapping enumerating the (indices of the) edges of a walk is a word over the indices of the edges of the graph. (Contributed by AV, 5-Apr-2021.)
|- I = (iEdg ` G )   =>    |- ( ( G e. W /\ F (Walks ` G ) P ) -> F e. Word dom I )
Theorem	wlkcl 16143	A walk has length ♯ ( F ), which is an integer. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
|- ( F (Walks ` G ) P -> (♯ ` F ) e. NN0 )
Theorem	wlkclg 16144	A walk has length ♯ ( F ), which is an integer. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
|- ( ( G e. W /\ F (Walks ` G ) P ) -> (♯ ` F ) e. NN0 )
Theorem	wlkp 16145	The mapping enumerating the vertices of a walk is a function. (Contributed by AV, 5-Apr-2021.)
|- V = (Vtx ` G )   =>    |- ( F (Walks ` G ) P -> P : ( 0 ... (♯ ` F ) ) --> V )
Theorem	wlkpg 16146	The mapping enumerating the vertices of a walk is a function. (Contributed by AV, 5-Apr-2021.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ F (Walks ` G ) P ) -> P : ( 0 ... (♯ ` F ) ) --> V )
Theorem	wlkpwrdg 16147	The sequence of vertices of a walk is a word over the set of vertices. (Contributed by AV, 27-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ F (Walks ` G ) P ) -> P e. Word V )
Theorem	wlklenvp1 16148	The number of vertices of a walk (in an undirected graph) is the number of its edges plus 1. (Contributed by Alexander van der Vekens, 29-Jun-2018.) (Revised by AV, 1-May-2021.)
|- ( F (Walks ` G ) P -> (♯ ` P ) = ( (♯ ` F ) + 1 ) )
Theorem	wlklenvp1g 16149	The number of vertices of a walk (in an undirected graph) is the number of its edges plus 1. (Contributed by Alexander van der Vekens, 29-Jun-2018.) (Revised by AV, 1-May-2021.)
|- ( ( G e. W /\ F (Walks ` G ) P ) -> (♯ ` P ) = ( (♯ ` F ) + 1 ) )
Theorem	wlkm 16150*	The sequence of vertices of a walk cannot be empty, i.e. a walk always consists of at least one vertex. (Contributed by Alexander van der Vekens, 19-Jul-2018.) (Revised by AV, 2-Jan-2021.)
|- ( F (Walks ` G ) P -> E. x x e. P )
Theorem	wlkvtxm 16151*	A graph with a walk has at least one vertex. (Contributed by Jim Kingdon, 8-Feb-2026.)
|- V = (Vtx ` G )   =>    |- ( F (Walks ` G ) P -> E. x x e. V )
Theorem	wlklenvm1 16152	The number of edges of a walk is the number of its vertices minus 1. (Contributed by Alexander van der Vekens, 1-Jul-2018.) (Revised by AV, 2-Jan-2021.)
|- ( F (Walks ` G ) P -> (♯ ` F ) = ( (♯ ` P ) - 1 ) )
Theorem	wlklenvm1g 16153	The number of edges of a walk is the number of its vertices minus 1. (Contributed by Alexander van der Vekens, 1-Jul-2018.) (Revised by AV, 2-Jan-2021.)
|- ( ( G e. W /\ F (Walks ` G ) P ) -> (♯ ` F ) = ( (♯ ` P ) - 1 ) )
Theorem	ifpsnprss 16154	Lemma for wlkvtxeledgg 16155: Two adjacent (not necessarily different) vertices A and B in a walk are incident with an edge E. (Contributed by AV, 4-Apr-2021.) (Revised by AV, 5-Nov-2021.)
|- (if- ( A = B , E = { A } , { A , B } C_ E ) -> { A , B } C_ E )
Theorem	wlkvtxeledgg 16155*	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 16156*	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 16157*	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 16158	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 16159	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 16160	A walk is an ordered pair. (Contributed by Jim Kingdon, 2-Feb-2026.)
|- ( W e. (Walks ` G ) -> W e. ( _V X. _V ) )
Theorem	wlkcprim 16161	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 16162*	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 16163*	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 16164	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 16165*	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 16166	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 16167	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 16168	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 16169	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 16170*	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 16171*	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 16172*	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 16173*	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 16174*	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 16175*	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 16176*	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 16177	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 16178	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 16179*	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 16180	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 16181	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 16182	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 16183	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 16184	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	2wlklem 16185*	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 16186*	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 16187	Lemma for wlkres 16188. (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 16188	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 16189	Extend class notation with trails (within a graph).
class Trails
Definition	df-trls 16190*	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 16191	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 16192*	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 16193	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 16194	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 16195	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 16196	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 16197	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 16198	Lemma for trlres 16199. (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 16199	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 16200	Extend class notation with closed walks (in an undirected graph) as word over the set of vertices.
class ClWWalks