Theorems · Theorem · logic and foundations

Turing.TM1to1.stepAux_read

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

Defined in

Mathlib.Computability.TuringMachine.PostTuringMachine

Cited by

1 results in Mathlib

Foundations

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

Assumes

Inhabited