awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
n : ℕ
c d : List Γ'
s : Option Γ'
l₁ : List Γ'
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum PosNum.one.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum PosNum.one ++ [Γ'.cons]) l₁ c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))

Tactic:
⟨Γ'.bit0 :: l₁, [Γ'.bit1], some Γ'.cons, rfl, TransGen.head rfl (TransGen.single ?_)⟩

Premises used: Relation.TransGen.head, Turing.PartrecToTM2.Γ'.cons, Option.some, Turing.PartrecToTM2.Γ'.bit1, List.cons, Turing.PartrecToTM2.Γ'.bit0, Relation.TransGen.single, And.intro, Exists.intro, rfl, List.nil
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
n : ℕ
c d : List Γ'
s : Option Γ'
l₁ : List Γ'
pos :
  TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (some Γ'.cons)
      (elim ([Γ'.bit1] ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d) ∈
    TM2.step (Γ := fun (x : K') ↦ Γ') tr
      (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr q.succ) s (elim (trPosNum PosNum.one ++ [Γ'.cons]) l₁ c d))
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum PosNum.one.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum PosNum.one ++ [Γ'.cons]) l₁ c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))

Tactic:
refine ⟨Γ'.bit0 :: l₁, [Γ'.bit1], some Γ'.cons, rfl, TransGen.head rfl (TransGen.single ?_)⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
n : ℕ
c d : List Γ'
s : Option Γ'
l₁ : List Γ'
⊢ TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (some Γ'.cons)
      (elim ([Γ'.bit1] ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d) ∈
    TM2.step (Γ := fun (x : K') ↦ Γ') tr
      (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr q.succ) s (elim (trPosNum PosNum.one ++ [Γ'.cons]) l₁ c d))

Tactic:
simp [trPosNum]

Premises used: Turing.PartrecToTM2.trPosNum
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
IH :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
s : Option Γ'
l₁ : List Γ'
pos :
  ∀ (l₁' l₂' : List Γ') (s' : Option Γ') (e : (Γ'.bit0 :: l₁).reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂')
    (h :
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) (some Γ'.bit1)
          (elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m.bit1.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit1.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))

Tactic:
obtain ⟨l₁', l₂', s', e, h⟩ := IH (Γ'.bit0 :: l₁)

Premises used: List.cons, Turing.PartrecToTM2.Γ'.bit0
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
IH :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit0 :: l₁).reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) (some Γ'.bit1)
      (elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit1.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))

Tactic:
⟨l₁', l₂', s', e, TransGen.head ?_ h⟩

Premises used: Relation.TransGen.head, And.intro, Exists.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
IH :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit0 :: l₁).reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) (some Γ'.bit1)
      (elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
pos :
  TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) (some Γ'.bit1)
      (elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d) ∈
    TM2.step (Γ := fun (x : K') ↦ Γ') tr
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d))
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit1.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))

Tactic:
refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
IH :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit0 :: l₁).reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) (some Γ'.bit1)
      (elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
pos : some Γ'.bit1 = some Γ'.bit1
⊢ TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) (some Γ'.bit1)
      (elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d) ∈
    TM2.step (Γ := fun (x : K') ↦ Γ') tr
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d))

Tactic:
simp [trPosNum]

Premises used: Turing.PartrecToTM2.trPosNum
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
IH :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit0 :: l₁).reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) (some Γ'.bit1)
      (elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
⊢ some Γ'.bit1 = some Γ'.bit1

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
a_ih :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
s : Option Γ'
l₁ : List Γ'
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit0.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m.bit0 ++ [Γ'.cons]) l₁ c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))

Tactic:
⟨l₁, _, some Γ'.bit0, rfl, TransGen.single ?_⟩

Premises used: Option.some, Turing.PartrecToTM2.Γ'.bit0, Relation.TransGen.single, And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
a_ih :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
s : Option Γ'
l₁ : List Γ'
pos :
  TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (some Γ'.bit0)
      (elim (trPosNum m.bit0.succ ++ [Γ'.cons]) l₁ c d) ∈
    TM2.step (Γ := fun (x : K') ↦ Γ') tr
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m.bit0 ++ [Γ'.cons]) l₁ c d))
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit0.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m.bit0 ++ [Γ'.cons]) l₁ c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))

Tactic:
refine ⟨l₁, _, some Γ'.bit0, rfl, TransGen.single ?_⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
a_ih :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
s : Option Γ'
l₁ : List Γ'
pos :
  (bif decide ((trPosNum m.bit0 ++ [Γ'.cons]).head? = some Γ'.bit1) then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) (trPosNum m.bit0 ++ [Γ'.cons]).head?
        (elim (trPosNum m.bit0 ++ [Γ'.cons]).tail (Γ'.bit0 :: l₁) c d)
    else
      bif decide ((trPosNum m.bit0 ++ [Γ'.cons]).head? = some Γ'.cons) then
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (trPosNum m.bit0 ++ [Γ'.cons]).head?
          (elim (Γ'.bit1 :: Γ'.cons :: (trPosNum m.bit0 ++ [Γ'.cons]).tail) l₁ c d)
      else
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (trPosNum m.bit0 ++ [Γ'.cons]).head?
          (elim (Γ'.bit1 :: (trPosNum m.bit0 ++ [Γ'.cons]).tail) l₁ c d)) =
    TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (some Γ'.bit0)
      (elim (trPosNum m.bit0.succ ++ [Γ'.cons]) l₁ c d)
⊢ TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (some Γ'.bit0)
      (elim (trPosNum m.bit0.succ ++ [Γ'.cons]) l₁ c d) ∈
    some
      (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
        (pop' main
          (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ decide (s = some Γ'.bit1))
            (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit0)
              (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q.succ))
            (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ decide (s = some Γ'.cons))
              (push (Γ := fun (x : K') ↦ Γ') main (fun (x : Option Γ') ↦ Γ'.cons)
                (push (Γ := fun (x : K') ↦ Γ') main (fun (x : Option Γ') ↦ Γ'.bit1)
                  (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q)))
              (push (Γ := fun (x : K') ↦ Γ') main (fun (x : Option Γ') ↦ Γ'.bit1)
                (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q)))))
        s (elim (trPosNum m.bit0 ++ [Γ'.cons]) l₁ c d))

Tactic:
simp only [TM2.stepAux, pop', elim_main, elim_update_main,
      elim_rev, elim_update_rev, Function.update_self, Option.mem_def, Option.some.injEq]

Premises used: Turing.TM2.stepAux, Option.some.injEq, Turing.PartrecToTM2.K'.elim_update_main, Turing.PartrecToTM2.K'.elim_rev, Turing.PartrecToTM2.K'.elim_main, Turing.PartrecToTM2.pop', Function.update_self, Turing.PartrecToTM2.K'.elim_update_rev, Option.mem_def
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
a_ih :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
s : Option Γ'
l₁ : List Γ'
⊢ (bif decide ((trPosNum m.bit0 ++ [Γ'.cons]).head? = some Γ'.bit1) then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) (trPosNum m.bit0 ++ [Γ'.cons]).head?
        (elim (trPosNum m.bit0 ++ [Γ'.cons]).tail (Γ'.bit0 :: l₁) c d)
    else
      bif decide ((trPosNum m.bit0 ++ [Γ'.cons]).head? = some Γ'.cons) then
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (trPosNum m.bit0 ++ [Γ'.cons]).head?
          (elim (Γ'.bit1 :: Γ'.cons :: (trPosNum m.bit0 ++ [Γ'.cons]).tail) l₁ c d)
      else
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (trPosNum m.bit0 ++ [Γ'.cons]).head?
          (elim (Γ'.bit1 :: (trPosNum m.bit0 ++ [Γ'.cons]).tail) l₁ c d)) =
    TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (some Γ'.bit0)
      (elim (trPosNum m.bit0.succ ++ [Γ'.cons]) l₁ c d)

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
v : List ℕ
c d : List Γ'
nil :
  ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList []) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList (List.tail [])) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: List.tail [])) [] c d))
        (List.headI []))
cons :
  ∀ (v : List ℕ),
    ∃ (s' : Option Γ'),
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList (0 :: v)) [] c d))
        (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList (0 :: v).tail) [] c d))
          (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
            TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: (0 :: v).tail)) [] c d))
          (0 :: v).headI)
cons₁ :
  ∀ (v : List ℕ) (n : ℕ),
    ∃ (s' : Option Γ'),
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList ((n + 1) :: v)) [] c d))
        (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList ((n + 1) :: v).tail) [] c d))
          (fun (n_1 : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
            TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n_1 :: ((n + 1) :: v).tail)) [] c d))
          ((n + 1) :: v).headI)
⊢ ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList v) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList v.tail) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: v.tail)) [] c d))
        v.headI)

Tactic:
rcases v with (_ | ⟨_ | n, v⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
⊢ ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList []) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList (List.tail [])) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: List.tail [])) [] c d))
        (List.headI []))

Tactic:
⟨none, TransGen.single ?_⟩

Premises used: Option.none, Relation.TransGen.single, Exists.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
nil :
  Membership.mem (α := TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
    (TM2.step (Γ := fun (x : K') ↦ Γ') tr
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList []) [] c d)))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) none (elim (trList (List.tail [])) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trList (n :: List.tail [])) [] c d))
        (List.headI []) :
      TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
⊢ ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList []) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList (List.tail [])) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: List.tail [])) [] c d))
        (List.headI []))

Tactic:
refine ⟨none, TransGen.single ?_⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
⊢ Membership.mem (α := TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
    (TM2.step (Γ := fun (x : K') ↦ Γ') tr
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList []) [] c d)))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) none (elim (trList (List.tail [])) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trList (n :: List.tail [])) [] c d))
        (List.headI []) :
      TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
⊢ ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList (0 :: v)) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList (0 :: v).tail) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: (0 :: v).tail)) [] c d))
        (0 :: v).headI)

Tactic:
⟨some Γ'.cons, TransGen.single ?_⟩

Premises used: Turing.PartrecToTM2.Γ'.cons, Option.some, Relation.TransGen.single, Exists.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
cons :
  Membership.mem (α := TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
    (TM2.step (Γ := fun (x : K') ↦ Γ') tr
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList (0 :: v)) [] c d)))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (some Γ'.cons) (elim (trList (0 :: v).tail) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) (some Γ'.cons) (elim (trList (n :: (0 :: v).tail)) [] c d))
        (0 :: v).headI :
      TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
⊢ ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList (0 :: v)) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList (0 :: v).tail) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: (0 :: v).tail)) [] c d))
        (0 :: v).headI)

Tactic:
refine ⟨some Γ'.cons, TransGen.single ?_⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
⊢ Membership.mem (α := TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
    (TM2.step (Γ := fun (x : K') ↦ Γ') tr
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList (0 :: v)) [] c d)))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (some Γ'.cons) (elim (trList (0 :: v).tail) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) (some Γ'.cons) (elim (trList (n :: (0 :: v).tail)) [] c d))
        (0 :: v).headI :
      TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))

Tactic:
simp