Theorems · Theorem · logic and foundations

Turing.TM0.Machine.map_step

∀ {Γ : 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₁ : Λ → Λ') (g₂ : Λ' → Λ) {S : Set Λ},
  Function.RightInverse f₁.f f₂.f →
    (∀ q ∈ S, g₂ (g₁ q) = q) →
      ∀ (c : Turing.TM0.Cfg Γ Λ),
        c.q ∈ S →
          Option.map (Turing.TM0.Cfg.map f₁ g₁) (Turing.TM0.step M c) =
            Turing.TM0.step (M.map f₁ f₂ g₁ g₂) (Turing.TM0.Cfg.map f₁ g₁ c)

Defined in

Mathlib.Computability.TuringMachine.PostTuringMachine

Cited by

1 results in Mathlib

Foundations

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

Assumes

InhabitedInhabitedInhabitedInhabited