# 圖的 walk 與 simple path：逐對核對、長度與 trail 的區別

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-graph-walk-simple-path/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

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



## 目標與範圍

有限無向無 loop 簡單圖 G：V={0,1,2,3,4}，E={{0,1},{1,2},{2,3},{0,3},{1,3},{3,4}}。對頂點序列 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) 逐一判定是否為 walk、長度為何、是否為 simple path；並證明 simple path 不重複邊，以及本圖中 simple path 的長度至多為 4。

在 MKO 的範圍內工作：頂點標為 0 到 n−1，完整的無向簡單邊集合與有序頂點序列都明示（假設 a1）；空序列不算 walk，單一頂點是長度 0 的 simple path（假設 a2）。trail 只用來對照 simple path；不處理 cycle、連通分量或有向圖，不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- 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}}，共 6 條邊；除此之外沒有其他邊。
- G2 — 待判定的序列：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)，以及空序列 ()。


- G=(V,E) — 給定的有限無向簡單圖
- \{p,q\} — 無序頂點對；p≠q 時才可能是邊
- W=(v_i)_{i=0}^{k} — 頂點序列 v₀ 到 v_k，共 k+1 項
- k — walk 的 edge length（連續對的個數）
- W_1,W_2,W_3,W_4,W_5,W_6 — 六個待判定的序列
- n=|V|=5 — 頂點數





## 規則與來源


- graph_basics · prerequisite — （簡單無向）圖：G=(V,E)，E 中每條邊是 V 中兩個相異頂點的無序對；頂點度數是與它相連的邊數；握手引理 Σ_v deg(v)=2|E|。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- mko_walk_def · cited — 固定有限無向無 loop 簡單圖。頂點序列 (v₀ 到 v_k) 為 walk，若每個連續無序對都是邊；其 edge length 為 k。simple path 是頂點不重複的 walk。walk 可重複頂點或邊，cycle 與 trail 另有額外責任。空序列不作 walk；單頂點序列是長度 0 的 simple path。 · mko-graph-walk-simple-path
- trail_def · prerequisite — trail 是不重複邊的 walk：對所有 0≤i<j≤k−1，{v_i,v_{i+1}}≠{v_j,v_{j+1}}。
- unordered_pair_eq · prerequisite — 無序對相等：{p,q}={r,s} 當且僅當 (p=r 且 q=s) 或 (p=s 且 q=r)。
- inj_size_le · prerequisite — 若有限集合 X 到有限集合 Y 有單射，則 |X|≤|Y|（鴿籠原理）。
- L_path_trail · lemma — 在簡單圖中，每個 simple path 都不重複邊，因此是 trail。





## 逐步主鏈

S01 · definition操作前

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|

條件：無

規則：graph_basics · 依賴：G1, graph_basics

葉節點依據：graph_basics + numeric_evaluation

先確認給定資料是 MKO 所要求的有限無向無 loop 簡單圖：每條邊是兩個相異頂點的無序對，清單中沒有重複的邊。度數為 deg0=2、deg1=3、deg2=2、deg3=4、deg4=1，和為 12=2·6，與握手引理一致，作為邊清單抄寫無誤的核對。



S02 · definition操作前

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)

條件：k\ge 0

規則：mko_walk_def · 依賴：mko_walk_def

葉節點依據：mko_walk_def + def_unfold

展開 MKO 的三個定義。walk 要求每一個連續無序對都是邊；長度 k 是連續對的個數，也就是項數減一；simple path 另外要求所有項彼此相異。序列至少有一項（k≥0），空序列被協定排除。



S03 · implies操作前

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

操作後

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

條件：無

規則：and_intro_elim · 依賴：S02, G1, G2

葉節點依據：and_intro_elim + mko_walk_def

W₁ 有四個連續對：{0,1}、{1,2}、{2,3}、{3,4}。逐一在 E 中查到。四個條件都成立，依合取引入，W₁ 是 walk。



S04 · equivalent操作前

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

操作後

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

條件：無

規則：mko_walk_def · 依賴：S02, S03

