-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
l : Λ
N : TM2.Stmt Γ Λ σ
run :
  ∀ (k : K) (s : StAct K Γ σ k) (q : TM2.Stmt Γ Λ σ)
    (IH :
      ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
        (hT :
          ∀ (k : K),
            ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
        ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
          TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) q v S) b ∧
            Reaches (TM1.step (tr (Γ := Γ) M)) (TM1.stepAux (trNormal (Γ := Γ) q) v (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
              b)
    {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
    (hT :
      ∀ (k : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
    ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
      TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) (stRun (Γ := Γ) s q) v S) b ∧
        Reaches (TM1.step (tr (Γ := Γ) M))
          (TM1.stepAux (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b
load :
  ∀ (a : σ → σ) (q : TM2.Stmt Γ Λ σ)
    (IH :
      ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
        (hT :
          ∀ (k : K),
            ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
        ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
          TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) q v S) b ∧
            Reaches (TM1.step (tr (Γ := Γ) M)) (TM1.stepAux (trNormal (Γ := Γ) q) v (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
              b)
    {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
    (hT :
      ∀ (k : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
    ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
      TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q) v S) b ∧
        Reaches (TM1.step (tr (Γ := Γ) M))
          (TM1.stepAux (trNormal (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q)) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b
branch :
  ∀ (p : σ → Bool) (q₁ q₂ : TM2.Stmt Γ Λ σ)
    (IH₁ :
      ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
        (hT :
          ∀ (k : K),
            ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
        ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
          TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) q₁ v S) b ∧
            Reaches (TM1.step (tr (Γ := Γ) M))
              (TM1.stepAux (trNormal (Γ := Γ) q₁) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b)
    (IH₂ :
      ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
        (hT :
          ∀ (k : K),
            ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
        ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
          TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) q₂ v S) b ∧
            Reaches (TM1.step (tr (Γ := Γ) M))
              (TM1.stepAux (trNormal (Γ := Γ) q₂) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b)
    {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
    (hT :
      ∀ (k : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
    ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
      TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂) v S) b ∧
        Reaches (TM1.step (tr (Γ := Γ) M))
          (TM1.stepAux (trNormal (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b
goto :
  ∀ (l : σ → Λ) {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
    (hT :
      ∀ (k : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
    ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
      TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l) v S) b ∧
        Reaches (TM1.step (tr (Γ := Γ) M))
          (TM1.stepAux (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b
halt :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k)))
    (hT :
      ∀ (k : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse),
    ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
      TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) (TM2.Stmt.halt (Γ := Γ)) v S) b ∧
        Reaches (TM1.step (tr (Γ := Γ) M))
          (TM1.stepAux (trNormal (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b
⊢ ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) N v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M)) (TM1.stepAux (trNormal (Γ := Γ) N) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b

Tactic:
induction N using stmtStRec generalizing v S L hT with
  | run k s q IH => exact tr_respects_aux M hT s @IH
  | load a _ IH => exact IH _ hT
  | branch p q₁ q₂ IH₁ IH₂ =>
    unfold TM2.stepAux trNormal TM1.stepAux
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/12129): additional beta reduction needed
    beta_reduce
    cases p v <;> [exact IH₂ _ hT; exact IH₁ _ hT]
  | goto => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
  | halt => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩

Premises used: Turing.TM2.stepAux, Turing.TM2to1.trNormal, Turing.TM1.stepAux, Turing.TM1.Stmt.halt, Turing.TM1.Stmt.goto, Turing.TM1.Stmt.load, Turing.TM1.Stmt.branch