rewrites_reverse_comm — Mathlib

English

Let r be a ContextFreeRule and u, v lists of symbols. Then the reverse rewrite relation is equivalent to rewriting the reversed lists with the reversed rule: r.reverse.Rewrites(u, v) if and only if r.Rewrites(u.reverse, v.reverse).

Русский

Пусть r — правило контекстно-свободной грамматики и u, v — списки символов. Тогда переписывания с разворотом равноправны: r.reverse.Rewrites(u, v) эквивалентно r.Rewrites(u.reverse, v.reverse).

LaTeX

$$$ r.^{\mathrm{rev}}.\Rewrites\bigl(u, v\bigr) \;\iff\; r.\Rewrites\bigl(u^{\mathrm{rev}}, v^{\mathrm{rev}}\bigr) $$$

Lean4

@[simp]
theorem rewrites_reverse_comm : r.reverse.Rewrites u v ↔ r.Rewrites u.reverse v.reverse := by
  rw [← rewrites_reverse, reverse_reverse]

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