Theorems · Theorem · logic and foundations

Turing.TM1to0.tr_respects

∀ {Γ : Type u_1} {Λ : Type u_2} [inst : Inhabited Λ] {σ : Type u_3} [inst_1 : Inhabited σ]
  (M : Λ → Turing.TM1.Stmt Γ Λ σ) [inst_2 : Inhabited Γ],
  StateTransition.Respects (Turing.TM1.step M) (Turing.TM0.step (Turing.TM1to0.tr M)) fun c₁ c₂ =>
    Turing.TM1to0.trCfg M c₁ = c₂

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

InhabitedInhabitedInhabited