# DFA迴圈量詞與a^n b^n反證 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-pumping-lemma-regular-languages/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-pumping-lemma-regular-languages-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 可見量詞次序、全pump count迴圈證明及全部合法splits。 regular必要條件，非充分條件；不以有限pump tests證regular。 ## 已知條件與符號 - work - G1 — 前半令D為任意完整DFA，R=L(D)，p=|Q|≥1。後半的L={a^n b^n:n≥0}是另一本欲否定regular的語言；其p只在前半必要條件證成後由regular假設取得。 - p — DFA state數或假設pumping長度 - r,s — 全部split參數 - i — 最後選的pump count ## 規則與來源 - mko_definition · cited — 固定量詞順序exists p forall w in L with |w|≥p exists x,y,z forall i≥0，且w=xyz、|xy|≤p、|y|>0、xy^i z∈L。regular positive family由完整DFA run中的repeated-state loop提供對所有i的symbolic closure，不只測若干i。對L={a^n b^n}選w=a^p b^p，完整枚舉所有合法splits；每個y皆只含a，選i=0即離開L。單一decomposition、有限words或bounded checks不能證regular，且不得倒置對手選word與證明者選decomposition的量詞。 · mko-pumping-lemma-regular-languages - work · prerequisite — regular語言可由完整有限DFA接受；另使用DFA確定run、鴿籠原理、word分割與長度、數學歸納和量詞否定。目標宣告只是設定待證命題；pumping必要性由DFA run證成，不作自身前提。 ## 逐步主鏈 S01 · definition操作前 \mathcal T:\ R\text{ regular}\Longrightarrow\text{the following pumping condition} 操作後 \text{Target: }\exists p\ge1\ \forall w\in R,\ |w|\ge p\ \exists x,y,z\ \forall i\ge0:\ w=xyz,\ |xy|\le p,\ |y|>0,\ xy^iz\in R 條件：無 規則：work · 依賴：G1, work 葉節點依據：work 此步只設定待證目標與量詞責任，不宣告目標已成立：word先選，split後選，pump count最後選。 S02 · implies操作前 w\in R,\ |w|\ge p\text{ arbitrary};\quad q_j=\delta^*(q_0,w[0:j])\ (0\le j\le p) 操作後 \exists0\le r0,\quad\delta^*(q_r,y)=q_r 條件：無 規則：work · 依賴：G1, S02, work 葉節點依據：work 重複state間word片段形成非空loop。 S04 · implies操作前 \delta^*(q_r,y)=q_r,\quad\delta^*(q_0,w)\in F 操作後 \forall i\ge0:\ \delta^*(q_0,xy^iz)=\delta^*(q_0,w)\in F 條件：無 規則：work · 依賴：G1, S03, work 葉節點依據：work i=0空loop是base，每多一次y回同state；歸納證所有pump counts均接受。w原先任意，故此刻才完成S01全稱目標。 S05 · implies操作前 \text{assume }L=\{a^nb^n:n\ge0\}\text{ regular};\quad p\text{ from the proved condition} 操作後 w=a^pb^p\in L,\quad |w|=2p\ge p 條件：無 規則：work · 依賴：G1, S04, work 葉節點依據：work regular語言具有完整DFA，故現在可用S04已證的必要條件取得p，再選反證word。 S06 · implies操作前 w=xyz,\quad|xy|\le p,\quad|y|>0 操作後 x=a^r,\quad y=a^s,\quad z=a^{p-r-s}b^p,\quad0\le r,\ 1\le s,\ r+s\le p 條件：無 規則：work · 依賴：G1, S05, work 葉節點依據：work 任意合法split都完全落前p個a內；以(r,s)參數列出全部splits。 S07 · implies操作前 \forall(r,s):0\le r,\ 1\le s,\ r+s\le p,\quad i=0 操作後 xy^0z=a^{p-s}b^p\notin L\quad\text{since }p-s