English
Let g be a context-free grammar and w a word (list of terminals). Then w belongs to the language generated by g if and only if the initial nonterminal derives the terminal-wrapped version of w.
Русский
Пусть g — контекстно-свободная грамматика и w — слово (список терминалов). Тогда w принадлежит языку, генерируемому g, iff начальный нетерминал выводит терминальное отображение w.
LaTeX
$$$w \in g.language \iff g.Derives([Symbol.nonterminal\; g.initial], (w.map\; Symbol.terminal))$$$
Lean4
/-- A given word `w` belongs to the language generated by a given context-free grammar `g` iff
`g` can derive the word `w` (wrapped as a string) from the initial nonterminal of `g` in some
number of steps. -/
@[simp]
theorem mem_language_iff (g : ContextFreeGrammar T) (w : List T) :
w ∈ g.language ↔ g.Derives [Symbol.nonterminal g.initial] (w.map Symbol.terminal) := by rfl