葉節點依據：mko_walk_def + numeric_evaluation

長度是邊數（連續對的個數），不是頂點數：5 項序列有 4 個連續對，所以長度為 4。



S05 · implies操作前

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

操作後

W_1\ \text{simple path}

條件：無

規則：mko_walk_def · 依賴：S03, S02, G2

葉節點依據：mko_walk_def + and_intro_elim

W₁ 的五項 0、1、2、3、4 兩兩相異，加上 S03 的 walk 資格，依定義 W₁ 是長度 4 的 simple path。



S06 · implies操作前

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

條件：無

規則：and_intro_elim · 依賴：S02, G1, G2

葉節點依據：and_intro_elim + unordered_pair_eq + mko_walk_def

W₂ 的四個連續對是 {0,1}、{1,3}、{3,1}、{1,2}。無序對 {3,1} 與 {1,3} 是同一條邊，在 E 中。四對都是邊，所以 W₂ 是 walk；5 項，長度 4。



S07 · implies操作前

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

操作後

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

條件：無

規則：quantifier_negation · 依賴：S06, S02

葉節點依據：quantifier_negation + mko_walk_def

W₂ 的索引 1 與索引 3 的項都是 1（i=1≠3=j），所以「項兩兩相異」不成立，W₂ 不是 simple path。它仍是 walk：MKO 明說 walk 可以重複頂點與邊（這裡邊 {1,3} 走了兩次）。



S08 · implies操作前

W_3=(0,2,3)

操作後

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

條件：無

規則：quantifier_negation · 依賴：S02, G1, G2

葉節點依據：quantifier_negation + mko_walk_def

第一個連續對 {0,2} 不在 E 中（E 中含 0 的邊只有 {0,1} 與 {0,3}）。walk 要求每一對都是邊，一對失敗就足以否定。雖然 0、2、3 都是頂點、彼此相異，W₃ 仍不是 walk，因此也不是 simple path。



S09 · implies操作前

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

條件：無

規則：trail_def · 依賴：S02, G1, G2, trail_def

葉節點依據：trail_def + and_intro_elim + unordered_pair_eq

W₄ 的五個連續對 {2,3}、{3,0}、{0,1}、{1,3}、{3,4} 都在 E 中，所以是 walk；6 項，長度 5。這五條邊兩兩不同（逐一比對無序對），所以 W₄ 不重複邊，是 trail。



S10 · implies操作前

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

操作後

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

條件：無

規則：quantifier_negation · 依賴：S09, S02

葉節點依據：quantifier_negation + mko_walk_def

W₄ 的索引 1 與索引 4 的項都是頂點 3，所以 W₄ 不是 simple path，雖然它沒有重複的邊。這正是 MKO 提醒的：不重複邊的 trail 不能與 simple path 混同。



S11 · implies操作前

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}

條件：無

規則：L_path_trail · 依賴：S02, trail_def

葉節點依據：contradiction + unordered_pair_eq + trail_def

反方向的關係：每個 simple path 都是 trail（引理 L_path_trail）。證明在子步 S11.1、S11.2：假設兩條邊相同，會推出兩個不同位置的頂點相同，與 simple path 矛盾。所以 simple path 比 trail 更嚴格，S10 說明反向不成立。



S12 · implies操作前

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

條件：無

規則：inj_size_le · 依賴：S02, G1, inj_size_le

葉節點依據：inj_size_le + finite_counting_basics

simple path 的 k+1 項兩兩相異，所以 i↦v_i 是由 {i∈ℤ:0≤i≤k}（k+1 個元素）到 V（5 個元素）的單射；依鴿籠原理 k+1≤5，即長度至多 4。W₁ 的長度恰為 4，達到上界。W₄ 的長度 5>4，所以由這個上界也可看出它不可能是 simple path，與 S10 一致。



S13 · implies操作前

W_5=(4),\ k=0

操作後

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

條件：無

規則：mko_walk_def · 依賴：S02, G2

葉節點依據：mko_walk_def + forall_intro

