Theorems · Theorem · logic and foundations

Turing.TM0to1.tr_respects

∀ {Γ : Type u_1} [inst : Inhabited Γ] {Λ : Type u_2} [inst_1 : Inhabited Λ] (M : Turing.TM0.Machine Γ Λ),
  StateTransition.Respects (Turing.TM0.step M) (Turing.TM1.step (Turing.TM0to1.tr M)) fun a b =>
    Turing.TM0to1.trCfg M a = b

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

InhabitedInhabited