append_left — Mathlib

English

The append_left theorem states that pre-pending a fixed context to both sides preserves rewrites.

Русский

Теорема добавления слева утверждает, что добавление фиксированного контекста слева сохраняет выводы.

LaTeX

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

Lean4

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

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