W₅ 只有一項，沒有連續對，「每個連續對都是邊」空真成立，所以是 walk，長度 1−1=0；唯一的一項當然不重複，所以是 simple path。依 MKO 協定（假設 a2），空序列 () 不算 walk，也沒有長度。



S14 · implies操作前

W_6=(1,1)

操作後

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

條件：無

規則：graph_basics · 依賴：S01, S02, G2

葉節點依據：graph_basics + quantifier_negation

唯一的連續對是 {1,1}，它只含一個頂點，不是兩個相異頂點的無序對；本圖無 loop（S01），所以它不是邊。W₆ 不是 walk，不能把「停在原地」當成長度 1 的 walk。



S15 · implies操作前

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

條件：無

規則：and_intro_elim · 依賴：S05, S07, S08, S10, S11, S12, S13, S14

葉節點依據：and_intro_elim

彙整：W₁ 是長度 4 的 simple path；W₂ 是長度 4 的 walk，重複頂點與邊；W₃ 不是 walk；W₄ 是長度 5 的 trail，但不是 simple path；W₅ 是長度 0 的 simple path；W₆ 與空序列不是 walk。另證得 simple path 必為 trail，且本圖 simple path 長度至多 4。







## 局部子步與引理

S11.1 · implies操作前

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

條件：i<j

規則：unordered_pair_eq · 依賴：unordered_pair_eq

葉節點依據：unordered_pair_eq + and_intro_elim

為了反證，假設存在 i<j 使兩條邊相同。依無序對相等，(v_i=v_j 且 v_{i+1}=v_{j+1}) 或 (v_i=v_{j+1} 且 v_{i+1}=v_j)；兩種情形都至少給出 v_i=v_j 或 v_i=v_{j+1}。



S11.2 · implies操作前

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

操作後

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

條件：無

規則：contradiction · 依賴：S11.1, S02

葉節點依據：contradiction + case_analysis + mko_walk_def

因 i<j<j+1，位置 i 與 j、i 與 j+1 都不同；simple path 在不同位置的頂點相異，所以兩個情形都矛盾（分情形證明）。假設不成立：任兩條邊都不同。S11.1 與 S11.2 合起來證得引理 L_path_trail。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S05, S07, S08, S10, S11, S12, S13, S14, and_intro_elim — 目標 G 是所有判定與兩個一般性質的合取；足夠條件 H 是各步的結論，H⇒G 由合取引入，每一項都由已知正向證得，沒有把 G 當作前提。
- S14 · premise_audit · S01, graph_basics, quantifier_negation — 依賴「簡單圖的邊是相異頂點的無序對」；若另換允許 loop 的模型，仍須實際含有頂點 1 的 loop 才會使 W₆ 成為長度 1 的 walk；只說允許 loop 不保證結論改變。即使該 loop 存在，W₆ 仍因頂點重複而非 simple path。該模型不在此 MKO 範圍內。
- S13 · premise_audit · mko_walk_def — 空真成立是因為沒有任何 i 滿足 0≤i≤k−1=−1；空序列的排除是協定規定，不是由定義推出。
- S12 · premise_audit · inj_size_le, S02 — 需要項兩兩相異（單射）；對一般 walk 不成立，W₂ 與 W₄ 都可重複頂點。長度 ≤4 只是必要條件，不推出是 simple path（N4、N5）。
- S11.2 · premise_audit · S11.1, contradiction, case_analysis — 兩個情形涵蓋 S11.1 的所有可能；矛盾只用到 simple path 的定義。
- S11.1 · premise_audit · unordered_pair_eq, and_intro_elim — 只取每個情形的第一個合取項，不宣稱反向。
- S11 · premise_audit · L_path_trail, trail_def — 只宣稱 simple path ⇒ trail；反向由 W₄ 否定。
- S10 · premise_audit · S09, quantifier_negation — 一組見證 (i,j)=(1,4) 足以否定頂點兩兩相異；S12 的長度上界給出獨立的交叉核對。
- S09 · premise_audit · S02, trail_def, unordered_pair_eq — trail 需要 walk 加上邊不重複；這裡兩者都已逐一核對（N3 核長度）。
- S08 · premise_audit · G1, quantifier_negation — 「{0,2}∉E」依 G1 的「沒有其他邊」成立；若邊集合不完整，就不能判定不相鄰，這正是假設 a1 要求完整邊集的原因。
- S07 · premise_audit · S06, quantifier_negation — 否定「對所有 i≠j，v_i≠v_j」只需一組見證 (i,j)=(1,3)。
- S06 · premise_audit · S02, unordered_pair_eq, and_intro_elim — 因圖是無向的，{3,1}={1,3}（無序對相等）；若是有向圖，這一步要另外核對方向。
- S05 · premise_audit · S03, mko_walk_def — simple path 需要兩個條件：walk（S03）與項不重複；只有項不重複而不是 walk 不夠（見 S08）。
- S04 · inverse_equivalence · mko_walk_def, numeric_evaluation — 反向：長度 4 加一得項數 5；兩種說法描述同一個序列（N2）。
- S03 · premise_audit · S02, G1, and_intro_elim — 必須核對每一個連續對，不能只核第一對或最後一對；這一步四對都已核對。
- S02 · premise_audit · mko_walk_def, def_unfold — 只展開定義，不推出新事實；之後每個判定都回到這三個條件。
- S01 · premise_audit · G1, graph_basics — 只確認資格與做一致性核對（N1）；握手等式成立不能證明邊清單正確，只能排除部分抄寫錯誤。





