Alphabeta Math
TheoremStatement: 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.

The extended transition function exists and is unique

Statement

For every DFA D=(Q,Σ,δ,q0,F) there exists a unique function δ∗:Q×Σ∗→Q such that, for all q∈Q, u∈Σ∗, and a∈Σ, δ∗(q,ε)=q,δ∗(q,ua)=δ(δ∗(q,u),a).

Facts & Assumptions

Given: A DFA D=(Q,Σ,δ,q0,F).

[L1]

By The extended transition function of a DFA, an extended transition function for D is exactly a function δ∗:Q×Σ∗→Q satisfying the two displayed clauses for ε and ua.

Proof

technique · direct
1.1givenconstruct

Fix q∈Q and a word w=a0a1⋯an−1. Define a sequence of states by s0=q and si+1=δ(si,ai) for 0≤i<n, and then define δ∗(q,w):=sn. This gives a function Q×Σ∗→Q because the DFA transition function supplies exactly one next state at each letter.

2.1step 1.1L1

If w=ε, then n=0 and step 1.1 gives δ∗(q,ε)=s0=q. If w=ua with u=a0⋯an−2 and a=an−1, then the last state in the sequence is sn=δ(sn−1,a)=δ(δ∗(q,u),a). So the function from step 1.1 satisfies the two clauses of [L1].

3.1baseL1step 2.1

Let η:Q×Σ∗→Q be any other function satisfying [L1]. We prove by induction on the length of w that η(q,w)=δ∗(q,w) for every q∈Q. For w=ε, both values are q by [L1] and step 2.1.

3.2ihL1step 2.1induction

Assume η(q,u)=δ∗(q,u) for all words u of length n, and let w=ua have length n+1. Then [L1] gives η(q,w)=δ(η(q,u),a), and the induction hypothesis turns this into δ(δ∗(q,u),a)=δ∗(q,w) by step 2.1.

4.1step 1.1step 2.1step 3.1step 3.2discharge-induction∎

Steps 3.1 and 3.2 show that every function satisfying [L1] agrees with the function built in step 1.1, so the extended transition function exists and is unique.

Depends on

Used by

Dependency tree · two levels

3 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