TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-12

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A language is regular if and only if its Nerode equivalence has finite index

Statement

Let $L \subseteq Σ^{*}$ be a language. Then $L$ is regular if and only if its Nerode equivalence relation $\equiv_{L}$ has finite index.

Facts & Assumptions

Given: A language $L \subseteq Σ^{*}$ over an alphabet $Σ$ .

[L1]

By Regular languages, a language is regular exactly when some DFA recognizes it; acceptance and the recognized language are those of Acceptance of a word by a DFA and the recognized language.

[L2]

By A DFA can realize at most one Nerode class per reachable state, if a DFA recognizes $L$ then distinct Nerode classes of $L$ must reach distinct reachable states of that DFA.

[L3]

By Nerode-equivalent words stay equivalent after right concatenation, $u \equiv_{L} v$ implies $u a \equiv_{L} v a$ for every letter $a \in Σ$ , so the transition rule $[u] \mapsto [u a]$ on Nerode classes is well defined.

[L4]

By Deterministic finite automata, a DFA is determined by a finite state set, a start state, a total transition rule on letters, and a chosen accepting subset.

Proof

technique · direct

1.1L1L2given

Assume $L$ is regular. By [L1], choose a DFA $D$ recognizing $L$ . Step [L2] gives an injection from the set of Nerode classes of $L$ into the reachable state set of $D$ , so the index of $\equiv_{L}$ is finite because a DFA has only finitely many states.

1.2L3L4construct

Assume conversely that $\equiv_{L}$ has finite index. Let $Q$ be its finite set of equivalence classes, let the start state be $[ε]$ , define $δ ([u], a) : = [u a]$ , and let $F : = {[u] \in Q : u \in L}$ . By [L3], the transition rule is well defined, so [L4] gives a DFA $D_{L} = (Q, Σ, δ, [ε], F)$ .

2.1L1step 1.2induction

For every word $u \in Σ^{*}$ , induction on $u$ shows that the state reached by $D_{L}$ from $[ε]$ is exactly $[u]$ . Hence $u \in L (D_{L}) ⟺ [u] \in F ⟺ u \in L$ , so $D_{L}$ recognizes $L$ and [L1] implies that $L$ is regular.

3.1step 1.1step 2.1∎

Steps 1.1 and 2.1 prove both implications.

Depends on

Used by

Infinitely many pairwise distinguishable prefixes force nonregularity Corollary
Nerode classes form the canonical minimal DFA Corollary

Dependency tree · two levels

14 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jean Gallier and Jocelyn Quaintance, Introduction to the Theory of Computation: Some Notes for CIS511 (standard reference, not scraped)
Eric Blais, Models of Computation, 20. Nonregular Languages (standard reference, not scraped)