append_right — Mathlib

English

Let r be a context-free rewriting rule. If u rewrites to v under r, then for every postfix p, the concatenation u ++ p rewrites to v ++ p under r.

Русский

Пусть r — правило переписывания контекстно свободной грамматики. Если u переходит в v при помощи r, то для любого постфикса p последовательности u ++ p будет переходить в v ++ p под тем же правилом.

LaTeX

$$$\forall r\; \forall u\forall v\forall p,\; r.Rewrites\, u\, v \Rightarrow r.Rewrites\, (u \\;++\\; p) \\; (v \\;++\\; p)$$$

Lean4

/-- Add extra postfix to context-free rewriting. -/
theorem append_right (hvw : r.Rewrites u v) (p : List (Symbol T N)) : r.Rewrites (u ++ p) (v ++ p) :=
  by
  rw [rewrites_iff] at *
  rcases hvw with ⟨x, y, hxy⟩
  use x, y ++ p
  simp_all

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