language_eq_zero_of_forall_input_ne_initial

English

If every rule's input is different from the initial nonterminal, then the language of g is empty (0).

Русский

Если каждый вход правила отличается от начального нетерминала, язык g пуст.

LaTeX

$$$(\forall r \in g.rules, r.input \neq g.initial) \Rightarrow g.language = 0$$$

Lean4

theorem language_eq_zero_of_forall_input_ne_initial (hg : ∀ r ∈ g.rules, r.input ≠ g.initial) : g.language = 0 := by
  ext; simp +contextual [derives_nonterminal, hg]

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