LemmaStatement: 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.

The quotient by state equivalence is a well-defined equivalent DFA

Statement

Let $D$ be a DFA. The quotient automaton $D / \equiv_{D}$ of The quotient DFA by state equivalence is well defined and recognizes the same language as $D$ .

Facts & Assumptions

Given: A DFA $D = (Q, Σ, δ, q_{0}, F)$ with extended transition function $δ^{*}$ .

[L1]

By The quotient DFA by state equivalence, the quotient automaton uses states $[q]$ , transition rule $\overline{δ} ([q], a) = [δ (q, a)]$ , start state $[q_{0}]$ , and accepting classes $\overline{F} = {[q] : q \in F}$ .

[L2]

By State-equivalent DFA states stay equivalent after every input word, if $q \equiv_{D} q^{'}$ then $δ^{*} (q, u) \equiv_{D} δ^{*} (q^{'}, u)$ for every word $u$ , hence in particular $δ (q, a) \equiv_{D} δ (q^{'}, a)$ for every letter $a$ .

[L3]

By Acceptance of a word by a DFA and the recognized language, a DFA accepts a word exactly when the state reached by its extended transition function is accepting.

[L4]

By The extended transition function of a DFA, the extended transition satisfies $δ^{*} (q, ε) = q$ and $δ^{*} (q, u a) = δ (δ^{*} (q, u), a)$ .

[L5]

By The right language of a DFA state and state equivalence, $q \equiv_{D} q^{'}$ means that for every continuation $u \in Σ^{*}$ one has $δ^{*} (q, u) \in F$ if and only if $δ^{*} (q^{'}, u) \in F$ .

Proof

technique · direct

1.1

Step [L2] shows that if $q \equiv_{D} q^{'}$ then $[δ (q, a)] = [δ (q^{'}, a)]$ for every letter $a$ , so $\overline{δ} ([q], a)$ is independent of the chosen representative.

L1L2given

1.2

If $q \equiv_{D} q^{'}$ and $q \in F$ , then [L4] gives $δ^{*} (q, ε) = q$ and $δ^{*} (q^{'}, ε) = q^{'}$ . Applying [L5] to the continuation $ε$ therefore shows $q^{'} \in F$ as well. Thus $\overline{F}$ is representative-independent.

L4L5

1.3

Let ${\overline{δ}}^{*}$ be the extended transition of the quotient DFA. Induction on $u$ using [L1] and [L4] gives ${\overline{δ}}^{*} ([q], u) = [δ^{*} (q, u)]$ for every state class $[q]$ and every word $u$ .

L1L4induction

2.1

For every word $u$ , step 1.3 and [L3] give $u \in L (D / \equiv_{D}) ⟺ {\overline{δ}}^{*} ([q_{0}], u) \in \overline{F} ⟺ [δ^{*} (q_{0}, u)] \in \overline{F} ⟺ δ^{*} (q_{0}, u) \in F ⟺ u \in L (D)$ .

L3step 1.2step 1.3

3.1

Therefore the quotient DFA is well defined and equivalent to $D$ .

step 1.1step 1.2step 2.1∎

Depends on

Used by

Dependency tree · two levels

10 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)