Definition df-wlks

Description: 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 wlk1walk ) discussed in Aksoy et al. The predicate F ( WalksG ) P can be read as "The pair <. F , P >. represents a walk in a graph G ", see also iswlk .

The condition { ( pk ) , ( p( k + 1 ) ) } C_ ( ( iEdgg )( fk ) ) (hereinafter referred to as C) would not be sufficient, because the repetition of a vertex in a walk (i.e. ( pk ) = ( p( k + 1 ) ) should be allowed only if there is a loop at ( pk ) . Otherwise, C would be fulfilled by each edge containing ( pk ) .

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)

	Ref	Expression
Assertion	df-wlks	|- 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 ) ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwlks	|- Walks
1		vg	|- g
2		cvv	|- _V
3		vf	|- f
4		vp	|- p
5	3	cv	|- f
6		ciedg	|- iEdg
7	1	cv	|- g
8	7 6	cfv	|- ( iEdg ` g )
9	8	cdm	|- dom ( iEdg ` g )
10	9	cword	|- Word dom ( iEdg ` g )
11	5 10	wcel	|- f e. Word dom ( iEdg ` g )
12	4	cv	|- p
13		cc0	|- 0
14		cfz	|- ...
15		chash	|- #
16	5 15	cfv	|- ( # ` f )
17	13 16 14	co	|- ( 0 ... ( # ` f ) )
18		cvtx	|- Vtx
19	7 18	cfv	|- ( Vtx ` g )
20	17 19 12	wf	|- p : ( 0 ... ( # ` f ) ) --> ( Vtx ` g )
21		vk	|- k
22		cfzo	|- ..^
23	13 16 22	co	|- ( 0 ..^ ( # ` f ) )
24	21	cv	|- k
25	24 12	cfv	|- ( p ` k )
26		caddc	|- +
27		c1	|- 1
28	24 27 26	co	|- ( k + 1 )
29	28 12	cfv	|- ( p ` ( k + 1 ) )
30	25 29	wceq	|- ( p ` k ) = ( p ` ( k + 1 ) )
31	24 5	cfv	|- ( f ` k )
32	31 8	cfv	|- ( ( iEdg ` g ) ` ( f ` k ) )
33	25	csn	|- { ( p ` k ) }
34	32 33	wceq	|- ( ( iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) }
35	25 29	cpr	|- { ( p ` k ) , ( p ` ( k + 1 ) ) }
36	35 32	wss	|- { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( ( iEdg ` g ) ` ( f ` k ) )
37	30 34 36	wif	|- if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( ( iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( ( iEdg ` g ) ` ( f ` k ) ) )
38	37 21 23	wral	|- 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 ) ) )
39	11 20 38	w3a	|- ( 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 ) ) ) )
40	39 3 4	copab	|- { <. 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 ) ) ) ) }
41	1 2 40	cmpt	|- ( 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 ) ) ) ) } )
42	0 41	wceq	|- 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 ) ) ) ) } )