Alphabeta Math
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,Σ,δ,q0,F) be a DFA, let Qr⊆Q be its reachable states, and let Dr be the DFA obtained by restricting D to the states Qr. Then L(Dr)=L(D).

Facts & Assumptions

Given: A DFA D=(Q,Σ,δ,q0,F) and its reachable-state subset Qr.

[L1]

A state is reachable exactly when it has the form δ∗(q0,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.1givenL1

Let w=a0a1⋯an−1 be any input word, and consider the run of D from q0 on w. After reading the prefix a0⋯ai−1, the machine is in the state δ∗(q0,a0⋯ai−1), so [L1] says every state visited during the run is reachable.

2.1step 1.1

Therefore the entire run of D on w stays inside Qr, and the restricted machine Dr has exactly the same transitions on those states. So Dr ends in the same final state as D on the word w.

3.1L2step 2.1

By [L2], the word w is accepted by Dr if and only if that common final state lies in F∩Qr, which is equivalent to the same final state lying in F. Hence w is accepted by Dr exactly when it is accepted by D.

4.1step 3.1∎

Since this holds for every word w∈Σ∗, the two machines recognize the same language.

Depends on

Used by

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