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

Unit productions can be eliminated

Statement

A unit production is a production A→B whose left- and right-hand sides are both single variables.

For every context-free grammar G there exists a context-free grammar H such that L(H)=L(G) and H has no unit productions.

Facts & Assumptions

Given: A context-free grammar G.

[L1]

By Epsilon-productions can be eliminated except possibly at the start symbol, we may first replace G by an equivalent grammar whose only possible ε-production is a special start-symbol rule.

[L2]

The generated language is defined by derivability from the start symbol, by The language generated by a CFG.

Proof

technique · direct
1.1L1construct

Replace G by an equivalent grammar G1 as in [L1]. For variables A,B, write A⇝B when A⇒G1∗B using only unit productions. Now form H by deleting all unit productions and, whenever A⇝B and B→α is a nonunit production of G1, adding the copied production A→α.

2.1step 1.1L2

Any derivation of a terminal word in G1 can be compressed to a derivation in H by replacing each maximal block of unit productions followed by one nonunit production B→α with the copied rule A→α placed into H. Therefore every word of L(G1) lies in L(H).

2.2step 1.1L2

Conversely, every copied production A→α of H came from some unit chain A⇝B in G1 and a nonunit production B→α of G1. Expanding one use of A→α back into that unit chain followed by B→α turns any derivation in H into a derivation in G1. So every word of L(H) lies in L(G1).

3.1L1step 2.1step 2.2∎

Steps 2.1 and 2.2 give L(H)=L(G1)=L(G), and H has no unit productions by construction.

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