# DFA-loop quantifiers and the a^n b^n contradiction [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-pumping-lemma-regular-languages/) 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-pumping-lemma-regular-languages-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope Expose quantifier order, the all-pump-count loop argument and every legal split. A necessary condition for regularity, not sufficient; no finite pumping tests prove regularity. ## Givens and symbols - work - G1 — First let D be any complete DFA, R=L(D), with p=|Q|≥1. The later L={a^n b^n:n≥0} is a separate language whose regularity is to be refuted; its p is obtained from the regularity assumption only after the first part proves the necessary condition. - p — DFA state count or assumed pumping length - r,s — parameters of all legal splits - i — last-chosen pump count ## Rules and sources - mko_definition · cited — Keep the quantifier order: there exists p, for every w in L with |w|≥p, there exist x,y,z, for every i≥0, with w=xyz, |xy|≤p, |y|>0 and xy^i z in L. Positive regular families use a repeated-state loop in a complete DFA run and a symbolic invariant for every i, not a few pump tests. For L={a^n b^n}, choose w=a^p b^p and address every legal split: y consists only of a symbols, so i=0 leaves the language. One decomposition, bounded words or finite checks do not prove regularity. The adversary chooses the word before the prover chooses the split and the adversary chooses i after that. · mko-pumping-lemma-regular-languages - work · prerequisite — A regular language is accepted by a complete finite DFA; also use deterministic runs, pigeonhole, word slicing and length, induction and quantifier negation. A target declaration only sets the proposition to prove; the DFA run establishes pumping necessity without assuming it. ## Main derivation S01 · definitionBefore \mathcal T:\ R\text{ regular}\Longrightarrow\text{the following pumping condition} After \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 Conditions: none Rule: work · Uses: G1, work Leaf basis: work This step sets a proof target and its quantifier obligations, not an established conclusion: word first, split next, pump count last. S02 · impliesBefore w\in R,\ |w|\ge p\text{ arbitrary};\quad q_j=\delta^*(q_0,w[0:j])\ (0\le j\le p) After \exists0\le r0,\quad\delta^*(q_r,y)=q_r Conditions: none Rule: work · Uses: G1, S02, work Leaf basis: work The word segment between repeated states forms a nonempty loop. S04 · impliesBefore \delta^*(q_r,y)=q_r,\quad\delta^*(q_0,w)\in F After \forall i\ge0:\ \delta^*(q_0,xy^iz)=\delta^*(q_0,w)\in F Conditions: none Rule: work · Uses: G1, S03, work Leaf basis: work Zero iterations are the base; each added y returns to the same state, proving acceptance for all pump counts. Since w was arbitrary, this now establishes the universal target of S01. S05 · impliesBefore \text{assume }L=\{a^nb^n:n\ge0\}\text{ regular};\quad p\text{ from the proved condition} After w=a^pb^p\in L,\quad |w|=2p\ge p Conditions: none Rule: work · Uses: G1, S04, work Leaf basis: work A regular language has a complete DFA, so the necessary condition proved at S04 now supplies p before the contradiction word is chosen. S06 · impliesBefore w=xyz,\quad|xy|\le p,\quad|y|>0 After 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 Conditions: none Rule: work · Uses: G1, S05, work Leaf basis: work Every legal split lies within the first p a's; parameters(r,s) describe all splits. S07 · impliesBefore \forall(r,s):0\le r,\ 1\le s,\ r+s\le p,\quad i=0 After xy^0z=a^{p-s}b^p\notin L\quad\text{since }p-s