DefinitionDefinition: Literature-sourcedProof: Not applicablejudge 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.

One-step derivation and finite derivation in a context-free grammar

Definition

Let $G = (V, Σ, P, S)$ be a context-free grammar. A word over $V \cup Σ$ is a sentential form.

For sentential forms $β, γ$ , write $β \Rightarrow_{G} γ$ when there exist words $x, y$ over $V \cup Σ$ , a variable $A \in V$ , and a production $A \to α$ in $P$ such that $β = x A y, γ = x α y .$ This is the one-step derivation relation of $G$ , a relation in the sense of Relation, $dom R$ , $ran R$ , $fld R$ , and the specialisations "relation from $A$ to $B$ " and "relation on $A$ " on the set of sentential forms.

Write $β \Rightarrow_{G}^{*} γ$ when $γ$ is obtained from $β$ by finitely many one-step derivations, possibly zero. This is the reflexive transitive closure of $\Rightarrow_{G}$ , and a chain $β = β_{0} \Rightarrow_{G} β_{1} \Rightarrow_{G} \dots \Rightarrow_{G} β_{n} = γ$ is a finite derivation from $β$ to $γ$ .

Depends on

Used by

Leftmost and rightmost derivations Definition
Nullable, generating, and reachable variables Definition
The language generated by a CFG Definition
Substituting a variable's productions into a leading variable occurrence preserves the language Lemma

Dependency tree · two levels

9 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)
John Watrous, Introduction to the Theory of Computing, Lecture 7 (standard reference, not scraped)