rewrites_iff — Mathlib

English

If u rewrites to v, then for any prefix p, p ++ u rewrites to p ++ v.

Русский

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

LaTeX

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

Lean4

/-- Rule `r` rewrites string `u` is to string `v` iff they share both a prefix `p` and postfix `q`
such that the remaining middle part of `u` is the input of `r` and the remaining middle part
of `u` is the output of `r`. -/
theorem rewrites_iff :
    r.Rewrites u v ↔ ∃ p q : List (Symbol T N), u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q :=
  ⟨Rewrites.exists_parts, by rintro ⟨p, q, rfl, rfl⟩; apply rewrites_of_exists_parts⟩

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