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

Regular languages are closed under homomorphic image

Statement

Let $h : Σ \to Δ^{*}$ be an alphabet map with induced word map $\hat{h} : Σ^{*} \to Δ^{*}$ , and let $L \subseteq Σ^{*}$ be regular. Then $\hat{h} [L] : = {\hat{h} (w) : w \in L}$ is a regular language over $Δ$ .

Facts & Assumptions

Given: An alphabet map $h : Σ \to Δ^{*}$ and a regular language $L \subseteq Σ^{*}$ .

[L1]

By Alphabet maps into $Δ^{*}$ and their induced maps on words, the induced map $\hat{h}$ sends a concatenated word to the concatenation of the image words of its letters.

[L2]

By The language denoted by a regular expression, the denotation of a regular expression is built recursively from union, concatenation, and star on languages.

[L3]

By Regular-expression denotation is structurally well-defined, recursive substitutions through a regular-expression tree produce a uniquely determined regular expression.

[L4]

By A language is regular if and only if some regular expression denotes it, every regular language is denoted by some regular expression.

Proof

technique · direct

1.1

Choose a regular expression $R$ over $Σ$ with $L (R) = L$ by [L4]. For each letter $a \in Σ$ , choose a regular expression $E_{a}$ over $Δ$ that denotes the single word $h (a)$ : if $h (a) = ε$ take $E_{a} = ε$ , and if $h (a) = b_{1} \dots b_{n}$ with $n \geq 1$ , take the concatenation $E_{a} : = b_{1} \dots b_{n}$ .

L1L4givenchoose

2.1

Define $T (R)$ by recursively replacing each occurrence of a letter $a$ in $R$ by $E_{a}$ , while leaving $\emptyset$ and $ε$ fixed and commuting with $+$ , concatenation, and $^{*}$ . By [L3], this gives one well-defined regular expression over $Δ$ .

L3step 1.1construct

3.1

A structural induction on $R$ using [L1] and [L2] shows that $L (T (R)) = {\hat{h} (w) : w \in L (R)}$ . Since $L (R) = L$ , this language is exactly $\hat{h} [L]$ . Therefore $\hat{h} [L]$ is denoted by a regular expression and is regular.

L1L2step 2.1induction∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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

H. Conrad Cunningham, Notes on Models of Computation, Chapter 4: Properties of Regular Languages (standard reference, not scraped)
Jean Gallier and Jocelyn Quaintance, Introduction to the Theory of Computation: Some Notes for CIS511 (standard reference, not scraped)