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.

Extended DFA transition respects concatenation

Statement

Let $D = (Q, Σ, δ, q_{0}, F)$ be a DFA with extended transition function $δ^{*}$ . Then for all $p \in Q$ and all words $u, v \in Σ^{*}$ , $δ^{*} (p, u v) = δ^{*} (δ^{*} (p, u), v) .$

Facts & Assumptions

Given: A DFA $D = (Q, Σ, δ, q_{0}, F)$ with its unique extended transition function $δ^{*}$ , a state $p \in Q$ , and words $u, v \in Σ^{*}$ .

[L1]

By The extended transition function exists and is unique, the function $δ^{*}$ satisfies $δ^{*} (q, ε) = q$ and $δ^{*} (q, x a) = δ (δ^{*} (q, x), a)$ for all states $q$ , words $x$ , and letters $a$ .

Proof

technique · direct

1.1

We prove the identity by induction on the length of $v$ . If $v = ε$ , then [L1] gives $δ^{*} (p, u ε) = δ^{*} (p, u)$ and also $δ^{*} (δ^{*} (p, u), ε) = δ^{*} (p, u)$ .

baseL1

1.2

Assume the identity holds for a word $v$ , and let $a \in Σ$ . We compare the two sides for $v a$ .

ihinduction

2.1

By [L1], $δ^{*} (p, u v a) = δ (δ^{*} (p, u v), a) .$ The induction hypothesis turns this into $δ (δ^{*} (δ^{*} (p, u), v), a) .$

L1step 1.2

3.1

Applying [L1] again, the last expression is exactly $δ^{*} (δ^{*} (p, u), v a)$ . Therefore $δ^{*} (p, u v a) = δ^{*} (δ^{*} (p, u), v a)$ .

L1step 2.1

4.1

Steps 1.1, 2.1, and 3.1 complete the induction on $v$ , so $δ^{*} (p, u v) = δ^{*} (δ^{*} (p, u), v)$ for all $u, v \in Σ^{*}$ .

step 1.1step 2.1step 3.1discharge-induction∎

Depends on

The extended transition function exists and is unique

Used by

Dependency tree · two levels

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