Theorems · Theorem · logic and foundations

Turing.TM2to1.tr_respects_aux

∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ)
  {q : Turing.TM2.Stmt Γ Λ σ} {v : σ} {T : Turing.ListBlank ((i : K) → Option (Γ i))} {k : K}
  {S : (k : K) → List (Γ k)},
  (∀ (k : K), Turing.ListBlank.map (Turing.proj k) T = Turing.ListBlank.mk (List.map some (S k)).reverse) →
    ∀ (o : Turing.TM2to1.StAct K Γ σ k),
      (∀ {v : σ} {S : (k : K) → List (Γ k)} {T : Turing.ListBlank ((k : K) → Option (Γ k))},
          (∀ (k : K), Turing.ListBlank.map (Turing.proj k) T = Turing.ListBlank.mk (List.map some (S k)).reverse) →
            ∃ b,
              Turing.TM2to1.TrCfg (Turing.TM2.stepAux q v S) b ∧
                StateTransition.Reaches (Turing.TM1.step (Turing.TM2to1.tr M))
                  (Turing.TM1.stepAux (Turing.TM2to1.trNormal q) v (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom T))) b) →
        ∃ b,
          Turing.TM2to1.TrCfg (Turing.TM2.stepAux (Turing.TM2to1.stRun o q) v S) b ∧
            StateTransition.Reaches (Turing.TM1.step (Turing.TM2to1.tr M))
              (Turing.TM1.stepAux (Turing.TM2to1.trNormal (Turing.TM2to1.stRun o q)) v
                (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom T)))
              b

Defined in

Mathlib.Computability.TuringMachine.StackTuringMachine

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEq