LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30

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.

Removing unreachable states preserves the recognized language

Statement

Let $D = (Q, Σ, δ, q_{0}, F)$ be a DFA, let $Q_{r} \subseteq Q$ be its reachable states, and let $D_{r}$ be the DFA obtained by restricting $D$ to the states $Q_{r}$ . Then $L (D_{r}) = L (D) .$

Facts & Assumptions

Given: A DFA $D = (Q, Σ, δ, q_{0}, F)$ and its reachable-state subset $Q_{r}$ .

[L1]

A state is reachable exactly when it has the form $δ^{*} (q_{0}, w)$ for some input word $w$ , by Reachable states of a DFA.

[L2]

A word is accepted exactly when the extended transition from the start state lands in an accepting state, by Acceptance of a word by a DFA and the recognized language.

Proof

technique · direct

1.1

Let $w = a_{0} a_{1} \dots a_{n - 1}$ be any input word, and consider the run of $D$ from $q_{0}$ on $w$ . After reading the prefix $a_{0} \dots a_{i - 1}$ , the machine is in the state $δ^{*} (q_{0}, a_{0} \dots a_{i - 1})$ , so [L1] says every state visited during the run is reachable.

givenL1

2.1

Therefore the entire run of $D$ on $w$ stays inside $Q_{r}$ , and the restricted machine $D_{r}$ has exactly the same transitions on those states. So $D_{r}$ ends in the same final state as $D$ on the word $w$ .

step 1.1

3.1

By [L2], the word $w$ is accepted by $D_{r}$ if and only if that common final state lies in $F \cap Q_{r}$ , which is equivalent to the same final state lying in $F$ . Hence $w$ is accepted by $D_{r}$ exactly when it is accepted by $D$ .

L2step 2.1

4.1

Since this holds for every word $w \in Σ^{*}$ , the two machines recognize the same language.

step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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