Theorems · Theorem · logic and foundations

Turing.TM2to1.tr_eval

∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ)
  [inst_1 : Inhabited Λ] [inst_2 : Inhabited σ] (k : K) (L : List (Γ k)) {L₁ : Turing.ListBlank (Turing.TM2to1.Γ' K Γ)}
  {L₂ : List (Γ k)},
  L₁ ∈ Turing.TM1.eval (Turing.TM2to1.tr M) (Turing.TM2to1.trInit k L) →
    L₂ ∈ Turing.TM2.eval M k L →
      ∃ S L',
        Turing.TM2to1.addBottom L' = L₁ ∧
          (∀ (k : K), Turing.ListBlank.map (Turing.proj k) L' = Turing.ListBlank.mk (List.map some (S k)).reverse) ∧
            S k = L₂

Defined in

Mathlib.Computability.TuringMachine.StackTuringMachine

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqInhabitedInhabited