awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Λ
b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ
c : TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) (M l) v S) b
r :
  Reaches (TM1.step (tr (Γ := Γ) M))
    (TM1.stepAux (tr (Γ := Γ) M (normal (Γ := Γ) l)) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b
⊢ match (motive := Option (TM2.Cfg Γ Λ σ) → Prop) TM2.step (Γ := Γ) M (TM2.Cfg.mk (Γ := Γ) (some l) v S) with
  | some b₁ =>
    ∃ (b₂ : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
      TrCfg (Γ := Γ) b₁ b₂ ∧
        Reaches₁ (TM1.step (tr (Γ := Γ) M))
          { l := Option.map (normal (Γ := Γ)) (some l), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) } b₂
  | none =>
    TM1.step (tr (Γ := Γ) M)
        { l := Option.map (normal (Γ := Γ)) (some l), var := v, Tape := Tape.mk' ∅ (addBottom (Γ := Γ) L) :
          TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ } =
      none

Tactic:
exact ⟨b, c, TransGen.head' rfl r⟩
-- 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 : Λ
generalize :
  ∀ (N : TM2.Stmt Γ Λ σ),
    ∃ (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
⊢ ∃ (b : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ),
    TrCfg (Γ := Γ) (TM2.stepAux (Γ := Γ) (M l) v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M)) (TM1.stepAux (trNormal (Γ := Γ) (M l)) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b

Tactic:
generalize M l = N
-- 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 : Λ
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

Tactic:
tr_respects_aux M hT s @IH

Premises used: Turing.TM2to1.tr_respects_aux
-- 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 : Λ
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

Tactic:
exact tr_respects_aux M hT s @IH

Premises used: Turing.TM2to1.tr_respects_aux
-- 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 : Λ
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

Tactic:
IH _ hT

Premises used: Turing.TM2.stepAux, Turing.TM2to1.trNormal, Turing.TM1.stepAux
-- 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 : Λ
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

Tactic:
exact IH _ hT
-- 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 p v then TM2.stepAux (Γ := Γ) q₁ v S else TM2.stepAux (Γ := Γ) q₂ v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (bif (fun (x : Γ' K Γ) ↦ p) (Tape.mk' ∅ (addBottom (Γ := Γ) L)).head v 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 (Γ := Γ) (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

Tactic:
unfold TM2.stepAux trNormal TM1.stepAux

Premises used: Turing.TM2.stepAux, Turing.TM2to1.trNormal, Turing.TM1.stepAux
-- 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 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
⊢ ∃ (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 (fun (x : Γ' K Γ) ↦ p) (Tape.mk' ∅ (addBottom (Γ := Γ) L)).head v then
          TM1.stepAux (trNormal (Γ := Γ) q₁) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))
        else TM1.stepAux (trNormal (Γ := Γ) q₂) v (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
        b

Tactic:
beta_reduce
-- 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
⊢ ∃ (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
-- 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
⊢ ∃ (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

Tactic:
IH₂ _ hT

Premises used: cond
-- 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
⊢ ∃ (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

Tactic:
exact IH₂ _ hT
-- 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
⊢ ∃ (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

Tactic:
IH₁ _ hT

Premises used: cond
-- 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
⊢ ∃ (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

Tactic:
exact IH₁ _ hT
-- 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 : Λ
l_1 : σ → Λ
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_1) v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (TM1.stepAux (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l_1)) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b

Tactic:
⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩

Premises used: Relation.ReflTransGen.refl, And.intro, Exists.intro, Turing.TM2to1.TrCfg.mk
-- 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 : Λ
l_1 : σ → Λ
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_1) v S) b ∧
      Reaches (TM1.step (tr (Γ := Γ) M))
        (TM1.stepAux (trNormal (Γ := Γ) (TM2.Stmt.goto (Γ := Γ) l_1)) v (Tape.mk' ∅ (addBottom (Γ := Γ) L))) b

Tactic:
exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
-- 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 : Λ
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

Tactic:
⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩

Premises used: Relation.ReflTransGen.refl, And.intro, Exists.intro, Turing.TM2to1.TrCfg.mk
-- 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 : Λ
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

Tactic:
exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
inst_1 : Inhabited Λ
inst_2 : Inhabited σ
k : K
L : List (Γ k)
rw :
  TrCfg.{u_1, u_2, u_3, u_4} (Γ := Γ) (Λ := Λ) (σ := σ) (TM2.init (Γ := Γ) k L)
    { l := Option.map (normal (Γ := Γ)) (some default), var := default,
      Tape :=
        Tape.mk' ∅
          (addBottom (Γ := Γ)
            (ListBlank.mk
              (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) L.reverse))) }
rw₁ :
  Eq (α := TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ) (TM1.init (trInit (Γ := Γ) k L))
    { l := Option.map (normal (Γ := Γ)) (some default), var := default,
      Tape :=
        Tape.mk' ∅
          (addBottom (Γ := Γ)
            (ListBlank.mk
              (List.map (fun (a : Γ k) ↦ update (β := fun (k : K) ↦ Option (Γ k)) default k (some a)) L.reverse))) }
⊢ TrCfg.{u_1, u_2, u_3, u_4} (Γ := Γ) (Λ := Λ) (σ := σ) (TM2.init (Γ := Γ) k L) (TM1.init (trInit (Γ := Γ) k L))

Tactic:
rw [(_ : TM1.init _ = _)]