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.

Derivations and parse trees correspond

Statement

Let G=(V,Σ,P,S) be a context-free grammar and let w∈Σ∗.

  1. The word w is derived from S in G if and only if there exists a parse tree for G with yield w.
  2. Every parse tree for G determines a unique leftmost derivation of its yield and a unique rightmost derivation of its yield.

Facts & Assumptions

Given: A context-free grammar G=(V,Σ,P,S) and a word w∈Σ∗.

[L1]

Leftmost and rightmost derivations are the derivations that rewrite the leftmost or rightmost remaining variable at each step, by Leftmost and rightmost derivations.

[L2]

A parse tree is finite; each internal node labelled A records exactly one production A→x1⋯xk whose ordered children carry the labels x1,…,xk; variable leaves may represent ε-productions; and the yield is the left-to-right list of terminal leaves, by Parse trees and their yields.

Proof

technique · direct
1.1

Suppose first that S⇒G∗w. Start with one root labelled S and process the derivation step by step. When a step rewrites a current leaf labelled A by a nonempty right-hand side x1⋯xk, make that leaf an internal node with ordered children labelled x1,…,xk. When a step uses A→ε, leave that leaf in place as the variable leaf corresponding to the ε-production. Because the derivation is finite, this constructs a finite parse tree whose nodes record exactly the productions used in the derivation.

givenL2induction
1.2

Conversely, suppose a parse tree for G has yield w. Start from the sentential form S and repeatedly rewrite the leftmost variable leaf represented in the fixed tree: if that leaf is an internal node of the tree with ordered children x1,…,xk, apply the production A→x1⋯xk; if it is a variable leaf corresponding to A→ε, apply that ε-production. By [L2], every step is licensed by G, and by construction every step is leftmost in the sense of [L1]. Because the tree is finite, this process terminates after one step for each variable-labelled node, and the final terminal frontier is exactly the yield w.

givenL1L2construct
2.1

At the end of the construction in step 1.1, the leaves read left to right are exactly the symbols of the terminal word w, because each derivation step replaces one leaf occurrence of A by the same ordered right-hand side that the tree stores. So a derivation of w yields a parse tree whose yield is w.

step 1.1L2
2.2

The choice in step 1.2 is forced: at each stage there is a unique leftmost variable leaf of the fixed parse tree, so the leftmost derivation read from the tree is unique. The same argument, reading rightmost variable leaves instead, gives a unique rightmost derivation.

step 1.2L1
3.1

Steps 1.1 and 2.1 prove the forward implication of clause 1, and step 1.2 proves the reverse implication. Step 2.2 proves clause 2.

step 1.1step 2.1step 1.2step 2.2∎

Depends on

Used by

Dependency tree · two levels

6 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