Context-free grammars
DefinitionInterpretation of a grammar symbol#✓fully proved
Under an assignment \(V\) of languages to nonterminals, a terminal \(a\) denotes the language containing only the one-letter word \(a\), and a nonterminal \(A\) denotes its assigned language \(V(A)\).
def evalSymbol (V : N → Language T) : Symbol T N → Language T
| .terminal a => {[a]}
| .nonterminal A => V AUsed by 16
DefinitionInterpretation of a sentential form#✓fully proved
Under an assignment \(V\) of languages to nonterminals, a sentential form denotes the concatenation, in order, of the languages its symbols denote: a terminal \(a\) denotes the language containing only the one-letter word \(a\), and a nonterminal \(A\) denotes \(V(A)\). The empty sentential form denotes the language containing only the empty word.
def evalForm (V : N → Language T) : List (Symbol T N) → Language T
| [] => 1
| s :: u => evalSymbol V s * evalForm V udef evalSymbol (V : N → Language T) : Symbol T N → Language T
| .terminal a => {[a]}
| .nonterminal A => V ACSLibExt/Computability/Languages/ContextFree/Basic.lean:51
Uses 1 · Used by 46
TheoremInterpretation of a concatenation#✓fully proved
For every assignment \(V\) of languages to nonterminals and all sentential forms \(u\) and \(v\), the language that \(uv\) denotes under \(V\) is the concatenation of the languages that \(u\) and \(v\) denote under \(V\).
theorem evalForm_append (V : N → Language T) (u v : List (Symbol T N)) :
evalForm V (u ++ v) = evalForm V u * evalForm V vdef evalForm (V : N → Language T) : List (Symbol T N) → Language T
| [] => 1
| s :: u => evalSymbol V s * evalForm V uCSLibExt/Computability/Languages/ContextFree/Basic.lean:68
Uses 2 · Used by 5
TheoremA terminal word denotes its singleton#✓fully proved
Under every assignment of languages to nonterminals, a terminal word \(w\), read as a sentential form, denotes the singleton language \(\{w\}\).
theorem evalForm_map_terminal (V : N → Language T) (w : List T) :
evalForm V (w.map Symbol.terminal) = {w}def evalForm (V : N → Language T) : List (Symbol T N) → Language T
| [] => 1
| s :: u => evalSymbol V s * evalForm V uCSLibExt/Computability/Languages/ContextFree/Basic.lean:68
Uses 1 · Used by 9
DefinitionValuation of a grammar#✓fully proved
Let \(g\) be a context-free grammar with terminals \(T\), and let \(V\) assign a language over \(T\) to each nonterminal of \(g\). Interpret a sentential form under \(V\) by sending each terminal \(a\) to the language \(\{a\}\) of the one-letter word \(a\) and each nonterminal \(B\) to \(V(B)\), and concatenating these languages in order (the empty form is interpreted as \(\{\varepsilon\}\)). Then \(V\) is a valuation of \(g\) when, for every production \(A \to u\) of \(g\), the interpretation of \(u\) under \(V\) is contained in \(V(A)\).
def IsValuation (g : ContextFreeGrammar T) (V : g.NT → Language T) : Prop :=
∀ r ∈ g.rules, evalForm V r.output ≤ V r.inputdef evalForm (V : N → Language T) : List (Symbol T N) → Language T
| [] => 1
| s :: u => evalSymbol V s * evalForm V uCSLibExt/Computability/Languages/ContextFree/Basic.lean:68
Uses 1 · Used by 29
TheoremA production step shrinks interpretations under a valuation#✓fully proved
Let \(g\) be a context-free grammar and \(V\) a valuation of \(g\). If a sentential form \(u\) rewrites to \(v\) by one production of \(g\), then the language that \(v\) denotes under \(V\) is contained in the language that \(u\) denotes under \(V\).
theorem evalForm_le_of_produces {V : g.NT → Language T} (hV : IsValuation g V)
{u v : List (Symbol T g.NT)} (h : g.Produces u v) :
evalForm V v ≤ evalForm V udef IsValuation (g : ContextFreeGrammar T) (V : g.NT → Language T) : Prop :=
∀ r ∈ g.rules, evalForm V r.output ≤ V r.inputCSLibExt/Computability/Languages/ContextFree/Basic.lean:108
def evalForm (V : N → Language T) : List (Symbol T N) → Language T
| [] => 1
| s :: u => evalSymbol V s * evalForm V uCSLibExt/Computability/Languages/ContextFree/Basic.lean:68
Uses 3 · Used by 1
TheoremDerivations shrink interpretations under a valuation#✓fully proved
Let \(g\) be a context-free grammar and \(V\) a valuation of \(g\). If a sentential form \(u\) derives \(v\) in \(g\) (in zero or more steps), then the language that \(v\) denotes under \(V\) is contained in the language that \(u\) denotes under \(V\).
theorem evalForm_le_of_derives {V : g.NT → Language T} (hV : IsValuation g V)
{u v : List (Symbol T g.NT)} (h : g.Derives u v) :
evalForm V v ≤ evalForm V udef IsValuation (g : ContextFreeGrammar T) (V : g.NT → Language T) : Prop :=
∀ r ∈ g.rules, evalForm V r.output ≤ V r.inputCSLibExt/Computability/Languages/ContextFree/Basic.lean:108
def evalForm (V : N → Language T) : List (Symbol T N) → Language T
| [] => 1
| s :: u => evalSymbol V s * evalForm V uCSLibExt/Computability/Languages/ContextFree/Basic.lean:68
Uses 3 · Used by 5
TheoremValuations bound the language of a grammar#✓fully proved
For every context-free grammar \(g\) and every valuation \(V\) of \(g\), the language generated by \(g\) is contained in \(V(S)\), where \(S\) is the initial nonterminal of \(g\).
theorem language_le_of_valuation {V : g.NT → Language T} (hV : IsValuation g V) :
g.language ≤ V g.initialdef IsValuation (g : ContextFreeGrammar T) (V : g.NT → Language T) : Prop :=
∀ r ∈ g.rules, evalForm V r.output ≤ V r.inputCSLibExt/Computability/Languages/ContextFree/Basic.lean:108
Uses 4 · Used by 20
TheoremConcatenating derivations#✓fully proved
Let \(g\) be a context-free grammar and let \(u\), \(u'\), \(v\), \(v'\) be sentential forms of \(g\). If \(u\) derives \(u'\) and \(v\) derives \(v'\) in \(g\) (each in zero or more steps), then the concatenation \(uv\) derives \(u'v'\) in \(g\).
theorem derives_append {u u' v v' : List (Symbol T g.NT)}
(hu : g.Derives u u') (hv : g.Derives v v') :
g.Derives (u ++ v) (u' ++ v')Used by 8
DefinitionRenaming the nonterminals of a symbol#✓fully proved
Given a map \(f\) from nonterminals \(N\) to nonterminals \(N'\), renaming a grammar symbol by \(f\) leaves a terminal \(a\) unchanged and sends a nonterminal \(A\) to the nonterminal \(f(A)\).
def mapSymbol {N' : Type*} (f : N → N') : Symbol T N → Symbol T N'
| .terminal a => .terminal a
| .nonterminal A => .nonterminal (f A)Used by 18
DefinitionRenaming the nonterminals of a production#✓fully proved
Given a map \(f\) from nonterminals \(N\) to nonterminals \(N'\), the renaming by \(f\) of a production \(A \to u\) is the production \(f(A) \to u'\), where \(u'\) is obtained from \(u\) by replacing each nonterminal \(B\) with \(f(B)\) and leaving each terminal unchanged.
def mapRule {N' : Type*} (f : N → N') (r : ContextFreeRule T N) :
ContextFreeRule T N' :=
⟨f r.input, r.output.map (mapSymbol f)⟩def mapSymbol {N' : Type*} (f : N → N') : Symbol T N → Symbol T N'
| .terminal a => .terminal a
| .nonterminal A => .nonterminal (f A)CSLibExt/Computability/Languages/ContextFree/Basic.lean:159
Uses 1 · Used by 15
TheoremInterpretation after renaming nonterminals#✓fully proved
Let \(f \colon N \to N'\) be a map of nonterminals, extended to sentential forms by renaming each nonterminal and keeping each terminal, and let \(V\) assign a language to each nonterminal in \(N'\). For every sentential form \(u\) over \(N\), the language that \(f(u)\) denotes under \(V\) equals the language that \(u\) denotes under the assignment \(V \circ f\).
theorem evalForm_map {N' : Type*} (f : N → N') (V : N' → Language T)
(u : List (Symbol T N)) :
evalForm V (u.map (mapSymbol f)) = evalForm (V ∘ f) udef evalForm (V : N → Language T) : List (Symbol T N) → Language T
| [] => 1
| s :: u => evalSymbol V s * evalForm V uCSLibExt/Computability/Languages/ContextFree/Basic.lean:68
def mapSymbol {N' : Type*} (f : N → N') : Symbol T N → Symbol T N'
| .terminal a => .terminal a
| .nonterminal A => .nonterminal (f A)CSLibExt/Computability/Languages/ContextFree/Basic.lean:159
Uses 2 · Used by 6
TheoremDerivations transfer along a renaming of nonterminals#✓fully proved
Let \(g\) and \(G\) be context-free grammars over the same terminal alphabet, and let \(f\) map the nonterminals of \(g\) to those of \(G\). Extend \(f\) to symbols and sentential forms by renaming each nonterminal and keeping each terminal. Suppose that for every production \(A \to \alpha\) of \(g\), the renamed production \(f(A) \to f(\alpha)\) is a production of \(G\). Then whenever a sentential form \(u\) derives \(v\) in \(g\) (in zero or more steps), \(f(u)\) derives \(f(v)\) in \(G\).
No injectivity of \(f\) is needed for this direction.
theorem derives_map_of_forall_mem {G : ContextFreeGrammar T} {f : g.NT → G.NT}
(hsub : ∀ r ∈ g.rules, mapRule f r ∈ G.rules)
{u v : List (Symbol T g.NT)} (h : g.Derives u v) :
G.Derives (u.map (mapSymbol f)) (v.map (mapSymbol f))def mapRule {N' : Type*} (f : N → N') (r : ContextFreeRule T N) :
ContextFreeRule T N' :=
⟨f r.input, r.output.map (mapSymbol f)⟩CSLibExt/Computability/Languages/ContextFree/Basic.lean:174
def mapSymbol {N' : Type*} (f : N → N') : Symbol T N → Symbol T N'
| .terminal a => .terminal a
| .nonterminal A => .nonterminal (f A)CSLibExt/Computability/Languages/ContextFree/Basic.lean:159
Uses 2 · Used by 5
DefinitionLanguage generated from a nonterminal#✓fully proved
For a context-free grammar \(g\) and a nonterminal \(A\) of \(g\), the language generated by \(g\) from \(A\) is the set of words \(w\) over the terminals of \(g\) such that \(g\) derives \(w\) from the one-symbol sentential form \(A\). It is the language of \(g\) with \(A\) in place of the initial nonterminal.
def languageFrom (g : ContextFreeGrammar T) (A : g.NT) : Language T :=
{ w : List T | g.Derives [Symbol.nonterminal A] (w.map Symbol.terminal) }Used by 34
TheoremWords of the canonical interpretation are derivable#✓fully proved
Let \(g\) be a context-free grammar and assign to each nonterminal \(A\) of \(g\) the language of terminal words that \(g\) derives from \(A\). If a terminal word \(w\) lies in the language that a sentential form \(u\) of \(g\) denotes under this assignment, then \(u\) derives \(w\) in \(g\).
theorem derives_of_mem_evalForm_languageFrom {u : List (Symbol T g.NT)} {w : List T}
(hw : w ∈ evalForm (languageFrom g) u) :
g.Derives u (w.map Symbol.terminal)def evalForm (V : N → Language T) : List (Symbol T N) → Language T
| [] => 1
| s :: u => evalSymbol V s * evalForm V uCSLibExt/Computability/Languages/ContextFree/Basic.lean:68
def languageFrom (g : ContextFreeGrammar T) (A : g.NT) : Language T :=
{ w : List T | g.Derives [Symbol.nonterminal A] (w.map Symbol.terminal) }CSLibExt/Computability/Languages/ContextFree/Basic.lean:219
Uses 4 · Used by 3
TheoremThe languages generated from each nonterminal form a valuation#✓fully proved
For every context-free grammar \(g\), the assignment that sends each nonterminal \(A\) of \(g\) to the language generated by \(g\) from \(A\) is a valuation of \(g\).
theorem isValuation_languageFrom : IsValuation g (languageFrom g)def IsValuation (g : ContextFreeGrammar T) (V : g.NT → Language T) : Prop :=
∀ r ∈ g.rules, evalForm V r.output ≤ V r.inputCSLibExt/Computability/Languages/ContextFree/Basic.lean:108
def languageFrom (g : ContextFreeGrammar T) (A : g.NT) : Language T :=
{ w : List T | g.Derives [Symbol.nonterminal A] (w.map Symbol.terminal) }CSLibExt/Computability/Languages/ContextFree/Basic.lean:219
Uses 4 · Used by 20
TheoremInjective renamings are injective on symbols#✓fully proved
If \(f\) is an injective map from nonterminals \(N\) to nonterminals \(N'\), then renaming grammar symbols by \(f\), which fixes each terminal and sends each nonterminal \(A\) to \(f(A)\), is injective.
theorem mapSymbol_injective {N' : Type*} {f : N → N'} (hf : Function.Injective f) :
Function.Injective (mapSymbol (T := T) f)def mapSymbol {N' : Type*} (f : N → N') : Symbol T N → Symbol T N'
| .terminal a => .terminal a
| .nonterminal A => .nonterminal (f A)CSLibExt/Computability/Languages/ContextFree/Basic.lean:159
Uses 1 · Used by 1
TheoremInjective renamings are injective on productions#✓fully proved
If \(f\) is an injective map from nonterminals \(N\) to nonterminals \(N'\), then renaming the nonterminals of productions over \(N\) by \(f\) is injective: two productions with the same renaming are equal.
In particular, renaming a finite set of productions by \(f\) merges none of them.
theorem mapRule_injective {N' : Type*} {f : N → N'} (hf : Function.Injective f) :
Function.Injective (mapRule (T := T) f)def mapRule {N' : Type*} (f : N → N') (r : ContextFreeRule T N) :
ContextFreeRule T N' :=
⟨f r.input, r.output.map (mapSymbol f)⟩CSLibExt/Computability/Languages/ContextFree/Basic.lean:174
Uses 3 · Used by 7
TheoremRenaming nonterminals fixes terminal words#✓fully proved
Let \(f\) map nonterminals \(N\) to nonterminals \(N'\), and let \(w\) be a word over the terminals. Reading \(w\) as a sentential form over \(N\) and renaming its nonterminals by \(f\) gives \(w\) read as a sentential form over \(N'\).
@[simp]
theorem map_mapSymbol_terminal {N' : Type*} (f : N → N') (w : List T) :
w.map (mapSymbol f ∘ Symbol.terminal) = w.map Symbol.terminaldef mapSymbol {N' : Type*} (f : N → N') : Symbol T N → Symbol T N'
| .terminal a => .terminal a
| .nonterminal A => .nonterminal (f A)CSLibExt/Computability/Languages/ContextFree/Basic.lean:159
Uses 1 · Used by 5
TheoremThe empty language is context-free#✓fully proved
The empty language over any alphabet is context-free: take a grammar with no productions.
theorem IsContextFree.zero : (0 : Language T).IsContextFreeUsed by 1
TheoremThe language of the empty word is context-free#✓fully proved
For every alphabet \(T\), the language over \(T\) whose only word is the empty word is context-free: a grammar with one nonterminal and a single production erasing it generates this language.
theorem IsContextFree.one : (1 : Language T).IsContextFreeUses 3 · Used by 1
TheoremSingleton languages are context-free#✓fully proved
For every word \(w\) over an alphabet \(T\), the language \(\{w\}\) consisting of \(w\) alone is context-free: one production spells the word out.
Uses 4 · Used by 4
InductiveYield of a sentential form#✓fully proved
For a context-free grammar \(g\) with terminal alphabet \(T\), the relation "the sentential form \(u\) yields the terminal word \(w\)" is the smallest relation such that: the empty form yields the empty word; if \(u\) yields \(w\), then for every terminal \(a\) the form \(a u\) yields \(a w\); and if \(A \to \alpha\) is a production of \(g\), \(\alpha\) yields \(w_1\) and \(u\) yields \(w_2\), then the form \(A u\) yields \(w_1 w_2\).
inductive Yields (g : ContextFreeGrammar T) : List (Symbol T g.NT) → List T → Prop
| nil : Yields g [] []
| terminal (a : T) {u : List (Symbol T g.NT)} {w : List T} (h : Yields g u w) :
Yields g (Symbol.terminal a :: u) (a :: w)
| nonterminal {r : ContextFreeRule T g.NT} (hr : r ∈ g.rules)
{u : List (Symbol T g.NT)} {w₁ w₂ : List T}
(hout : Yields g r.output w₁) (hrest : Yields g u w₂) :
Yields g (Symbol.nonterminal r.input :: u) (w₁ ++ w₂)Used by 57
TheoremConcatenation of yields#✓fully proved
Let \(g\) be a context-free grammar. If the sentential form \(u\) yields the terminal word \(w_1\) and the sentential form \(v\) yields the terminal word \(w_2\), then the concatenated form \(u v\) yields \(w_1 w_2\).
theorem Yields.append {u v : List (Symbol T g.NT)} {w₁ w₂ : List T}
(hu : Yields g u w₁) (hv : Yields g v w₂) : Yields g (u ++ v) (w₁ ++ w₂)inductive Yields (g : ContextFreeGrammar T) : List (Symbol T g.NT) → List T → Prop
| nil : Yields g [] []
| terminal (a : T) {u : List (Symbol T g.NT)} {w : List T} (h : Yields g u w) :
Yields g (Symbol.terminal a :: u) (a :: w)
| nonterminal {r : ContextFreeRule T g.NT} (hr : r ∈ g.rules)
{u : List (Symbol T g.NT)} {w₁ w₂ : List T}
(hout : Yields g r.output w₁) (hrest : Yields g u w₂) :
Yields g (Symbol.nonterminal r.input :: u) (w₁ ++ w₂)CSLibExt/Computability/Languages/ContextFree/Yields.lean:48
Uses 1 · Used by 12
TheoremSplitting a yield over a concatenation#✓fully proved
Let \(g\) be a context-free grammar. If the concatenated sentential form \(u v\) yields the terminal word \(w\), then there are terminal words \(w_1\) and \(w_2\) with \(w = w_1 w_2\) such that \(u\) yields \(w_1\) and \(v\) yields \(w_2\).
theorem Yields.append_inv {u v : List (Symbol T g.NT)} {w : List T}
(h : Yields g (u ++ v) w) :
∃ w₁ w₂, w = w₁ ++ w₂ ∧ Yields g u w₁ ∧ Yields g v w₂inductive Yields (g : ContextFreeGrammar T) : List (Symbol T g.NT) → List T → Prop
| nil : Yields g [] []
| terminal (a : T) {u : List (Symbol T g.NT)} {w : List T} (h : Yields g u w) :
Yields g (Symbol.terminal a :: u) (a :: w)
| nonterminal {r : ContextFreeRule T g.NT} (hr : r ∈ g.rules)
{u : List (Symbol T g.NT)} {w₁ w₂ : List T}
(hout : Yields g r.output w₁) (hrest : Yields g u w₂) :
Yields g (Symbol.nonterminal r.input :: u) (w₁ ++ w₂)CSLibExt/Computability/Languages/ContextFree/Yields.lean:48
Uses 1 · Used by 6
TheoremYield through one production#✓fully proved
Let \(g\) be a context-free grammar and \(A \to \alpha\) a production of \(g\). If \(\alpha\) yields the terminal word \(w\), then the one-symbol sentential form \(A\) yields \(w\).
theorem yields_of_rule {r : ContextFreeRule T g.NT} (hr : r ∈ g.rules) {w : List T}
(hout : Yields g r.output w) : Yields g [Symbol.nonterminal r.input] winductive Yields (g : ContextFreeGrammar T) : List (Symbol T g.NT) → List T → Prop
| nil : Yields g [] []
| terminal (a : T) {u : List (Symbol T g.NT)} {w : List T} (h : Yields g u w) :
Yields g (Symbol.terminal a :: u) (a :: w)
| nonterminal {r : ContextFreeRule T g.NT} (hr : r ∈ g.rules)
{u : List (Symbol T g.NT)} {w₁ w₂ : List T}
(hout : Yields g r.output w₁) (hrest : Yields g u w₂) :
Yields g (Symbol.nonterminal r.input :: u) (w₁ ++ w₂)CSLibExt/Computability/Languages/ContextFree/Yields.lean:48
Uses 1 · Used by 17
TheoremYields are derivable#✓fully proved
Let \(g\) be a context-free grammar. If the sentential form \(u\) yields the terminal word \(w\), then \(u\) derives \(w\), read as a string of terminal symbols, in \(g\): that is, \(u \Rightarrow^* w\) in zero or more rewriting steps.
theorem derives_of_yields {u : List (Symbol T g.NT)} {w : List T}
(h : Yields g u w) : g.Derives u (w.map Symbol.terminal)inductive Yields (g : ContextFreeGrammar T) : List (Symbol T g.NT) → List T → Prop
| nil : Yields g [] []
| terminal (a : T) {u : List (Symbol T g.NT)} {w : List T} (h : Yields g u w) :
Yields g (Symbol.terminal a :: u) (a :: w)
| nonterminal {r : ContextFreeRule T g.NT} (hr : r ∈ g.rules)
{u : List (Symbol T g.NT)} {w₁ w₂ : List T}
(hout : Yields g r.output w₁) (hrest : Yields g u w₂) :
Yields g (Symbol.nonterminal r.input :: u) (w₁ ++ w₂)CSLibExt/Computability/Languages/ContextFree/Yields.lean:48
Uses 2 · Used by 2
TheoremDerivable terminal words are yields#✓fully proved
Let \(g\) be a context-free grammar. If the sentential form \(u\) derives the terminal word \(w\), read as a string of terminal symbols, in \(g\), then \(u\) yields \(w\).
The proof is the valuation argument: the languages yielded by the nonterminals form a valuation.
theorem yields_of_derives {u : List (Symbol T g.NT)} {w : List T}
(h : g.Derives u (w.map Symbol.terminal)) : Yields g u winductive Yields (g : ContextFreeGrammar T) : List (Symbol T g.NT) → List T → Prop
| nil : Yields g [] []
| terminal (a : T) {u : List (Symbol T g.NT)} {w : List T} (h : Yields g u w) :
Yields g (Symbol.terminal a :: u) (a :: w)
| nonterminal {r : ContextFreeRule T g.NT} (hr : r ∈ g.rules)
{u : List (Symbol T g.NT)} {w₁ w₂ : List T}
(hout : Yields g r.output w₁) (hrest : Yields g u w₂) :
Yields g (Symbol.nonterminal r.input :: u) (w₁ ++ w₂)CSLibExt/Computability/Languages/ContextFree/Yields.lean:48
Uses 7 · Used by 2
TheoremYields coincide with derivations of terminal words#✓fully proved
Let \(g\) be a context-free grammar, \(u\) a sentential form of \(g\) and \(w\) a word of terminals. Then \(u\) yields \(w\) in \(g\) if and only if \(u\) derives in \(g\), by zero or more rewriting steps, the sentential form consisting of the letters of \(w\) read as terminals.
theorem yields_iff_derives {u : List (Symbol T g.NT)} {w : List T} :
Yields g u w ↔ g.Derives u (w.map Symbol.terminal)inductive Yields (g : ContextFreeGrammar T) : List (Symbol T g.NT) → List T → Prop
| nil : Yields g [] []
| terminal (a : T) {u : List (Symbol T g.NT)} {w : List T} (h : Yields g u w) :
Yields g (Symbol.terminal a :: u) (a :: w)
| nonterminal {r : ContextFreeRule T g.NT} (hr : r ∈ g.rules)
{u : List (Symbol T g.NT)} {w₁ w₂ : List T}
(hout : Yields g r.output w₁) (hrest : Yields g u w₂) :
Yields g (Symbol.nonterminal r.input :: u) (w₁ ++ w₂)CSLibExt/Computability/Languages/ContextFree/Yields.lean:48
Uses 3 · Used by 5
TheoremLanguage membership through yields#✓fully proved
Let \(g\) be a context-free grammar with initial nonterminal \(S\). A terminal word \(w\) belongs to the language of \(g\) if and only if the one-symbol sentential form \(S\) yields \(w\).
theorem mem_language_iff_yields {w : List T} :
w ∈ g.language ↔ Yields g [Symbol.nonterminal g.initial] winductive Yields (g : ContextFreeGrammar T) : List (Symbol T g.NT) → List T → Prop
| nil : Yields g [] []
| terminal (a : T) {u : List (Symbol T g.NT)} {w : List T} (h : Yields g u w) :
Yields g (Symbol.terminal a :: u) (a :: w)
| nonterminal {r : ContextFreeRule T g.NT} (hr : r ∈ g.rules)
{u : List (Symbol T g.NT)} {w₁ w₂ : List T}
(hout : Yields g r.output w₁) (hrest : Yields g u w₂) :
Yields g (Symbol.nonterminal r.input :: u) (w₁ ++ w₂)CSLibExt/Computability/Languages/ContextFree/Yields.lean:48
Uses 2 · Used by 17
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.