Graph walks and simple paths: pair-by-pair checks, length and the difference from trails

Goal and scope

Finite undirected loop-free simple graph G: V={0,1,2,3,4}, E={{0,1},{1,2},{2,3},{0,3},{1,3},{3,4}}. For the vertex sequences W₁=(0,1,2,3,4), W₂=(0,1,3,1,2), W₃=(0,2,3), W₄=(2,3,0,1,3,4), W₅=(4) and W₆=(1,1), decide whether each is a walk, its length, and whether it is a simple path; also prove that a simple path repeats no edge and that in this graph a simple path has length at most 4.

Works inside the MKO's scope: vertices are labeled 0 to n−1, and the complete undirected simple edge set and ordered vertex sequences are explicit (assumption a1); the empty sequence is not a walk and a single vertex is a simple path of length 0 (assumption a2). Trails appear only for contrast with simple paths; cycles, connected components and directed graphs are not treated, and the canonical MKO and its English edition are not changed.

Givens and symbols

• graph_basics
• finite_counting_basics
• quantifier_negation
• and_intro_elim
• numeric_evaluation

• G1 — V={0,1,2,3,4}; E={{0,1},{1,2},{2,3},{0,3},{1,3},{3,4}}, six edges in all; there are no other edges.
• G2 — The sequences to decide: W₁=(0,1,2,3,4), W₂=(0,1,3,1,2), W₃=(0,2,3), W₄=(2,3,0,1,3,4), W₅=(4), W₆=(1,1), and the empty sequence ().

• G=(V,E) — the given finite undirected simple graph
• \{p,q\} — an unordered pair of vertices; it can be an edge only if p≠q
• W=(v_i)_{i=0}^{k} — the vertex sequence v₀ to v_k, with k+1 entries
• k — the edge length of a walk (the number of consecutive pairs)
• W_1,W_2,W_3,W_4,W_5,W_6 — the six sequences to be decided
• n=|V|=5 — the number of vertices

Rules and sources

• graph_basics · prerequisite — (Simple undirected) graph: G=(V,E), where each edge is an unordered pair of distinct vertices; the degree of a vertex is the number of edges at it; handshake lemma Σ_v deg(v)=2|E|.
• finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• mko_walk_def · cited — Fix a finite undirected loop-free simple graph. A vertex sequence (v₀ to v_k) is a walk if every consecutive unordered pair is an edge; its edge length is k. A simple path is a walk without repeated vertices. A walk may repeat vertices or edges; cycles and trails have additional obligations. The empty sequence is not a walk; a singleton vertex is a length-zero simple path. · mko-graph-walk-simple-path
• trail_def · prerequisite — A trail is a walk with no repeated edge: for all 0≤i<j≤k−1, {v_i,v_{i+1}}≠{v_j,v_{j+1}}.
• unordered_pair_eq · prerequisite — Equality of unordered pairs: {p,q}={r,s} iff (p=r and q=s) or (p=s and q=r).
• inj_size_le · prerequisite — If there is an injective map from a finite set X to a finite set Y, then |X|≤|Y| (pigeonhole principle).
• L_path_trail · lemma — In a simple graph every simple path repeats no edge and is therefore a trail.

Main derivation

V=\{0,1,2,3,4\},\ E=\{\{0,1\},\{1,2\},\{2,3\},\{0,3\},\{1,3\},\{3,4\}\}

G\ \text{simple, loop-free};\ \sum_{v}\deg v=2+3+2+4+1=12=2|E|

W=(v_i)_{i=0}^{k}

W\ \text{walk}\iff\forall i\ (0\le i\le k-1):\ \{v_i,v_{i+1}\}\in E;\ \ \text{length}=k;\ \ \text{simple path}\iff\text{walk}\land(i\neq j\Rightarrow v_i\neq v_j)

W_1=(0,1,2,3,4)

\{0,1\},\{1,2\},\{2,3\},\{3,4\}\in E\ \Rightarrow\ W_1\ \text{walk}

W_1\ \text{has}\ 5\ \text{entries}

\operatorname{len}(W_1)=5-1=4

