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

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-graph-walk-simple-path/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-graph-walk-simple-path-01 · production-20261019-adopted-96



## 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

S01 · definitionBefore

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

After

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

Conditions: none

Rule: graph_basics · Uses: G1, graph_basics

Leaf basis: graph_basics + numeric_evaluation

First confirm that the data form the finite undirected loop-free simple graph the MKO requires: each edge is an unordered pair of two distinct vertices and no edge is listed twice. The degrees are deg0=2, deg1=3, deg2=2, deg3=4, deg4=1, summing to 12=2·6, in agreement with the handshake lemma, which checks that the edge list was copied consistently.



S02 · definitionBefore

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

After

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)

Conditions: k\ge 0

Rule: mko_walk_def · Uses: mko_walk_def

Leaf basis: mko_walk_def + def_unfold

Unfold the MKO's three definitions. A walk requires every consecutive unordered pair to be an edge; the length k is the number of consecutive pairs, that is the number of entries minus one; a simple path additionally requires all entries to be distinct. A sequence has at least one entry (k≥0); the empty sequence is excluded by the protocol.



S03 · impliesBefore

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

After

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

Conditions: none

Rule: and_intro_elim · Uses: S02, G1, G2

Leaf basis: and_intro_elim + mko_walk_def

W₁ has four consecutive pairs: {0,1}, {1,2}, {2,3}, {3,4}. Each is found in E. All four conditions hold, so by conjunction introduction W₁ is a walk.



S04 · equivalentBefore

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

After

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

Conditions: none

Rule: mko_walk_def · Uses: S02, S03

Leaf basis: mko_walk_def + numeric_evaluation

The length is the number of edges (consecutive pairs), not the number of vertices: a sequence of 5 entries has 4 consecutive pairs, so the length is 4.



S05 · impliesBefore

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

After

W_1\ \text{simple path}

Conditions: none

Rule: mko_walk_def · Uses: S03, S02, G2

Leaf basis: mko_walk_def + and_intro_elim

The five entries 0, 1, 2, 3, 4 of W₁ are pairwise distinct; together with the walk property of S03, W₁ is by definition a simple path of length 4.



S06 · impliesBefore

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

After

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

Conditions: none

Rule: and_intro_elim · Uses: S02, G1, G2

Leaf basis: and_intro_elim + unordered_pair_eq + mko_walk_def

The four consecutive pairs of W₂ are {0,1}, {1,3}, {3,1}, {1,2}. The unordered pair {3,1} is the same edge as {1,3}, which is in E. All four are edges, so W₂ is a walk; it has 5 entries and length 4.



S07 · impliesBefore

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

After

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

Conditions: none

Rule: quantifier_negation · Uses: S06, S02

Leaf basis: quantifier_negation + mko_walk_def

The entries at indices 1 and 3 of W₂ are both 1 (i=1≠3=j), so 'entries pairwise distinct' fails and W₂ is not a simple path. It is still a walk: the MKO says a walk may repeat vertices and edges (here the edge {1,3} is used twice).



S08 · impliesBefore

W_3=(0,2,3)

After

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

Conditions: none

Rule: quantifier_negation · Uses: S02, G1, G2

Leaf basis: quantifier_negation + mko_walk_def

The first consecutive pair {0,2} is not in E (the only edges of E containing 0 are {0,1} and {0,3}). A walk requires every pair to be an edge, so one failing pair refutes it. Although 0, 2, 3 are distinct vertices, W₃ is not a walk and hence not a simple path.



S09 · impliesBefore

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

After

