-- 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 Γ Λ σ
l : Λ
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
branch :
  ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ) (bif false then TM2.stepAux (Γ := Γ) q₁ v S else TM2.stepAux (Γ := Γ) q₂ v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (bif false then TM1.stepAux (trNormal (Γ := Γ) q₁) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))
        else TM1.stepAux (trNormal (Γ := Γ) q₂) v (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
        b
branch₁ :
  ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ) (bif true then TM2.stepAux (Γ := Γ) q₁ v S else TM2.stepAux (Γ := Γ) q₂ v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (bif true then TM1.stepAux (trNormal (Γ := Γ) q₁) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))
        else TM1.stepAux (trNormal (Γ := Γ) q₂) v (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
        b
branch₂ :
  ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ) (bif false then TM2.stepAux (Γ := Γ) q₁ v S else TM2.stepAux (Γ := Γ) q₂ v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (bif false then TM1.stepAux (trNormal (Γ := Γ) q₁) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))
        else TM1.stepAux (trNormal (Γ := Γ) q₂) v (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
        b
branch₃ :
  ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ) (bif true then TM2.stepAux (Γ := Γ) q₁ v S else TM2.stepAux (Γ := Γ) q₂ v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (bif true then TM1.stepAux (trNormal (Γ := Γ) q₁) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))
        else TM1.stepAux (trNormal (Γ := Γ) q₂) v (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
        b
⊢ ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ) (bif p v then TM2.stepAux (Γ := Γ) q₁ v S else TM2.stepAux (Γ := Γ) q₂ v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (bif p v then TM1.stepAux (trNormal (Γ := Γ) q₁) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))
        else TM1.stepAux (trNormal (Γ := Γ) q₂) v (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
        b

Tactic:
cases p v <;> [exact IH₂ _ hT; exact IH₁ _ hT]