Theorems · Definition · logic and foundations

Turing.TM2to1.tr

{K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} →
        [DecidableEq K] →
          (Λ → Turing.TM2.Stmt Γ Λ σ) →
            Turing.TM2to1.Λ' K Γ Λ σ → Turing.TM1.Stmt (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ

The TM2 emulator machine states written as a TM1 program. This handles the go and ret states, which shuttle to and from a stack top.

Defined in

Mathlib.Computability.TuringMachine.StackTuringMachine

Cited by

7 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

DecidableEq