Theorems · Theorem · logic and foundations

Turing.TM2to1.trNormal_run

∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {k : K} (s : Turing.TM2to1.StAct K Γ σ k)
  (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.trNormal (Turing.TM2to1.stRun s q) = Turing.TM1.Stmt.goto fun x x_1 => Turing.TM2to1.Λ'.go k s q

Defined in

Mathlib.Computability.TuringMachine.StackTuringMachine

Cited by

2 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms