Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 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.

Context-free languages are closed under union, concatenation, Kleene star, and homomorphism

Statement

If L1,L2 are context-free languages over an alphabet Σ, and if h:ΣΔ is an alphabet map, then the following languages are context-free:

  1. L1L2,
  2. L1L2,
  3. L1,
  4. h^(L1)={h^(w):wL1}.

Facts & Assumptions

Given: Context-free languages L1 and L2, together with grammars G1=(V1,Σ,P1,S1) and G2=(V2,Σ,P2,S2) generating them, and an alphabet map h:ΣΔ.

[L1]

A language is context-free exactly when it is generated by some context-free grammar, by The language generated by a CFG.

[L2]

The induced word map h^ is obtained by replacing each letter a of a word by the word h(a) and concatenating the results, by Alphabet maps into Δ and their induced maps on words.

Proof

technique · direct
1.1

Rename variables of G1 and G2 apart, and add a fresh start variable S. The grammar with productions of G1 and G2 together with SS1 and SS2 generates exactly L1L2. Similarly, adding only the bridge rule SS1S2 yields a grammar for the concatenation L1L2.

givenL1construct
1.2

For Kleene star, keep G1 and add a fresh start variable S with productions Sε and SS1S. Repeating the second rule any finite number of times and then using Sε generates exactly a concatenation of finitely many words from L1, so the new grammar generates L1.

constructL1
1.3

For homomorphism, first rename the variables of the chosen grammar for L1 so that they are disjoint from Δ. Then replace every terminal letter a occurring in a production by the word h(a), keeping that renamed variable set unchanged. The result is still a context-free grammar over Δ, and if a derivation in the source grammar yields w=a0an1, then the corresponding derivation in the rewritten grammar yields h(a0)h(an1)=h^(w) by [L2].

L2construct
2.1

Conversely, any terminal derivation in the rewritten grammar follows the same variable-expansion pattern as a terminal derivation in the renamed source grammar, because the only change was to replace each source terminal occurrence by its prescribed image word h(a). Therefore the terminal word produced at the end is exactly the image under h^ of a word of L1, so the new grammar generates exactly h^(L1).

L2step 1.3
3.1

Steps 1.1, 1.2, 1.3, and 2.1 construct grammars for all four languages, so [L1] shows that context-free languages are closed under union, concatenation, Kleene star, and homomorphism.

L1step 1.1step 1.2step 1.3step 2.1

Depends on

Used by

Dependency tree · two levels

5 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