produces_reverse — Mathlib

English

Reversing a context-free grammar preserves the Produces relation up to reversal; g.reverse.Produces(u.reverse, v.reverse) is equivalent to g.Produces(u, v).

Русский

Разворот грамматики сохраняет отношение Produces с учётом разворота: g.reverse.Produces(u.reverse, v.reverse) эквивалентно g.Produces(u, v).

LaTeX

$$$ g.reverse.Produces\bigl(u.reverse, v.reverse\bigr) \iff g.Produces\bigl(u, v\bigr) $$$

Lean4

theorem produces_reverse : g.reverse.Produces u.reverse v.reverse ↔ g.Produces u v :=
  (Equiv.ofBijective _ ContextFreeRule.reverse_bijective).exists_congr
    (by simp [ContextFreeRule.reverse_involutive.eq_iff])

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