# A CFG production list and derivation witness [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-context-free-grammar/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-context-free-grammar-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope The grammar S to aSb or epsilon has finite derivation witnesses for aaabbb and epsilon. Grammar qualification and specified-word membership are separate; no regularity or CFG-PDA equivalence claim. ## Givens and symbols - calc - G1 — N={S}, terminals {a,b}, start S; all productions are S to aSb and S to epsilon; epsilon is the empty rhs. - N,\Sigma — nonterminal and terminal sets - P — complete production set ## Rules and sources - calc · prerequisite — Assume finite sets, finite strings and indices, stepwise function updates and induction on natural numbers; epsilon denotes the length-zero word. - mko_definition · cited — Each right side is a finite string over terminal and nonterminal symbols, with the epsilon convention explicit. A derivation is a finite production sequence. The generated language contains only terminal-only words derivable from the start. The empty language is not a language containing epsilon. A derivation witness proves membership, but bounded-search failure does not prove nonmembership. Unambiguity, regularity and CFG-PDA equivalence do not follow automatically. · mko-context-free-grammar ## Main derivation S01 · impliesBefore N=\{S\},\quad\Sigma=\{a,b\} After N\cap\Sigma=\varnothing,\quad S\in N Conditions: none Rule: calc · Uses: G1 Leaf basis: calc Both alphabets are finite, internally distinct and disjoint, with a nonterminal start. S02 · impliesBefore P=\{S\to aSb,\ S\to\varepsilon\} After \text{each lhs is one nonterminal; every rhs symbol is legal} Conditions: none Rule: calc · Uses: G1, S01 Leaf basis: calc Both left sides are the single nonterminal S; aSb uses legal symbols and epsilon is a length-zero string, not another character. S03 · impliesBefore S After aSb Conditions: none Rule: calc · Uses: G1, S02 Leaf basis: calc Apply S to aSb at the start, leaving one S. S04 · impliesBefore aSb After aaSbb Conditions: none Rule: calc · Uses: G1, S02, S03 Leaf basis: calc Replace only the central S, preserving the surrounding terminals' order. S05 · impliesBefore aaSbb After aaaSbbb Conditions: none Rule: calc · Uses: G1, S02, S04 Leaf basis: calc Use the same production again to create a third a,b pair. S06 · impliesBefore aaaSbbb After aaabbb Conditions: none Rule: calc · Uses: G1, S02, S05 Leaf basis: calc Use S to epsilon to remove the sole S without deleting or reordering terminals. S07 · impliesBefore S\Rightarrow aSb\Rightarrow aaSbb\Rightarrow aaaSbbb\Rightarrow aaabbb After aaabbb\in L(G) Conditions: none Rule: mko_definition · Uses: G1, S03, S04, S05, S06 Leaf basis: mko_definition Four legal production steps end at a terminal-only word, certifying membership. S08 · impliesBefore S\Rightarrow\varepsilon After \varepsilon\in L(G),\quad L(G)\ne\varnothing Conditions: none Rule: calc · Uses: G1, S02, S07 Leaf basis: calc The empty production gives another finite witness; a language containing epsilon is not empty. S09 · impliesBefore \text{search depth }2 After aaabbb\text{ not found by depth 2, but has the depth-4 witness above} Conditions: none Rule: calc · Uses: G1, S03, S04, S05, S06, S07 Leaf basis: calc A too-shallow search does not prove nonmembership, as the exact depth-four witness shows. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S09 · premise_audit · G1, S03, S04, S05, S06, S07 — The grammar's explicit witness suffices without invoking CFG-PDA equivalence. - S08 · premise_audit · G1, S02, S07 — Epsilon is an element of the language, whereas the empty language has no elements. - S07 · premise_audit · G1, S03, S04, S05, S06 — This witness certifies this word only, not unambiguity. - S06 · premise_audit · G1, S02, S05 — An epsilon replacement has length zero and does not output a letter called epsilon. - S05 · premise_audit · G1, S02, S04 — Each step rewrites the actual single S rather than replacing an arbitrary whole word. - S04 · premise_audit · G1, S02, S03 — A previously produced terminal a cannot be rewritten as S. - S03 · premise_audit · G1, S02 — A nonterminal remains, so this is not a terminal-only endpoint. - S02 · premise_audit · G1, S01 — Grammar qualification does not imply every word is derivable. - S01 · premise_audit · G1 — S is not terminal; a sentential form containing S is not a terminal word. ## Error controls and negative controls Terminal-only endpointA sentential form containing S is not an accepted terminal word. Production locationRewrite only a valid lhs occurrence and preserve other symbols' order. - aaSbb is already a terminal word in the language. → reject — It still contains nonterminal S. - Deriving epsilon makes the language empty. → reject — Epsilon is already an element, and aaabbb is another. - No hit at depth 2 rejects aaabbb. → reject — The explicit depth-four derivation certifies membership. ## Result and limitations The grammar S to aSb or epsilon has finite derivation witnesses for aaabbb and epsilon. ## Verification and source binding 0 declared checks for this guide; only the listed expressions are covered. - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: a8dca2b816c0c085ecbc6756e9970e00e0953a31ba8d0a4e35d497a9265aa220 - original source SHA-256: a8dca2b816c0c085ecbc6756e9970e00e0953a31ba8d0a4e35d497a9265aa220 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-context-free-grammar-01.json)