rewrites_reverse — Mathlib

English

Let r be a context-free rule on symbols, and let u and v be lists of symbols. Then reversing both the rule and the lists preserves the rewrite relation: r.reverse.Rewrites(u.reverse, v.reverse) holds if and only if r.Rewrites(u, v).

Русский

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

LaTeX

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

Lean4

theorem rewrites_reverse : r.reverse.Rewrites u.reverse v.reverse ↔ r.Rewrites u v :=
  ⟨fun h ↦ by simpa using h.reverse, .reverse⟩

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