rewrites_of_exists_parts — Mathlib

English

If r.Rewrites u v, there exist p,q such that u = p ++ [nonterminal input] ++ q and v = p ++ output ++ q.

Русский

Если r.Rewrites u v, существуют p,q такие что u = p ++ [nonterminal input] ++ q и v = p ++ output ++ q.

LaTeX

$$$\exists p,q : List(\text{Symbol } T N),\ u = p ++ [\text{Symbol.nonterminal } r.input] ++ q \wedge\ v = p ++ r.output ++ q$$$

Lean4

theorem rewrites_of_exists_parts (r : ContextFreeRule T N) (p q : List (Symbol T N)) :
    r.Rewrites (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q) := by
  induction p with
  | nil => exact Rewrites.head q
  | cons d l ih => exact Rewrites.cons d ih

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