append_right — Mathlib

English

If v is produced to w, then for any postfix p, v ++ p is produced to w ++ p.

Русский

Если v порождается в w, то для любого постфикса p v ++ p порождает w ++ p.

LaTeX

$$$\forall v\forall w,\ g.Produces\ v\ w \Rightarrow \forall p,\ g.Produces\ (v ++ p)\ (w ++ p)$$$

Lean4

/-- Add extra postfix to context-free producing. -/
theorem append_right {v w : List (Symbol T g.NT)} (hvw : g.Produces v w) (p : List (Symbol T g.NT)) :
    g.Produces (v ++ p) (w ++ p) :=
  match hvw with
  | ⟨r, hrmem, hrvw⟩ => ⟨r, hrmem, hrvw.append_right p⟩

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