W_1\ \text{walk},\ 0,1,2,3,4\ \text{pairwise distinct}

W_1\ \text{simple path}

W_2=(0,1,3,1,2)

\{0,1\},\{1,3\},\{3,1\},\{1,2\}\in E\ \Rightarrow\ W_2\ \text{walk},\ \operatorname{len}(W_2)=4

v_1=1=v_3\ \text{in}\ W_2

W_2\ \text{walk but not a simple path}

W_3=(0,2,3)

\{0,2\}\notin E\ \Rightarrow\ W_3\ \text{not a walk}

W_4=(2,3,0,1,3,4)

\{2,3\},\{3,0\},\{0,1\},\{1,3\},\{3,4\}\in E,\ \text{pairwise distinct}\ \Rightarrow\ W_4\ \text{trail},\ \operatorname{len}(W_4)=5

v_1=3=v_4\ \text{in}\ W_4

W_4\ \text{trail but not a simple path}

W=(v_i)_{i=0}^{k}\ \text{simple path}

\{v_i,v_{i+1}\}\neq\{v_j,v_{j+1}\}\ \ (0\le i<j\le k-1),\ \text{so}\ W\ \text{is a trail}

W=(v_i)_{i=0}^{k}\ \text{simple path in}\ G,\ |V|=5

k+1\le 5,\ \text{so}\ \operatorname{len}(W)=k\le 4

W_5=(4),\ k=0

W_5\ \text{simple path of length}\ 0;\ \ ()\ \text{not a walk}

W_6=(1,1)

\{1,1\}\notin E\ \Rightarrow\ W_6\ \text{not a walk}

\text{S05},\ \text{S07},\ \text{S08},\ \text{S10},\ \text{S13},\ \text{S14}

W_1,W_5\ \text{simple paths};\ W_2\ \text{walk only};\ W_4\ \text{trail, not simple path};\ W_3,W_6,()\ \text{not walks}

Substeps and lemmas

\{v_i,v_{i+1}\}=\{v_j,v_{j+1}\},\ 0\le i<j\le k-1

v_i=v_j\ \lor\ v_i=v_{j+1}

v_i=v_j\ \lor\ v_i=v_{j+1},\ \ i<j<j+1

\bot,\ \text{hence no two edges of}\ W\ \text{coincide}

Reverse audits

• S15 · sufficient_goal_reduction · S05, S07, S08, S10, S11, S12, S13, S14, and_intro_elim — Goal G is the conjunction of all decisions and the two general facts; the sufficient condition H consists of the conclusions of the steps listed, H⇒G by conjunction introduction, and each part is proved forwards from the givens; G is never used as a premise.
• S14 · premise_audit · S01, graph_basics, quantifier_negation — It relies on edges of a simple graph being unordered pairs of distinct vertices; in a different model allowing loops, an actual loop at vertex 1 is still needed for W₆ to be a length-1 walk. Merely allowing loops does not force a changed conclusion. Even with that loop, repeated vertices keep W₆ from being a simple path. That model is outside this MKO's scope.
• S13 · premise_audit · mko_walk_def — The vacuous truth holds because no i satisfies 0≤i≤k−1=−1; the exclusion of the empty sequence is a protocol choice, not derived from the definition.
• S12 · premise_audit · inj_size_le, S02 — It needs pairwise distinct entries (injectivity); for a general walk it fails, since W₂ and W₄ repeat vertices. Length ≤4 is only necessary and does not imply being a simple path (N4, N5).
• S11.2 · premise_audit · S11.1, contradiction, case_analysis — The two cases cover every possibility from S11.1; the contradiction uses only the definition of a simple path.
• S11.1 · premise_audit · unordered_pair_eq, and_intro_elim — Only the first conjunct of each case is kept; no converse is claimed.
• S11 · premise_audit · L_path_trail, trail_def — Only simple path ⇒ trail is claimed; the converse is refuted by W₄.
• S10 · premise_audit · S09, quantifier_negation — One witness pair (i,j)=(1,4) suffices to deny pairwise distinct vertices; the length bound of S12 gives an independent cross-check.
• S09 · premise_audit · S02, trail_def, unordered_pair_eq — A trail needs the walk property plus no repeated edge; both are checked one by one here (N3 checks the length).
• S08 · premise_audit · G1, quantifier_negation — '{0,2}∉E' holds by the clause 'no other edges' in G1; with an incomplete edge set non-adjacency could not be decided, which is why assumption a1 requires the complete edge set.
• S07 · premise_audit · S06, quantifier_negation — Denying 'for all i≠j, v_i≠v_j' needs one witness pair (i,j)=(1,3).
• S06 · premise_audit · S02, unordered_pair_eq, and_intro_elim — Because the graph is undirected, {3,1}={1,3} (equality of unordered pairs); in a directed graph this step would need a separate check of direction.
• S05 · premise_audit · S03, mko_walk_def — A simple path needs two conditions: being a walk (S03) and having no repeated entry; distinct entries without the walk property are not enough (see S08).
• S04 · inverse_equivalence · mko_walk_def, numeric_evaluation — Backward: length 4 plus one gives 5 entries; both descriptions refer to the same sequence (N2).
• S03 · premise_audit · S02, G1, and_intro_elim — Every consecutive pair must be checked, not just the first or the last; this step checks all four.
• S02 · premise_audit · mko_walk_def, def_unfold — It only unfolds definitions and derives no new fact; each later decision returns to these three conditions.
• S01 · premise_audit · G1, graph_basics — It only confirms the setting and makes a consistency check (N1); the handshake equation cannot prove the edge list correct, only exclude some copying errors.

