English
If every rule's input is different from a fixed nonterminal t, then from the initial nonterminal, you cannot derive any string that begins with t in a prohibited way; in particular, certain strings cannot be derived.
Русский
Если для всех правил вход не равен фиксированному нетерминалу t, тогда из начального нетерминала нельзя вывести строку, начинающуюся с t в запрещенной конфигурации.
LaTeX
$$$\forall t,\ (\forall r \in g.rules, r.input \neq t) \Rightarrow \forall s, s \neq [.nonterminal\ t] \Rightarrow ¬ g.Derives [.nonterminal\ t] s$$$
Lean4
theorem derives_nonterminal {t : g.NT} (hgt : ∀ r ∈ g.rules, r.input ≠ t) (s : List (Symbol T g.NT))
(hs : s ≠ [.nonterminal t]) : ¬g.Derives [.nonterminal t] s :=
by
rw [derives_iff_eq_or_head]
push_neg
refine ⟨hs.symm, fun _ hx ↦ ?_⟩
have hxr := hx.exists_nonterminal_input_mem
simp_rw [List.mem_singleton, Symbol.nonterminal.injEq] at hxr
tauto
