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.

Extended DFA transition respects concatenation

Statement

Let D=(Q,Σ,δ,q0,F) be a DFA with extended transition function δ∗. Then for all p∈Q and all words u,v∈Σ∗, δ∗(p,uv)=δ∗(δ∗(p,u),v).

Facts & Assumptions

Given: A DFA D=(Q,Σ,δ,q0,F) with its unique extended transition function δ∗, a state p∈Q, and words u,v∈Σ∗.

[L1]

By The extended transition function exists and is unique, the function δ∗ satisfies δ∗(q,ε)=q and δ∗(q,xa)=δ(δ∗(q,x),a) for all states q, words x, and letters a.

Proof

technique · direct
1.1baseL1

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

1.2ihinduction

Assume the identity holds for a word v, and let a∈Σ. We compare the two sides for va.

2.1L1step 1.2

By [L1], δ∗(p,uva)=δ(δ∗(p,uv),a). The induction hypothesis turns this into δ(δ∗(δ∗(p,u),v),a).

3.1L1step 2.1

Applying [L1] again, the last expression is exactly δ∗(δ∗(p,u),va). Therefore δ∗(p,uva)=δ∗(δ∗(p,u),va).

4.1step 1.1step 2.1step 3.1discharge-induction∎

Steps 1.1, 2.1, and 3.1 complete the induction on v, so δ∗(p,uv)=δ∗(δ∗(p,u),v) for all u,v∈Σ∗.

Depends on

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