Error controls and negative controls

A list of vertices need not be a walk

One misconception named by the MKO is to treat any list of vertices as a walk. The three vertices of W₃=(0,2,3) are in V and distinct, yet {0,2} is not an edge, so W₃ is not a walk. The decision must check every consecutive pair (S03, S08), and the complete edge set is needed to decide non-adjacency.

Length counts edges, not vertices

W₁ has 5 vertices and length 4. W₂ has 5 entries but only 4 distinct vertices and 3 distinct edges, and its length is still 4: the length counts consecutive pairs (edges traversed, repetitions included), which is the number of entries minus one.

A trail need not be a simple path

W₄ repeats no edge but passes through vertex 3 twice. A simple path forbids repeated vertices; having no repeated edge is only the weaker trail condition. Lemma L_path_trail gives only the direction simple path ⇒ trail.

• The vertices of (0,2,3) are all in V and do not repeat, so it is a simple path → reject — {0,2}∉E, so it is not even a walk.
• W₁=(0,1,2,3,4) has 5 vertices, so its length is 5 → reject — The length is the number of consecutive pairs, 5−1=4.
• W₄ has no repeated edge, so it is a simple path → reject — Vertex 3 appears at indices 1 and 4; moreover its length 5 exceeds the simple-path bound 4.
• (1,1) is a walk of length 1 that stays at vertex 1 for one step → reject — {1,1} is not an unordered pair of distinct vertices and is not an edge of a loop-free simple graph.

Result and limitations

In G: W₁=(0,1,2,3,4) is a simple path of length 4; W₂=(0,1,3,1,2) is a walk of length 4 but not a simple path; W₃=(0,2,3) is not a walk because {0,2}∉E; W₄=(2,3,0,1,3,4) is a trail of length 5 but repeats vertex 3 and is not a simple path; W₅=(4) is a simple path of length 0; W₆=(1,1) and the empty sequence are not walks. Every simple path is a trail but not conversely; in this graph a simple path has length at most 4.

• This guide checks pairs against the complete edge list; for larger graphs the same decisions can be written as an algorithm, but its complexity is not analyzed here.
• Cycles and connected components are outside this guide's scope; trails are used only for contrast.

Verification and source binding

7 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 49f77d500fdd6a9edd41755d563203dc6463ebe4857c93350c07bbfd67d26ec3
• original source SHA-256: 658afc79124d38166f5b5ff1eb4fae1b1b76dccfe69d963b6d261be4216f8d9c
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)