awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s : Option Γ'
case :
  ∃ (b₂ : Cfg'),
    TrCfg
        ((fun (k : Cont) (v : List ℕ) ↦
            (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
                (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI :
              Cfg))
          k v)
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal (f.case g) k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
rw [stepNormal]

Premises used: Turing.ToPartrec.stepNormal
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s : Option Γ'
case :
  ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI)
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg
        ((fun (k : Cont) (v : List ℕ) ↦
            (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
                (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI :
              Cfg))
          k v)
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
simp only
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s : Option Γ'
case :
  ∀ (s' : Option Γ')
    (h :
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
          (elim (trList v) [] [] (trContStack k)))
        (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
            (elim (trList v.tail) [] [] (trContStack k)))
          (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
            TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
              (elim (trList (n :: v.tail)) [] [] (trContStack k)))
          v.headI)),
    ∃ (b₂ : Cfg'),
      TrCfg
          (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
            (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI)
          b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI)
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
obtain ⟨s', h⟩ := pred_ok _ _ s v _ _

Premises used: Turing.PartrecToTM2.pred_ok
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s s' : Option Γ'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
      (elim (trList v) [] [] (trContStack k)))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
        (elim (trList v.tail) [] [] (trContStack k)))
      (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
          (elim (trList (n :: v.tail)) [] [] (trContStack k)))
      v.headI)
case :
  ∀
    (h :
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
          (elim (trList v) [] [] (trContStack k)))
        (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
            (elim (trList v.tail) [] [] (trContStack k)))
          (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
            TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
              (elim (trList (n :: v.tail)) [] [] (trContStack k)))
          v.headI)),
    ∃ (b₂ : Cfg'),
      TrCfg
          (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
            (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI)
          b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI)
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
revert h
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s s' : Option Γ'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
      (elim (trList v) [] [] (trContStack k)))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
        (elim (trList v.tail) [] [] (trContStack k)))
      (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
          (elim (trList (n :: v.tail)) [] [] (trContStack k)))
      0)
case :
  ∀ (c : Cfg') (h₁ : TrCfg (stepNormal f k v.tail) c)
    (h₂ :
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
          (elim (trList v.tail) [] [] (trContStack k)))
        c),
    ∃ (b₂ : Cfg'),
      TrCfg
          (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
            (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) 0)
          b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) 0)
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
obtain ⟨c, h₁, h₂⟩ := IHf k _ s'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s s' : Option Γ'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
      (elim (trList v) [] [] (trContStack k)))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
        (elim (trList v.tail) [] [] (trContStack k)))
      (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
          (elim (trList (n :: v.tail)) [] [] (trContStack k)))
      0)
c : Cfg'
h₁ : TrCfg (stepNormal f k v.tail) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s' (elim (trList v.tail) [] [] (trContStack k)))
    c
⊢ ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) 0)
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
⟨_, h₁, h.trans h₂⟩

Premises used: Relation.TransGen.trans, And.intro, Exists.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s s' : Option Γ'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
      (elim (trList v) [] [] (trContStack k)))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
        (elim (trList v.tail) [] [] (trContStack k)))
      (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
          (elim (trList (n :: v.tail)) [] [] (trContStack k)))
      0)
c : Cfg'
h₁ : TrCfg (stepNormal f k v.tail) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s' (elim (trList v.tail) [] [] (trContStack k)))
    c
⊢ ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) 0)
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
exact ⟨_, h₁, h.trans h₂⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s s' : Option Γ'
n : ℕ
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
      (elim (trList v) [] [] (trContStack k)))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
        (elim (trList v.tail) [] [] (trContStack k)))
      (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
          (elim (trList (n :: v.tail)) [] [] (trContStack k)))
      (n + 1))
case :
  ∀ (c : Cfg') (h₁ : TrCfg (stepNormal g k (n :: v.tail)) c)
    (h₂ :
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
          (elim (trList (n :: v.tail)) [] [] (trContStack k)))
        c),
    ∃ (b₂ : Cfg'),
      TrCfg
          (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
            (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) (n + 1))
          b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) (n + 1))
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
obtain ⟨c, h₁, h₂⟩ := IHg k _ s'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s s' : Option Γ'
n : ℕ
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
      (elim (trList v) [] [] (trContStack k)))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
        (elim (trList v.tail) [] [] (trContStack k)))
      (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
          (elim (trList (n :: v.tail)) [] [] (trContStack k)))
      (n + 1))
c : Cfg'
h₁ : TrCfg (stepNormal g k (n :: v.tail)) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
      (elim (trList (n :: v.tail)) [] [] (trContStack k)))
    c
⊢ ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) (n + 1))
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
⟨_, h₁, h.trans h₂⟩

Premises used: Relation.TransGen.trans, And.intro, Exists.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s s' : Option Γ'
n : ℕ
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some ((trNormal f (trCont k)).pred (trNormal g (trCont k)))) s
      (elim (trList v) [] [] (trContStack k)))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s'
        (elim (trList v.tail) [] [] (trContStack k)))
      (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
          (elim (trList (n :: v.tail)) [] [] (trContStack k)))
      (n + 1))
c : Cfg'
h₁ : TrCfg (stepNormal g k (n :: v.tail)) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s'
      (elim (trList (n :: v.tail)) [] [] (trContStack k)))
    c
⊢ ∃ (b₂ : Cfg'),
    TrCfg
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) (n + 1))
        b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
exact ⟨_, h₁, h.trans h₂⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
IH :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal f.fix k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f.fix (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
apply IH
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
v : List ℕ
s : Option Γ'
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepRet Cont.halt v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont Cont.halt))) s
          (elim (trList v) [] [] (trContStack Cont.halt)))
        b₂

Tactic:
⟨_, rfl, TransGen.single rfl⟩

Premises used: Relation.TransGen.single, And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
v : List ℕ
s : Option Γ'
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepRet Cont.halt v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont Cont.halt))) s
          (elim (trList v) [] [] (trContStack Cont.halt)))
        b₂

Tactic:
exact ⟨_, rfl, TransGen.single rfl⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_ih :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) s (elim (trList v) [] [] (trContStack k))) b₂
v : List ℕ
s : Option Γ'
cons₁ :
  ∀ (s' : Cfg') (h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s')
    (h₂ :
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
          (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
        s'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet (Cont.cons₁ fs as k) v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.cons₁ fs as k)))) s
            (elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k))))
          b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepRet (Cont.cons₁ fs as k) v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.cons₁ fs as k)))) s
          (elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k))))
        b₂

Tactic:
obtain ⟨s', h₁, h₂⟩ := trNormal_respects fs (Cont.cons₂ v k) as none

Premises used: Turing.ToPartrec.Cont.cons₂, Option.none, Turing.PartrecToTM2.trNormal_respects