Theorems · Theorem · logic and foundations

Turing.TM0.Machine.map_respects

∀ {Γ : Type u_1} [inst : Inhabited Γ] {Γ' : Type u_2} [inst_1 : Inhabited Γ'] {Λ : Type u_3} [inst_2 : Inhabited Λ]
  {Λ' : Type u_4} [inst_3 : Inhabited Λ'] (M : Turing.TM0.Machine Γ Λ) (f₁ : Turing.PointedMap Γ Γ')
  (f₂ : Turing.PointedMap Γ' Γ) (g₁ : Turing.PointedMap Λ Λ') (g₂ : Λ' → Λ) {S : Set Λ},
  Turing.TM0.Supports M S →
    Function.RightInverse f₁.f f₂.f →
      (∀ q ∈ S, g₂ (g₁.f q) = q) →
        StateTransition.Respects (Turing.TM0.step M) (Turing.TM0.step (M.map f₁ f₂ g₁.f g₂)) fun a b =>
          a.q ∈ S ∧ Turing.TM0.Cfg.map f₁ g₁.f a = b

Defined in

Mathlib.Computability.TuringMachine.PostTuringMachine

Cited by

0 results in Mathlib

Foundations

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

Assumes

InhabitedInhabitedInhabitedInhabited