LemmaStatement: Literature-sourcedProof: 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.

The induced word map is the unique concatenation-preserving extension

Statement

Let $h : Σ \to Δ^{*}$ be an alphabet map and let $\hat{h} : Σ^{*} \to Δ^{*}$ be its induced word map. For $a \in Σ$ , write $⟨ a ⟩ : 1 \to Σ$ for the one-letter word whose unique value is $a$ .

For all words $u, v \in Σ^{*}$ , $\hat{h} (u v) = \hat{h} (u) \hat{h} (v) .$
If $g : Σ^{*} \to Δ^{*}$ satisfies $g (u v) = g (u) g (v)$ for all words $u, v$ and $g (⟨ a ⟩) = h (a)$ for every $a \in Σ$ , then $g = \hat{h}$ .

Facts & Assumptions

Given: An alphabet map $h : Σ \to Δ^{*}$ , its induced map $\hat{h} : Σ^{*} \to Δ^{*}$ , and a map $g : Σ^{*} \to Δ^{*}$ preserving concatenation and satisfying $g (⟨ a ⟩) = h (a)$ for every $a \in Σ$ .

[L1]

The induced map is defined by $\hat{h} (ε) = ε$ and $\hat{h} (a_{0} \dots a_{n - 1}) = h (a_{0}) \dots h (a_{n - 1})$ by Alphabet maps into $Δ^{*}$ and their induced maps on words.

[L2]

Word concatenation is formed by writing the letters of the first word followed by those of the second, by Computation alphabets, words, the empty word, and $Σ^{*}$ .

Proof

technique · direct

1.1givenL1L2

If $u = a_{0} \dots a_{m - 1}$ and $v = b_{0} \dots b_{n - 1}$ , then [L2] says that the word $u v$ is $a_{0} \dots a_{m - 1} b_{0} \dots b_{n - 1}$ . Applying [L1] to that word gives $\hat{h} (u v) = h (a_{0}) \dots h (a_{m - 1}) h (b_{0}) \dots h (b_{n - 1})$ , which is exactly $\hat{h} (u) \hat{h} (v)$ .

1.2givenalgebra

Since $g$ preserves concatenation, $g (ε) = g (ε ε) = g (ε) g (ε)$ . Comparing word lengths forces $g (ε) = ε$ .

1.3ihgivenL1induction

For the induction step, write a nonempty word as $w = u ⟨ a ⟩$ with $a \in Σ$ its final letter. If $g (u) = \hat{h} (u)$ , then $g (w) = g (u ⟨ a ⟩) = g (u) g (⟨ a ⟩) = \hat{h} (u) h (a) = \hat{h} (u ⟨ a ⟩) = \hat{h} (w)$ by the hypothesis on $g$ and [L1].

2.1step 1.2L1base

We prove $g (w) = \hat{h} (w)$ for every word $w$ by induction on the length of $w$ . The base case is the empty word, handled by step 1.2 and [L1].

3.1step 1.1step 2.1step 1.3discharge-induction∎

Steps 2.1 and 1.3 show that $g (w) = \hat{h} (w)$ for every word $w$ , so $g = \hat{h}$ . Together with step 1.1 this proves both clauses.

Depends on

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)