Theorems · Theorem · logic and foundations

Turing.TM1to1.tr_respects

∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} {enc : Γ → List.Vector Bool n} (dec : List.Vector Bool n → Γ)
  (M : Λ → Turing.TM1.Stmt Γ Λ σ) [inst : Inhabited Γ] {enc0 : enc default = List.Vector.replicate n false},
  (∀ (a : Γ), dec (enc a) = a) →
    StateTransition.Respects (Turing.TM1.step M) (Turing.TM1.step (Turing.TM1to1.tr enc dec M)) fun c₁ c₂ =>
      Turing.TM1to1.trCfg enc enc0 c₁ = c₂

Defined in

Mathlib.Computability.TuringMachine.PostTuringMachine

Cited by

0 results in Mathlib

Foundations

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

Assumes

Inhabited