## 錯誤控制與反例

頂點清單不一定是 walkMKO 指出的誤解之一是把任何頂點清單當成 walk。W₃=(0,2,3) 的三個頂點都在 V 中且彼此相異，但 {0,2} 不是邊，所以不是 walk。判定必須逐一核對每個連續對（S03、S08），而且需要完整的邊集合才能判定「不相鄰」。

長度是邊數，不是頂點數W₁ 有 5 個頂點，長度是 4。W₂ 有 5 項但只有 4 個不同頂點、3 條不同的邊，長度仍是 4：長度數的是連續對（走過的邊，重複也算），等於項數減一。

trail 不一定是 simple pathW₄ 不重複任何邊，卻兩次經過頂點 3。simple path 禁止的是重複頂點；不重複邊只是較弱的 trail 條件。引理 L_path_trail 只給出 simple path ⇒ trail 這一個方向。


- (0,2,3) 的頂點都在 V 中且不重複，所以它是 simple path → reject — {0,2}∉E，所以它根本不是 walk。
- W₁=(0,1,2,3,4) 有 5 個頂點，所以長度是 5 → reject — 長度是連續對的個數 5−1=4。
- W₄ 沒有重複的邊，所以是 simple path → reject — 頂點 3 出現在索引 1 與索引 4 的項；而且長度 5 超過 simple path 的上界 4。
- (1,1) 是在頂點 1 停留一步、長度為 1 的 walk → reject — {1,1} 不是兩個相異頂點的無序對，無 loop 簡單圖中不是邊。





## 結論與限制

在 G 中：W₁=(0,1,2,3,4) 是長度 4 的 simple path；W₂=(0,1,3,1,2) 是長度 4 的 walk 但不是 simple path；W₃=(0,2,3) 因 {0,2}∉E 不是 walk；W₄=(2,3,0,1,3,4) 是長度 5 的 trail，但頂點 3 重複，不是 simple path；W₅=(4) 是長度 0 的 simple path；W₆=(1,1) 與空序列不是 walk。每個 simple path 都是 trail，反之不然；本圖中 simple path 的長度至多為 4。


- 本稿以完整邊清單逐對核對；對更大的圖，同樣的判定可寫成演算法，但本稿不分析其複雜度。
- cycle 與連通分量不在本稿範圍內，trail 只用作對照。





## 驗證及來源綁定

7 個本稿宣告算術檢查；只支持所列算式。


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

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-graph-walk-simple-path-01.json)