nonterminal_input_mem

Mathlib.Computability.ContextFreeGrammar

URI: https://scilib.ai/kg/mathlib#ContextFreeRule.Rewrites.nonterminal_input_mem

English

If r.Rewrites u v, then the nonterminal r.input occurs in u.

Русский

Если есть выкладка r.Rewrites u v, то в строке u встречается не терминал r.input.

LaTeX

$$$ r.Rewrites u v \rightarrow \text{Symbol.nonterminal } r.input \in u $$$

Lean4

theorem nonterminal_input_mem : r.Rewrites u v → .nonterminal r.input ∈ u := by
  simp +contextual [rewrites_iff, List.append_assoc]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru