Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case refine_2
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (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')

pp: case refine_3
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (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')

pp: case refine_4
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (l : σ → Λ),
    TM2.SupportsStmt S (TM2.Stmt.goto l) →
      (∀ x ∈ trStmts₁ (TM2.Stmt.goto l), x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l)) ∧
          ∀ l' ∈ trStmts₁ (TM2.Stmt.goto l), TM1.SupportsStmt (trSupp M S) (tr M l')

pp: case refine_5
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
⊢ TM2.SupportsStmt S TM2.Stmt.halt →
    (∀ x ∈ trStmts₁ TM2.Stmt.halt, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧
        ∀ l' ∈ trStmts₁ TM2.Stmt.halt, TM1.SupportsStmt (trSupp M S) (tr M l')

Tactic:
· intro _ _ IH ss' sub -- load
      unfold TM2to1.trStmts₁ at sub ⊢
      exact IH ss' sub

Goal state after:
case refine_3
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (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')

case refine_4
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (l : σ → Λ),
    TM2.SupportsStmt S (TM2.Stmt.goto l) →
      (∀ x ∈ trStmts₁ (TM2.Stmt.goto l), x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l)) ∧
          ∀ l' ∈ trStmts₁ (TM2.Stmt.goto l), TM1.SupportsStmt (trSupp M S) (tr M l')

case refine_5
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
⊢ TM2.SupportsStmt S TM2.Stmt.halt →
    (∀ x ∈ trStmts₁ TM2.Stmt.halt, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧
        ∀ l' ∈ trStmts₁ TM2.Stmt.halt, TM1.SupportsStmt (trSupp M S) (tr M l')