-- 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 Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
refine_1 :
  ∀ (k : K) (s : StAct K Γ σ k) (q : TM2.Stmt Γ Λ σ),
    (TM2.SupportsStmt (Γ := Γ) S q →
        (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
            ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')) →
      TM2.SupportsStmt (Γ := Γ) S (stRun (Γ := Γ) s q) →
        (∀ x ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), x ∈ trSupp (Γ := Γ) M S) →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (stRun (Γ := Γ) s q)) ∧
            ∀ l' ∈ trStmts₁ (Γ := Γ) (stRun (Γ := Γ) s q), TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
refine_2 :
  ∀ (a : σ → σ) (q : TM2.Stmt Γ Λ σ),
    (TM2.SupportsStmt (Γ := Γ) S q →
        (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
            ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')) →
      TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.load (Γ := Γ) a q) →
        (∀ x ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q), x ∈ trSupp (Γ := Γ) M S) →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q)) ∧
            ∀ l' ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.load (Γ := Γ) a q),
              TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
refine_3 :
  ∀ (p : σ → Bool) (q₁ q₂ : TM2.Stmt Γ Λ σ),
    (TM2.SupportsStmt (Γ := Γ) S q₁ →
        (∀ x ∈ trStmts₁ (Γ := Γ) q₁, x ∈ trSupp (Γ := Γ) M S) →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₁) ∧
            ∀ l' ∈ trStmts₁ (Γ := Γ) q₁, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')) →
      (TM2.SupportsStmt (Γ := Γ) S q₂ →
          (∀ x ∈ trStmts₁ (Γ := Γ) q₂, x ∈ trSupp (Γ := Γ) M S) →
            TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q₂) ∧
              ∀ l' ∈ trStmts₁ (Γ := Γ) q₂, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')) →
        TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.branch (Γ := Γ) p q₁ q₂) →
          (∀ x ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂), x ∈ trSupp (Γ := Γ) M S) →
            TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂)) ∧
              ∀ l' ∈ trStmts₁ (Γ := Γ) (TM2.Stmt.branch (Γ := Γ) p q₁ q₂),
                TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
refine_4 :
  ∀ (l : σ → Λ),
    TM2.SupportsStmt (Γ := Γ) S (TM2.Stmt.goto (Γ := Γ) l) →
      (∀ (x : Λ' K Γ Λ σ),
          Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) x →
            x ∈ trSupp (Γ := Γ) M S) →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) ∧
          ∀ (l' : Λ' K Γ Λ σ),
            Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l)) l' →
              TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
refine_5 :
  TM2.SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (TM2.Stmt.halt (Γ := Γ)) →
    (∀ (x : Λ' K Γ Λ σ),
        Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) x →
          x ∈ trSupp (Γ := Γ) M S) →
      TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) ∧
        ∀ (l' : Λ' K Γ Λ σ),
          Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) l' →
            TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ ∀ (q : TM2.Stmt Γ Λ σ),
    TM2.SupportsStmt (Γ := Γ) S q →
      (∀ x ∈ trStmts₁ (Γ := Γ) q, x ∈ trSupp (Γ := Γ) M S) →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) q) ∧
          ∀ l' ∈ trStmts₁ (Γ := Γ) q, TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
refine stmtStRec ?_ ?_ ?_ ?_ ?_