Theorems · Definition · logic and foundations

Turing.TM1to1.move

{Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      ℕ → Turing.Dir → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ

A move left or right corresponds to n moves across the super-cell.

Defined in

Mathlib.Computability.TuringMachine.PostTuringMachine

Cited by

6 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms