exists_nonterminal_input_mem — Mathlib

English

If g.Produces u v, then there exists a rule r with r in g.rules such that the nonterminal r.input is in u.

Русский

Если g.Produces u v, то существует правило r из g.rules, у которого входной нетерминал r.input встречается в u.

LaTeX

$$$\exists r \in g.rules, .nonterminal r.input \in u$$$

Lean4

theorem exists_nonterminal_input_mem {u v : List (Symbol T g.NT)} (hguv : g.Produces u v) :
    ∃ r ∈ g.rules, .nonterminal r.input ∈ u := by
  obtain ⟨w, l, r⟩ := hguv
  exact ⟨w, l, r.nonterminal_input_mem⟩

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