ExampleConstruction: Literature-sourcedVerification: 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.

Merging equivalent sink-like states in a small DFA

Example

Consider the DFA over ${a, b}$ with states $q_{0}, q_{a}, q_{b}, r, s,$ start state $q_{0}$ , accepting states ${q_{a}, q_{b}}$ , and transitions $δ (q_{0}, a) = q_{a}, δ (q_{0}, b) = q_{b}, δ (q_{a}, a) = r, δ (q_{a}, b) = s,$ $δ (q_{b}, a) = r, δ (q_{b}, b) = q_{b}, δ (r, a) = r, δ (r, b) = r, δ (s, a) = s, δ (s, b) = s .$ It recognizes the language ${a} \cup {b^{m} : m \geq 1}$ .

Facts & Assumptions

Given: The displayed DFA.

[L1]

By The quotient by state equivalence is a well-defined equivalent DFA, merging state-equivalent states yields a well-defined DFA with the same language.

Verification

technique · direct

1.1given

The states $r$ and $s$ are equivalent because every continuation from either state stays in a rejecting sink. No other pair is equivalent: $q_{a}$ is distinguished from $q_{b}$ by the word $b$ , and $q_{0}$ is distinguished from both $q_{a}$ and $q_{b}$ by $ε$ .

2.1L1step 1.1

The quotient therefore has four states $[q_{0}]$ , $[q_{a}]$ , $[q_{b}]$ , and $[r] = [s]$ . Its only nontrivial merge is the class $[r] = [s]$ , and [L1] shows that the quotient recognizes the same language as the original DFA.

3.1step 2.1∎

Concretely, the quotient still accepts $a$ , $b$ , and $b b$ , while it rejects $ε$ , $a b$ , and $b a$ . The merge removes a redundant rejecting state without changing any acceptance decision.

Depends on

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

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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