reverse_reverse

Mathlib.Computability.NFA

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

English

Taking the reverse of an automaton twice returns the original automaton.

Русский

Дважды применяя операцию разворота к автомату, получаем исходный автомат.

LaTeX

$$$M.reverse.reverse = M$$$

Lean4

@[simp]
theorem reverse_reverse : M.reverse.reverse = M := by simp [reverse]

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

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

Разделы

Аффилиация

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