LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 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.

State-equivalent DFA states stay equivalent after every input word

Statement

For every DFA $D$ , the state-equivalence relation $\equiv_{D}$ of The right language of a DFA state and state equivalence is an equivalence relation on the state set, and for every word $u \in Σ^{*}$ , $p \equiv_{D} q ⟹ δ^{*} (p, u) \equiv_{D} δ^{*} (q, u) .$

Facts & Assumptions

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

[L1]

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

[L2]

By Equivalence relation, equivalence class, and the quotient set $A / \sim$ , a relation is an equivalence relation exactly when it is reflexive, symmetric, and transitive.

[L3]

By The extended transition function of a DFA, $δ^{*} (s, ε) = s$ and $δ^{*} (s, v a) = δ (δ^{*} (s, v), a)$ for every state $s$ , word $v$ , and letter $a$ .

Proof

technique · direct

1.1L1L2given

Equality of right languages is reflexive, symmetric, and transitive, so [L1] and [L2] show that $\equiv_{D}$ is an equivalence relation on $Q$ .

1.2L1L3construct

Fix a letter $a \in Σ$ . If $p \equiv_{D} q$ , then induction on $v$ using [L3] gives $δ^{*} (δ (p, a), v) = δ^{*} (p, a v)$ and $δ^{*} (δ (q, a), v) = δ^{*} (q, a v)$ for every word $v$ ; applying [L1] to the continuation $a v$ therefore yields $δ (p, a) \equiv_{D} δ (q, a)$ .

2.1L3step 1.2induction

We now induct on the word $u$ . The case $u = ε$ is immediate from [L3]. If the claim holds for $u$ and $a \in Σ$ , then step 1.2 applied to the equivalent states $δ^{*} (p, u)$ and $δ^{*} (q, u)$ gives $δ^{*} (p, u a) \equiv_{D} δ^{*} (q, u a)$ .

3.1step 1.1step 2.1∎

Steps 1.1 and 2.1 prove both claims.

Depends on

Used by

Dependency tree · two levels

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