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 = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cwlks | ⊢ Walks | |
| 1 | vg | ⊢ 𝑔 | |
| 2 | cvv | ⊢ V | |
| 3 | vf | ⊢ 𝑓 | |
| 4 | vp | ⊢ 𝑝 | |
| 5 | 3 | cv | ⊢ 𝑓 |
| 6 | ciedg | ⊢ iEdg | |
| 7 | 1 | cv | ⊢ 𝑔 |
| 8 | 7 6 | cfv | ⊢ ( iEdg ‘ 𝑔 ) |
| 9 | 8 | cdm | ⊢ dom ( iEdg ‘ 𝑔 ) |
| 10 | 9 | cword | ⊢ Word dom ( iEdg ‘ 𝑔 ) |
| 11 | 5 10 | wcel | ⊢ 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) |
| 12 | 4 | cv | ⊢ 𝑝 |
| 13 | cc0 | ⊢ 0 | |
| 14 | cfz | ⊢ ... | |
| 15 | chash | ⊢ ♯ | |
| 16 | 5 15 | cfv | ⊢ ( ♯ ‘ 𝑓 ) |
| 17 | 13 16 14 | co | ⊢ ( 0 ... ( ♯ ‘ 𝑓 ) ) |
| 18 | cvtx | ⊢ Vtx | |
| 19 | 7 18 | cfv | ⊢ ( Vtx ‘ 𝑔 ) |
| 20 | 17 19 12 | wf | ⊢ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) |
| 21 | vk | ⊢ 𝑘 | |
| 22 | cfzo | ⊢ ..^ | |
| 23 | 13 16 22 | co | ⊢ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) |
| 24 | 21 | cv | ⊢ 𝑘 |
| 25 | 24 12 | cfv | ⊢ ( 𝑝 ‘ 𝑘 ) |
| 26 | caddc | ⊢ + | |
| 27 | c1 | ⊢ 1 | |
| 28 | 24 27 26 | co | ⊢ ( 𝑘 + 1 ) |
| 29 | 28 12 | cfv | ⊢ ( 𝑝 ‘ ( 𝑘 + 1 ) ) |
| 30 | 25 29 | wceq | ⊢ ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) |
| 31 | 24 5 | cfv | ⊢ ( 𝑓 ‘ 𝑘 ) |
| 32 | 31 8 | cfv | ⊢ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) |
| 33 | 25 | csn | ⊢ { ( 𝑝 ‘ 𝑘 ) } |
| 34 | 32 33 | wceq | ⊢ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } |
| 35 | 25 29 | cpr | ⊢ { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } |
| 36 | 35 32 | wss | ⊢ { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) |
| 37 | 30 34 36 | wif | ⊢ if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) |
| 38 | 37 21 23 | wral | ⊢ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) |
| 39 | 11 20 38 | w3a | ⊢ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) |
| 40 | 39 3 4 | copab | ⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } |
| 41 | 1 2 40 | cmpt | ⊢ ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } ) |
| 42 | 0 41 | wceq | ⊢ Walks = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } ) |