trTape_mk'

Mathlib.Computability.PostTuringMachine

URI: https://scilib.ai/kg/mathlib#Turing.TM1to1.trTape_mk'

English

Equivalence between trTape transitions under left/right moves.

Русский

Эквивалентность переходов trTape при сдвигах влево/вправо.

LaTeX

$$trTape_move (enc0) (L,R) : trTape enc0 (Tape.mk' L R) = trTape enc0 (Tape.mk' L' R')$$

Lean4

theorem trTape_mk' (L R : ListBlank Γ) : trTape enc0 (Tape.mk' L R) = trTape' enc0 L R := by
  simp only [trTape, Tape.mk'_left, Tape.mk'_right₀]

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

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

Разделы

Аффилиация

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