reverse_reverse

Mathlib.Computability.ContextFreeGrammar

URI: https://scilib.ai/kg/mathlib#ContextFreeRule.reverse_reverse

English

For any rule r, reversing twice returns the original rule: reverse(reverse(r)) = r.

Русский

Для любого правила r двойной разворот возвращает исходное правило: reverse(reverse(r)) = r.

LaTeX

$$$\forall r,\; r.reverse\.reverse = r$$$

Lean4

@[simp]
theorem reverse_reverse (r : ContextFreeRule T N) : r.reverse.reverse = r := by simp [reverse]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru