Theorems · Theorem · logic and foundations

Turing.TM1to1.stepAux_write

∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} {enc : Γ → List.Vector Bool n} [inst : Inhabited Γ]
  (enc0 : enc default = List.Vector.replicate n false) (q : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ) (v : σ)
  (a b : Γ) (L R : Turing.ListBlank Γ),
  Turing.TM1.stepAux (Turing.TM1to1.write (enc a).toList q) v
      (Turing.TM1to1.trTape' enc0 L (Turing.ListBlank.cons b R)) =
    Turing.TM1.stepAux q v (Turing.TM1to1.trTape' enc0 (Turing.ListBlank.cons a L) R)

Defined in

Mathlib.Computability.TuringMachine.PostTuringMachine

Cited by

1 results in Mathlib

Foundations

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

Assumes

Inhabited