\{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

Conditions: none

Rule: trail_def · Uses: S02, G1, G2, trail_def

Leaf basis: trail_def + and_intro_elim + unordered_pair_eq

The five consecutive pairs {2,3}, {3,0}, {0,1}, {1,3}, {3,4} of W₄ are all in E, so W₄ is a walk; it has 6 entries and length 5. These five edges are pairwise different (compare the unordered pairs one by one), so W₄ repeats no edge and is a trail.



S10 · impliesBefore

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

After

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

Conditions: none

Rule: quantifier_negation · Uses: S09, S02

Leaf basis: quantifier_negation + mko_walk_def

The entries at indices 1 and 4 of W₄ are both vertex 3, so W₄ is not a simple path, even though it repeats no edge. This is exactly the MKO's warning: a trail without repeated edges must not be confused with a simple path.



S11 · impliesBefore

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

After

\{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}

Conditions: none

Rule: L_path_trail · Uses: S02, trail_def

Leaf basis: contradiction + unordered_pair_eq + trail_def

The relation in the other direction: every simple path is a trail (Lemma L_path_trail). The proof is in sub-steps S11.1 and S11.2: if two edges were the same, two different positions would carry the same vertex, contradicting the simple-path property. So simple paths are stricter than trails, and S10 shows the converse fails.



S12 · impliesBefore

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

After

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

Conditions: none

Rule: inj_size_le · Uses: S02, G1, inj_size_le

Leaf basis: inj_size_le + finite_counting_basics

The k+1 entries of a simple path are pairwise distinct, so i↦v_i is an injective map from {i∈ℤ:0≤i≤k} (k+1 elements) into V (5 elements); by the pigeonhole principle k+1≤5, so the length is at most 4. W₁ has length exactly 4 and attains the bound. W₄ has length 5>4, so the bound alone also shows it cannot be a simple path, in agreement with S10.



S13 · impliesBefore

W_5=(4),\ k=0

After

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

Conditions: none

Rule: mko_walk_def · Uses: S02, G2

Leaf basis: mko_walk_def + forall_intro

W₅ has one entry and no consecutive pair, so 'every consecutive pair is an edge' holds vacuously: it is a walk of length 1−1=0, and its single entry cannot repeat, so it is a simple path. By the MKO's protocol (assumption a2), the empty sequence () is not a walk and has no length.



S14 · impliesBefore

W_6=(1,1)

After

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

Conditions: none

Rule: graph_basics · Uses: S01, S02, G2

Leaf basis: graph_basics + quantifier_negation

The only consecutive pair is {1,1}, which contains a single vertex and is not an unordered pair of two distinct vertices; the graph has no loops (S01), so it is not an edge. W₆ is not a walk, and 'staying in place' cannot count as a walk of length 1.



S15 · impliesBefore

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

After

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}

Conditions: none

Rule: and_intro_elim · Uses: S05, S07, S08, S10, S11, S12, S13, S14

Leaf basis: and_intro_elim

Summary: W₁ is a simple path of length 4; W₂ is a walk of length 4 that repeats a vertex and an edge; W₃ is not a walk; W₄ is a trail of length 5 but not a simple path; W₅ is a simple path of length 0; W₆ and the empty sequence are not walks. Also proved: every simple path is a trail, and in this graph a simple path has length at most 4.







## Substeps and lemmas

S11.1 · impliesBefore

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

After

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

Conditions: i<j

Rule: unordered_pair_eq · Uses: unordered_pair_eq

Leaf basis: unordered_pair_eq + and_intro_elim

For a proof by contradiction, suppose some i<j makes the two edges equal. By equality of unordered pairs, (v_i=v_j and v_{i+1}=v_{j+1}) or (v_i=v_{j+1} and v_{i+1}=v_j); either case gives at least v_i=v_j or v_i=v_{j+1}.



S11.2 · impliesBefore

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

After

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

Conditions: none

Rule: contradiction · Uses: S11.1, S02

Leaf basis: contradiction + case_analysis + mko_walk_def

Since i<j<j+1, the positions i and j, and i and j+1, are different; a simple path has different vertices at different positions, so both cases are contradictory (proof by cases). The assumption fails: no two edges coincide. S11.1 and S11.2 together prove Lemma L_path_trail.







## 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 walkOne 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 verticesW₁ 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 pathW₄ 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-graph-walk-simple-path-01.json)