-- 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 Γ Λ σ
q : TM2.Stmt Γ Λ σ
v : σ
T : ListBlank ((i : K) → Option (Γ i))
k : K
S : (k : K) → List (Γ k)
hT : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) T = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
IH :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} {T : ListBlank ((k : K) → Option (Γ k))},
    (∀ (k : K),
        ListBlank.map (proj (Γ := fun (i : K) ↦ Option (Γ i)) k) T = 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 (Γ := Γ) T))) b
hgo :
  Reaches₀ (TM1.step (tr (Γ := Γ) M))
    { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) T) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
    { l := some (go (Γ := Γ) k o q), var := v,
      Tape := (Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) T)) }
T' : ListBlank ((k : K) → Option (Γ k))
hT' :
  ∀ (k_1 : K),
    ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) T' =
      ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (stWrite (Γ := Γ) v (S k) o) k_1)).reverse
hrun :
  Eq (α := TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ)
    (TM1.stepAux (trStAct (Γ := Γ) (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ ret (Γ := Γ) q) o) v
      ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) T))))
    (TM1.stepAux (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ ret (Γ := Γ) q) (stVar (Γ := Γ) v (S k) o)
      ((Tape.move Dir.right)^[(update (β := fun (a : K) ↦ List (Γ a)) S k (stWrite (Γ := Γ) v (S k) o) k).length]
        (Tape.mk' ∅ (addBottom (Γ := Γ) T'))))
this :
  Reaches₁ (TM1.step (tr (Γ := Γ) M))
    { l := some (go (Γ := Γ) k o q), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) T) :
      TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ }
    { l := some (ret (Γ := Γ) q), var := stVar (Γ := Γ) v (S k) o,
      Tape :=
        (Tape.move Dir.right)^[(update (β := fun (a : K) ↦ List (Γ a)) S k (stWrite (Γ := Γ) v (S k) o) k).length]
          (Tape.mk' ∅ (addBottom (Γ := Γ) T')) }
c : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ
gc :
  TrCfg (Γ := Γ)
    (TM2.stepAux (Γ := Γ) q (stVar (Γ := Γ) v (S k) o)
      (update (β := fun (a : K) ↦ List (Γ a)) S k (stWrite (Γ := Γ) v (S k) o)))
    c
rc :
  Reaches (TM1.step (tr (Γ := Γ) M))
    (TM1.stepAux (trNormal (Γ := Γ) q) (stVar (Γ := Γ) v (S k) o) (Tape.mk' ∅ (addBottom (Γ := Γ) T'))) c
⊢ ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ)
        (TM2.stepAux (Γ := Γ) q (stVar (Γ := Γ) v (S k) o)
          (update (β := fun (k : K) ↦ List (Γ k)) S k (stWrite (Γ := Γ) v (S k) o)))
        b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (TM1.stepAux (goto fun (x : Γ' K Γ) (x_1 : σ) ↦ go (Γ := Γ) k o q) v (Tape.mk' ∅ (addBottom (Γ := Γ) T))) b

Tactic:
⟨c, gc, (this.to₀.trans (tr_respects_aux₃ M _) c (TransGen.head' rfl ?_)).to_reflTransGen⟩

Premises used: StateTransition.Reaches₁.to₀, Turing.TM2to1.tr_respects_aux₃, Relation.TransGen.head', StateTransition.Reaches₀.trans, And.intro, Exists.intro, Relation.TransGen.to_reflTransGen, rfl