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.

Eliminating immediate left recursion preserves the language

Statement

Suppose the productions of a variable $A$ in a context-free grammar are exactly $A \to A u_{1}, \dots, A \to A u_{r}, A \to v_{1}, \dots, A \to v_{s},$ where none of the words $v_{j}$ begins with $A$ . Introduce a fresh variable $R$ and replace those productions by $A \to v_{1}, \dots, A \to v_{s}, A \to v_{1} R, \dots, A \to v_{s} R,$ $R \to u_{1}, \dots, R \to u_{r}, R \to u_{1} R, \dots, R \to u_{r} R,$ leaving every other production unchanged.

Then the resulting grammar generates the same language as the original grammar.

Facts & Assumptions

Given: The original grammar and the rewritten grammar related by the displayed immediate-left-recursion elimination step.

[L1]

Leftmost derivations always rewrite the leftmost remaining variable, by Leftmost and rightmost derivations.

[L2]

The language of a grammar is determined by the terminal words derivable from its start symbol, by The language generated by a CFG.

Proof

technique · direct

1.1

Consider a leftmost derivation segment in the original grammar beginning with $A$ . Because every left-recursive rule has the form $A \to A u_{i}$ , any maximal initial block of left-recursive steps must look like $A \Rightarrow A u_{i_{1}} \Rightarrow A u_{i_{2}} u_{i_{1}} \Rightarrow \dots \Rightarrow A u_{i_{k}} \dots u_{i_{1}} \Rightarrow v_{j} u_{i_{k}} \dots u_{i_{1}} .$ So the contribution of this segment is always one non-left-recursive word $v_{j}$ followed by a finite concatenation of the $u_{i}$ .

L1given

2.1

The new variable $R$ generates exactly the nonempty finite concatenations of the $u_{i}$ : use $R \to u_{i}$ for a one-term concatenation and $R \to u_{i} R$ to prepend further $u_{i}$ 's. Therefore the segment in step 1.1 is reproduced in the rewritten grammar either by $A \to v_{j}$ when $k = 0$ or by $A \to v_{j} R$ followed by a derivation of the same tail from $R$ when $k \geq 1$ .

constructstep 1.1

3.1

Conversely, any derivation segment in the rewritten grammar beginning with $A$ either uses $A \to v_{j}$ directly or uses $A \to v_{j} R$ followed by a derivation of a finite concatenation of the $u_{i}$ from $R$ . Reversing the regrouping in step 1.1 turns that segment back into a block of left-recursive uses of $A \to A u_{i}$ ending with $A \to v_{j}$ in the original grammar.

step 2.1

4.1

Since all other productions are unchanged, steps 2.1 and 3.1 convert derivations of terminal words back and forth without changing the yield. Hence [L2] gives equality of the generated languages.

L2step 2.1step 3.1∎

Depends on

Used by

Every context-free language has an equivalent grammar in Greibach normal form Theorem

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

CSC444 CFLs and PDAs (standard reference, not scraped)