P. 283 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28201-28300   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cwwlksnon 28201	Extend class notation with walks between two vertices (in a graph) of a fixed length as word over the set of vertices.
class WWalksNOn
Syntax	cwwspthsn 28202	Extend class notation with simple paths (in a graph) of a fixed length as word over the set of vertices.
class WSPathsN
Syntax	cwwspthsnon 28203	Extend class notation with simple paths between two vertices (in a graph) of a fixed length as word over the set of vertices.
class WSPathsNOn
Definition	df-wwlks 28204*	Define the set of all 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) p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlks 27975. 𝑤 = ∅ has to be excluded because a walk always consists of at least one vertex, see wlkn0 27997. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)
⊢ WWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))})
Definition	df-wwlksn 28205*	Define the set of all walks (in an undirected graph) of a fixed length n as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlks 27975. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)
⊢ WWalksN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (WWalks‘𝑔) ∣ (♯‘𝑤) = (𝑛 + 1)})
Definition	df-wwlksnon 28206*	Define the collection of walks of a fixed length with particular endpoints as word over the set of vertices. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 11-May-2021.)
⊢ WWalksNOn = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)}))
Definition	df-wspthsn 28207*	Define the collection of simple paths of a fixed length as word over the set of vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.)
⊢ WSPathsN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ∃𝑓 𝑓(SPaths‘𝑔)𝑤})
Definition	df-wspthsnon 28208*	Define the collection of simple paths of a fixed length with particular endpoints as word over the set of vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.)
⊢ WSPathsNOn = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑎(𝑛 WWalksNOn 𝑔)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤}))
Theorem	wwlks 28209*	The set of walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (WWalks‘𝐺) = {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸)}
Theorem	iswwlks 28210*	A word over the set of vertices representing a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑊 ∈ (WWalks‘𝐺) ↔ (𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸))
Theorem	wwlksn 28211*	The set of walks (in an undirected graph) of a fixed length as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)
⊢ (𝑁 ∈ ℕ0 → (𝑁 WWalksN 𝐺) = {𝑤 ∈ (WWalks‘𝐺) ∣ (♯‘𝑤) = (𝑁 + 1)})
Theorem	iswwlksn 28212	A word over the set of vertices representing a walk of a fixed length (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)
⊢ (𝑁 ∈ ℕ0 → (𝑊 ∈ (𝑁 WWalksN 𝐺) ↔ (𝑊 ∈ (WWalks‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))))
Theorem	wwlksnprcl 28213	Derivation of the length of a word 𝑊 whose concatenation with a singleton word represents a walk of a fixed length 𝑁 (a partial reverse closure theorem). (Contributed by AV, 4-Mar-2022.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑁 WWalksN 𝐺) → (♯‘𝑊) = 𝑁))
Theorem	iswwlksnx 28214*	Properties of a word to represent a walk of a fixed length, definition of WWalks expanded. (Contributed by AV, 28-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑊 ∈ (𝑁 WWalksN 𝐺) ↔ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ (♯‘𝑊) = (𝑁 + 1))))
Theorem	wwlkbp 28215	Basic properties of a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 9-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑊 ∈ (WWalks‘𝐺) → (𝐺 ∈ V ∧ 𝑊 ∈ Word 𝑉))
Theorem	wwlknbp 28216	Basic properties of a walk of a fixed length (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 16-Jul-2018.) (Revised by AV, 9-Apr-2021.) (Proof shortened by AV, 20-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉))
Theorem	wwlknp 28217*	Properties of a set being a walk of length n (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 9-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸))
Theorem	wwlknbp1 28218	Other basic properties of a walk of a fixed length as word. (Contributed by AV, 8-Mar-2022.)
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)))
Theorem	wwlknvtx 28219*	The symbols of a word 𝑊 representing a walk of a fixed length 𝑁 are vertices. (Contributed by AV, 16-Mar-2022.)
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ∀𝑖 ∈ (0...𝑁)(𝑊‘𝑖) ∈ (Vtx‘𝐺))
Theorem	wwlknllvtx 28220	If a word 𝑊 represents a walk of a fixed length 𝑁, then the first and the last symbol of the word is a vertex. (Contributed by AV, 14-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑊‘0) ∈ 𝑉 ∧ (𝑊‘𝑁) ∈ 𝑉))
Theorem	wwlknlsw 28221	If a word represents a walk of a fixed length, then the last symbol of the word is the endvertex of the walk. (Contributed by AV, 8-Mar-2022.)
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊‘𝑁) = (lastS‘𝑊))
Theorem	wspthsn 28222*	The set of simple paths of a fixed length as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.)
⊢ (𝑁 WSPathsN 𝐺) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ∃𝑓 𝑓(SPaths‘𝐺)𝑤}
Theorem	iswspthn 28223*	An element of the set of simple paths of a fixed length as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.)
⊢ (𝑊 ∈ (𝑁 WSPathsN 𝐺) ↔ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ∃𝑓 𝑓(SPaths‘𝐺)𝑊))
Theorem	wspthnp 28224*	Properties of a set being a simple path of a fixed length as word. (Contributed by AV, 18-May-2021.)
⊢ (𝑊 ∈ (𝑁 WSPathsN 𝐺) → ((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ∃𝑓 𝑓(SPaths‘𝐺)𝑊))
Theorem	wwlksnon 28225*	The set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 11-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈) → (𝑁 WWalksNOn 𝐺) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏)}))
Theorem	wspthsnon 28226*	The set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈) → (𝑁 WSPathsNOn 𝐺) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑤 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑤}))
Theorem	iswwlksnon 28227*	The set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 14-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)}
Theorem	wwlksnon0 28228	Sufficient conditions for a set of walks of a fixed length between two vertices to be empty. (Contributed by AV, 15-May-2021.) (Proof shortened by AV, 21-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (¬ ((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = ∅)
Theorem	wwlksonvtx 28229	If a word 𝑊 represents a walk of length 2 on two classes 𝐴 and 𝐶, these classes are vertices. (Contributed by AV, 14-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑊 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐶) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))
Theorem	iswspthsnon 28230*	The set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 14-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) = {𝑤 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤}
Theorem	wwlknon 28231	An element of the set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 14-Mar-2022.)
⊢ (𝑊 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ↔ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝐴 ∧ (𝑊‘𝑁) = 𝐵))
Theorem	wspthnon 28232*	An element of the set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 15-Mar-2022.)
⊢ (𝑊 ∈ (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) ↔ (𝑊 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑊))
Theorem	wspthnonp 28233*	Properties of a set being a simple path of a fixed length between two vertices as word. (Contributed by AV, 14-May-2021.) (Proof shortened by AV, 15-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑊 ∈ (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) → ((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝑊 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑊)))
Theorem	wspthneq1eq2 28234	Two simple paths with identical sequences of vertices start and end at the same vertices. (Contributed by AV, 14-May-2021.)
⊢ ((𝑃 ∈ (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) ∧ 𝑃 ∈ (𝐶(𝑁 WSPathsNOn 𝐺)𝐷)) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	wwlksn0s 28235*	The set of all walks as words of length 0 is the set of all words of length 1 over the vertices. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 12-Apr-2021.)
⊢ (0 WWalksN 𝐺) = {𝑤 ∈ Word (Vtx‘𝐺) ∣ (♯‘𝑤) = 1}
Theorem	wwlkssswrd 28236	Walks (represented by words) are words. (Contributed by Alexander van der Vekens, 17-Jul-2018.) (Revised by AV, 9-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (WWalks‘𝐺) ⊆ Word 𝑉
Theorem	wwlksn0 28237*	A walk of length 0 is represented by a singleton word. (Contributed by Alexander van der Vekens, 20-Jul-2018.) (Revised by AV, 9-Apr-2021.) (Proof shortened by AV, 21-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑊 ∈ (0 WWalksN 𝐺) → ∃𝑣 ∈ 𝑉 𝑊 = ⟨“𝑣”⟩)
Theorem	0enwwlksnge1 28238	In graphs without edges, there are no walks of length greater than 0. (Contributed by Alexander van der Vekens, 26-Jul-2018.) (Revised by AV, 7-May-2021.)
⊢ (((Edg‘𝐺) = ∅ ∧ 𝑁 ∈ ℕ) → (𝑁 WWalksN 𝐺) = ∅)
Theorem	wwlkswwlksn 28239	A walk of a fixed length as word is a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 17-Jul-2018.) (Revised by AV, 12-Apr-2021.)
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝑊 ∈ (WWalks‘𝐺))
Theorem	wwlkssswwlksn 28240	The walks of a fixed length as words are walks (in an undirected graph) as words. (Contributed by Alexander van der Vekens, 17-Jul-2018.) (Revised by AV, 12-Apr-2021.)
⊢ (𝑁 WWalksN 𝐺) ⊆ (WWalks‘𝐺)
Theorem	wlkiswwlks1 28241	The sequence of vertices in a walk is a walk as word in a pseudograph. (Contributed by Alexander van der Vekens, 20-Jul-2018.) (Revised by AV, 9-Apr-2021.)
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 → 𝑃 ∈ (WWalks‘𝐺)))
Theorem	wlklnwwlkln1 28242	The sequence of vertices in a walk of length 𝑁 is a walk as word of length 𝑁 in a pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.)
⊢ (𝐺 ∈ UPGraph → ((𝐹(Walks‘𝐺)𝑃 ∧ (♯‘𝐹) = 𝑁) → 𝑃 ∈ (𝑁 WWalksN 𝐺)))
Theorem	wlkiswwlks2lem1 28243*	Lemma 1 for wlkiswwlks2 28249. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))    ⇒   ⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (♯‘𝐹) = ((♯‘𝑃) − 1))
Theorem	wlkiswwlks2lem2 28244*	Lemma 2 for wlkiswwlks2 28249. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))    ⇒   ⊢ (((♯‘𝑃) ∈ ℕ0 ∧ 𝐼 ∈ (0..^((♯‘𝑃) − 1))) → (𝐹‘𝐼) = (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}))
Theorem	wlkiswwlks2lem3 28245*	Lemma 3 for wlkiswwlks2 28249. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))    ⇒   ⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 𝑃:(0...(♯‘𝐹))⟶𝑉)
Theorem	wlkiswwlks2lem4 28246*	Lemma 4 for wlkiswwlks2 28249. (Contributed by Alexander van der Vekens, 20-Jul-2018.) (Revised by AV, 10-Apr-2021.)
⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))
Theorem	wlkiswwlks2lem5 28247*	Lemma 5 for wlkiswwlks2 28249. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.)
⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → 𝐹 ∈ Word dom 𝐸))
Theorem	wlkiswwlks2lem6 28248*	Lemma 6 for wlkiswwlks2 28249. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.)
⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))    &   ⊢ 𝐸 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})))
Theorem	wlkiswwlks2 28249*	A walk as word corresponds to the sequence of vertices in a walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.)
⊢ (𝐺 ∈ USPGraph → (𝑃 ∈ (WWalks‘𝐺) → ∃𝑓 𝑓(Walks‘𝐺)𝑃))
Theorem	wlkiswwlks 28250*	A walk as word corresponds to a walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.)
⊢ (𝐺 ∈ USPGraph → (∃𝑓 𝑓(Walks‘𝐺)𝑃 ↔ 𝑃 ∈ (WWalks‘𝐺)))
Theorem	wlkiswwlksupgr2 28251*	A walk as word corresponds to the sequence of vertices in a walk in a pseudograph. This variant of wlkiswwlks2 28249 does not require 𝐺 to be a simple pseudograph, but it requires the Axiom of Choice (ac6 10245) for its proof. Notice that only the existence of a function 𝑓 can be proven, but, in general, it cannot be "constructed" (as in wlkiswwlks2 28249). (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.)
⊢ (𝐺 ∈ UPGraph → (𝑃 ∈ (WWalks‘𝐺) → ∃𝑓 𝑓(Walks‘𝐺)𝑃))
Theorem	wlkiswwlkupgr 28252*	A walk as word corresponds to a walk in a pseudograph. This variant of wlkiswwlks 28250 does not require 𝐺 to be a simple pseudograph, but it requires (indirectly) the Axiom of Choice for its proof. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.)
⊢ (𝐺 ∈ UPGraph → (∃𝑓 𝑓(Walks‘𝐺)𝑃 ↔ 𝑃 ∈ (WWalks‘𝐺)))
Theorem	wlkswwlksf1o 28253*	The mapping of (ordinary) walks to their sequences of vertices is a bijection in a simple pseudograph. (Contributed by AV, 6-May-2021.)
⊢ 𝐹 = (𝑤 ∈ (Walks‘𝐺) ↦ (2nd ‘𝑤))    ⇒   ⊢ (𝐺 ∈ USPGraph → 𝐹:(Walks‘𝐺)–1-1-onto→(WWalks‘𝐺))
Theorem	wlkswwlksen 28254	The set of walks as words and the set of (ordinary) walks are equinumerous in a simple pseudograph. (Contributed by AV, 6-May-2021.) (Revised by AV, 5-Aug-2022.)
⊢ (𝐺 ∈ USPGraph → (Walks‘𝐺) ≈ (WWalks‘𝐺))
Theorem	wwlksm1edg 28255	Removing the trailing edge from a walk (as word) with at least one edge results in a walk. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 19-Apr-2021.) (Revised by AV, 26-Oct-2022.)
⊢ ((𝑊 ∈ (WWalks‘𝐺) ∧ 2 ≤ (♯‘𝑊)) → (𝑊 prefix ((♯‘𝑊) − 1)) ∈ (WWalks‘𝐺))
Theorem	wlklnwwlkln2lem 28256*	Lemma for wlklnwwlkln2 28257 and wlklnwwlklnupgr2 28259. Formerly part of proof for wlklnwwlkln2 28257. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.)
⊢ (𝜑 → (𝑃 ∈ (WWalks‘𝐺) → ∃𝑓 𝑓(Walks‘𝐺)𝑃))    ⇒   ⊢ (𝜑 → (𝑃 ∈ (𝑁 WWalksN 𝐺) → ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁)))
Theorem	wlklnwwlkln2 28257*	A walk of length 𝑁 as word corresponds to the sequence of vertices in a walk of length 𝑁 in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.)
⊢ (𝐺 ∈ USPGraph → (𝑃 ∈ (𝑁 WWalksN 𝐺) → ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁)))
Theorem	wlklnwwlkn 28258*	A walk of length 𝑁 as word corresponds to a walk with length 𝑁 in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.)
⊢ (𝐺 ∈ USPGraph → (∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁) ↔ 𝑃 ∈ (𝑁 WWalksN 𝐺)))
Theorem	wlklnwwlklnupgr2 28259*	A walk of length 𝑁 as word corresponds to the sequence of vertices in a walk of length 𝑁 in a pseudograph. This variant of wlklnwwlkln2 28257 does not require 𝐺 to be a simple pseudograph, but it requires (indirectly) the Axiom of Choice. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.)
⊢ (𝐺 ∈ UPGraph → (𝑃 ∈ (𝑁 WWalksN 𝐺) → ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁)))
Theorem	wlklnwwlknupgr 28260*	A walk of length 𝑁 as word corresponds to a walk with length 𝑁 in a pseudograph. This variant of wlkiswwlks 28250 does not require 𝐺 to be a simple pseudograph, but it requires (indirectly) the Axiom of Choice for its proof. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.)
⊢ (𝐺 ∈ UPGraph → (∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁) ↔ 𝑃 ∈ (𝑁 WWalksN 𝐺)))
Theorem	wlknewwlksn 28261	If a walk in a pseudograph has length 𝑁, then the sequence of the vertices of the walk is a word representing the walk as word of length 𝑁. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 11-Apr-2021.)
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧ (♯‘(1st ‘𝑊)) = 𝑁)) → (2nd ‘𝑊) ∈ (𝑁 WWalksN 𝐺))
Theorem	wlknwwlksnbij 28262*	The mapping (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length in a simple pseudograph. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 5-Aug-2022.)
⊢ 𝑇 = {𝑝 ∈ (Walks‘𝐺) ∣ (♯‘(1st ‘𝑝)) = 𝑁}    &   ⊢ 𝑊 = (𝑁 WWalksN 𝐺)    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡))    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–1-1-onto→𝑊)
Theorem	wlknwwlksnen 28263*	In a simple pseudograph, the set of walks of a fixed length and the set of walks represented by words are equinumerous. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 5-Aug-2022.)
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0) → {𝑝 ∈ (Walks‘𝐺) ∣ (♯‘(1st ‘𝑝)) = 𝑁} ≈ (𝑁 WWalksN 𝐺))
Theorem	wlknwwlksneqs 28264*	The set of walks of a fixed length and the set of walks represented by words have the same size. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 15-Apr-2021.)
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0) → (♯‘{𝑝 ∈ (Walks‘𝐺) ∣ (♯‘(1st ‘𝑝)) = 𝑁}) = (♯‘(𝑁 WWalksN 𝐺)))
Theorem	wwlkseq 28265*	Equality of two walks (as words). (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.)
⊢ ((𝑊 ∈ (WWalks‘𝐺) ∧ 𝑇 ∈ (WWalks‘𝐺)) → (𝑊 = 𝑇 ↔ ((♯‘𝑊) = (♯‘𝑇) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑇‘𝑖))))
Theorem	wwlksnred 28266	Reduction of a walk (as word) by removing the trailing edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.) (Revised by AV, 26-Oct-2022.)
⊢ (𝑁 ∈ ℕ0 → (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) → (𝑊 prefix (𝑁 + 1)) ∈ (𝑁 WWalksN 𝐺)))
Theorem	wwlksnext 28267	Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺))
Theorem	wwlksnextbi 28268	Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by AV, 16-Apr-2021.) (Proof shortened by AV, 27-Oct-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ 𝑊 = (𝑇 ++ ⟨“𝑆”⟩) ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ 𝑇 ∈ (𝑁 WWalksN 𝐺)))
Theorem	wwlksnredwwlkn 28269*	For each walk (as word) of length at least 1 there is a shorter walk (as word). (Contributed by Alexander van der Vekens, 22-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 26-Oct-2022.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) → ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑊 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑊)} ∈ 𝐸)))
Theorem	wwlksnredwwlkn0 28270*	For each walk (as word) of length at least 1 there is a shorter walk (as word) starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 26-Oct-2022.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺)) → ((𝑊‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑊 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑊)} ∈ 𝐸)))
Theorem	wwlksnextwrd 28271*	Lemma for wwlksnextbij 28276. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 27-Oct-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}    ⇒   ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝐷 = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)})
Theorem	wwlksnextfun 28272*	Lemma for wwlksnextbij 28276. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 27-Oct-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (lastS‘𝑡))    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝐷⟶𝑅)
Theorem	wwlksnextinj 28273*	Lemma for wwlksnextbij 28276. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 27-Oct-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (lastS‘𝑡))    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝐷–1-1→𝑅)
Theorem	wwlksnextsurj 28274*	Lemma for wwlksnextbij 28276. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 27-Oct-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (lastS‘𝑡))    ⇒   ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝐹:𝐷–onto→𝑅)
Theorem	wwlksnextbij0 28275*	Lemma for wwlksnextbij 28276. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (lastS‘𝑡))    ⇒   ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝐹:𝐷–1-1-onto→𝑅)
Theorem	wwlksnextbij 28276*	There is a bijection between the extensions of a walk (as word) by an edge and the set of vertices being connected to the trailing vertex of the walk. (Contributed by Alexander van der Vekens, 21-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 27-Oct-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ∃𝑓 𝑓:{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸})
Theorem	wwlksnexthasheq 28277*	The number of the extensions of a walk (as word) by an edge equals the number of vertices being connected to the trailing vertex of the walk. (Contributed by Alexander van der Vekens, 23-Aug-2018.) (Revised by AV, 19-Apr-2021.) (Revised by AV, 27-Oct-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}) = (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸}))
Theorem	disjxwwlksn 28278*	Sets of walks (as words) extended by an edge are disjunct if each set contains extensions of distinct walks. (Contributed by Alexander van der Vekens, 29-Jul-2018.) (Revised by AV, 19-Apr-2021.) (Revised by AV, 27-Oct-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ Disj 𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ ((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)}
Theorem	wwlksnndef 28279	Conditions for WWalksN not being defined. (Contributed by Alexander van der Vekens, 30-Jul-2018.) (Revised by AV, 19-Apr-2021.)
⊢ ((𝐺 ∉ V ∨ 𝑁 ∉ ℕ0) → (𝑁 WWalksN 𝐺) = ∅)
Theorem	wwlksnfi 28280	The number of walks represented by words of fixed length is finite if the number of vertices is finite (in the graph). (Contributed by Alexander van der Vekens, 30-Jul-2018.) (Revised by AV, 19-Apr-2021.) (Proof shortened by JJ, 18-Nov-2022.)
⊢ ((Vtx‘𝐺) ∈ Fin → (𝑁 WWalksN 𝐺) ∈ Fin)
Theorem	wlksnfi 28281*	The number of walks of fixed length is finite if the number of vertices is finite (in the graph). (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 20-Apr-2021.)
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ0) → {𝑝 ∈ (Walks‘𝐺) ∣ (♯‘(1st ‘𝑝)) = 𝑁} ∈ Fin)
Theorem	wlksnwwlknvbij 28282*	There is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length and starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 5-Aug-2022.)
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0) → ∃𝑓 𝑓:{𝑝 ∈ (Walks‘𝐺) ∣ ((♯‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋})
Theorem	wwlksnextproplem1 28283	Lemma 1 for wwlksnextprop 28286. (Contributed by Alexander van der Vekens, 31-Jul-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 29-Oct-2022.)
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑊 prefix (𝑁 + 1))‘0) = (𝑊‘0))
Theorem	wwlksnextproplem2 28284	Lemma 2 for wwlksnextprop 28286. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 29-Oct-2022.)
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → {(lastS‘(𝑊 prefix (𝑁 + 1))), (lastS‘𝑊)} ∈ 𝐸)
Theorem	wwlksnextproplem3 28285*	Lemma 3 for wwlksnextprop 28286. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 29-Oct-2022.)
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑌 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ (𝑊‘0) = 𝑃 ∧ 𝑁 ∈ ℕ0) → (𝑊 prefix (𝑁 + 1)) ∈ 𝑌)
Theorem	wwlksnextprop 28286*	Adding additional properties to the set of walks (as words) of a fixed length starting at a fixed vertex. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 29-Oct-2022.)
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑌 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}    ⇒   ⊢ (𝑁 ∈ ℕ0 → {𝑥 ∈ 𝑋 ∣ (𝑥‘0) = 𝑃} = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 ((𝑥 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)})
Theorem	disjxwwlkn 28287*	Sets of walks (as words) extended by an edge are disjunct if each set contains extensions of distinct walks. (Contributed by Alexander van der Vekens, 21-Aug-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 26-Oct-2022.)
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑌 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}    ⇒   ⊢ Disj 𝑦 ∈ 𝑌 {𝑥 ∈ 𝑋 ∣ ((𝑥 prefix 𝑀) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)}
Theorem	hashwwlksnext 28288*	Number of walks (as words) extended by an edge as a sum over the prefixes. (Contributed by Alexander van der Vekens, 21-Aug-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 26-Oct-2022.)
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑌 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}    ⇒   ⊢ ((Vtx‘𝐺) ∈ Fin → (♯‘{𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 ((𝑥 prefix 𝑀) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)}) = Σ𝑦 ∈ 𝑌 (♯‘{𝑥 ∈ 𝑋 ∣ ((𝑥 prefix 𝑀) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)}))
Theorem	wwlksnwwlksnon 28289*	A walk of fixed length is a walk of fixed length between two vertices. (Contributed by Alexander van der Vekens, 21-Feb-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 13-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏))
Theorem	wspthsnwspthsnon 28290*	A simple path of fixed length is a simple path of fixed length between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-May-2021.) (Revised by AV, 13-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑊 ∈ (𝑁 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑊 ∈ (𝑎(𝑁 WSPathsNOn 𝐺)𝑏))
Theorem	wspthsnonn0vne 28291	If the set of simple paths of length at least 1 between two vertices is not empty, the two vertices must be different. (Contributed by Alexander van der Vekens, 3-Mar-2018.) (Revised by AV, 16-May-2021.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑋(𝑁 WSPathsNOn 𝐺)𝑌) ≠ ∅) → 𝑋 ≠ 𝑌)
Theorem	wspthsswwlkn 28292	The set of simple paths of a fixed length between two vertices is a subset of the set of walks of the fixed length. (Contributed by AV, 18-May-2021.)
⊢ (𝑁 WSPathsN 𝐺) ⊆ (𝑁 WWalksN 𝐺)
Theorem	wspthnfi 28293	In a finite graph, the set of simple paths of a fixed length is finite. (Contributed by Alexander van der Vekens, 4-Mar-2018.) (Revised by AV, 18-May-2021.)
⊢ ((Vtx‘𝐺) ∈ Fin → (𝑁 WSPathsN 𝐺) ∈ Fin)
Theorem	wwlksnonfi 28294	In a finite graph, the set of walks of a fixed length between two vertices is finite. (Contributed by Alexander van der Vekens, 4-Mar-2018.) (Revised by AV, 15-May-2021.) (Proof shortened by AV, 15-Mar-2022.)
⊢ ((Vtx‘𝐺) ∈ Fin → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∈ Fin)
Theorem	wspthsswwlknon 28295	The set of simple paths of a fixed length between two vertices is a subset of the set of walks of the fixed length between the two vertices. (Contributed by AV, 15-May-2021.)
⊢ (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) ⊆ (𝐴(𝑁 WWalksNOn 𝐺)𝐵)
Theorem	wspthnonfi 28296	In a finite graph, the set of simple paths of a fixed length between two vertices is finite. (Contributed by Alexander van der Vekens, 4-Mar-2018.) (Revised by AV, 15-May-2021.)
⊢ ((Vtx‘𝐺) ∈ Fin → (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) ∈ Fin)
Theorem	wspniunwspnon 28297*	The set of nonempty simple paths of fixed length is the double union of the simple paths of the fixed length between different vertices. (Contributed by Alexander van der Vekens, 3-Mar-2018.) (Revised by AV, 16-May-2021.) (Proof shortened by AV, 15-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐺 ∈ 𝑈) → (𝑁 WSPathsN 𝐺) = ∪ 𝑥 ∈ 𝑉 ∪ 𝑦 ∈ (𝑉 ∖ {𝑥})(𝑥(𝑁 WSPathsNOn 𝐺)𝑦))
Theorem	wspn0 28298	If there are no vertices, then there are no simple paths (of any length), too. (Contributed by Alexander van der Vekens, 11-Mar-2018.) (Revised by AV, 16-May-2021.) (Proof shortened by AV, 13-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑉 = ∅ → (𝑁 WSPathsN 𝐺) = ∅)
16.3.8  Walks/paths of length 2 (as length 3 strings)
Theorem	2wlkdlem1 28299	Lemma 1 for 2wlkd 28310. (Contributed by AV, 14-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾”⟩    ⇒   ⊢ (♯‘𝑃) = ((♯‘𝐹) + 1)
Theorem	2wlkdlem2 28300	Lemma 2 for 2wlkd 28310. (Contributed by AV, 14-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾”⟩    ⇒   ⊢ (0..^(♯‘𝐹)) = {0, 1}