exists_parts — Mathlib

English

Every rewrite u → v for a context-free rule r can be decomposed into a prefix, the input Nonterminal, and a suffix, with v correspondingly built from the prefix and the rule output.

Русский

Любое правило вывода можно разложить на префикс, входной непроизводимый символ и суффикс, а строка v строится по префиксу и выводу правила.

LaTeX

$$There exist p,q with u = p ++ [nonterminal r.input] ++ q and v = p ++ r.output ++ q.$$

Lean4

theorem exists_parts (hr : r.Rewrites u v) :
    ∃ p q : List (Symbol T N), u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q := by
  induction hr with
  | head s =>
    use [], s
    simp
  | cons x _ ih =>
    rcases ih with ⟨p', q', rfl, rfl⟩
    use x :: p', q'
    simp

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