Theorems · Theorem · logic and foundations

Turing.TM1to1.stepAux_move

∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (d : Turing.Dir)
  (q : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ) (v : σ) (T : Turing.Tape Bool),
  Turing.TM1.stepAux (Turing.TM1to1.move n d q) v T = Turing.TM1.stepAux q v ((Turing.Tape.move d)^[n] T)

Defined in

Mathlib.Computability.TuringMachine.PostTuringMachine

Cited by

2 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound