awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
w : List ℕ
hm : ∀ {m : ℕ}, m < 0 → ¬f (m ::ᵥ v) = 0
this :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: (↑v : List ℕ)))
    w
⊢ Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: (↑v : List ℕ)))
    w

Tactic:
exact this
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n_2 + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n_2
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
w : List ℕ
n : ℕ
IH :
  ∀ (hm : ∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0)
    (this :
      Membership.mem (γ := Part (List ℕ))
        (PFun.fix
          (fun (v : List ℕ) ↦
            (cf.eval v).bind fun (y : List ℕ) ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          (n :: (↑v : List ℕ)))
        w),
    Membership.mem (γ := Part (List ℕ))
      (PFun.fix
        (fun (v : List ℕ) ↦
          (cf.eval v).bind fun (y : List ℕ) ↦
            Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
        (0 :: (↑v : List ℕ)))
      w
hm : ∀ {m : ℕ}, m < n + 1 → ¬f (m ::ᵥ v) = 0
this :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      ((n + 1) :: (↑v : List ℕ)))
    w
⊢ Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: (↑v : List ℕ)))
    w

Tactic:
IH (fun {m} h' => hm (Nat.lt_succ_of_lt h'))
          (PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, this⟩))

Premises used: Iff.mpr, And.intro, Exists.intro, Nat.lt_succ_of_lt, PFun.mem_fix_iff, Or.inr
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n_2 + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n_2
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
w : List ℕ
n : ℕ
IH :
  ∀ (hm : ∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0)
    (this :
      Membership.mem (γ := Part (List ℕ))
        (PFun.fix
          (fun (v : List ℕ) ↦
            (cf.eval v).bind fun (y : List ℕ) ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          (n :: (↑v : List ℕ)))
        w),
    Membership.mem (γ := Part (List ℕ))
      (PFun.fix
        (fun (v : List ℕ) ↦
          (cf.eval v).bind fun (y : List ℕ) ↦
            Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
        (0 :: (↑v : List ℕ)))
      w
hm : ∀ {m : ℕ}, m < n + 1 → ¬f (m ::ᵥ v) = 0
this :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      ((n + 1) :: (↑v : List ℕ)))
    w
rfind :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
    ((cf.eval (n :: (↑v : List ℕ))).bind fun (y : List ℕ) ↦
      Part.some
        (if y.headI = 0 then Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)
        else Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)))
    (Sum.inr ((n + 1) :: (↑v : List ℕ)))
⊢ Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: (↑v : List ℕ)))
    w

Tactic:
refine IH (fun {m} h' => hm (Nat.lt_succ_of_lt h'))
          (PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, this⟩))

Premises used: Iff.mpr, And.intro, Exists.intro, Nat.lt_succ_of_lt, PFun.mem_fix_iff, Or.inr
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n_2 + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n_2
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
w : List ℕ
n : ℕ
IH :
  ∀ (hm : ∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0)
    (this :
      Membership.mem (γ := Part (List ℕ))
        (PFun.fix
          (fun (v : List ℕ) ↦
            (cf.eval v).bind fun (y : List ℕ) ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          (n :: (↑v : List ℕ)))
        w),
    Membership.mem (γ := Part (List ℕ))
      (PFun.fix
        (fun (v : List ℕ) ↦
          (cf.eval v).bind fun (y : List ℕ) ↦
            Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
        (0 :: (↑v : List ℕ)))
      w
hm : ∀ {m : ℕ}, m < n + 1 → ¬f (m ::ᵥ v) = 0
this :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      ((n + 1) :: (↑v : List ℕ)))
    w
⊢ Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
    ((cf.eval (n :: (↑v : List ℕ))).bind fun (y : List ℕ) ↦
      Part.some
        (if y.headI = 0 then Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)
        else Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)))
    (Sum.inr ((n + 1) :: (↑v : List ℕ)))

Tactic:
simp only [hf, hm n.lt_succ_self, Part.bind_some, List.headI, if_false,
          Part.mem_some_iff, List.tail_cons]

Premises used: Part.bind_some, Part.mem_some_iff, if_false, Nat.lt_succ_self, List.tail_cons, List.headI
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
v : List ℕ
⊢ (halt.then k').eval v = halt.eval v >>= k'.eval

Tactic:
simp only [Cont.eval, Cont.then, pure_bind]

Premises used: Turing.ToPartrec.Cont.eval, LawfulMonad.pure_bind, Turing.ToPartrec.Cont.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : Code
a_1 : List ℕ
a_2 : Cont
a_ih : ∀ {v : List ℕ}, (a_2.then k').eval v = a_2.eval v >>= k'.eval
v : List ℕ
⊢ ((cons₁ a a_1 a_2).then k').eval v = (cons₁ a a_1 a_2).eval v >>= k'.eval

Tactic:
simp only [Cont.eval, Cont.then, bind_assoc, *]

Premises used: Turing.ToPartrec.Cont.eval, LawfulMonad.bind_assoc, Turing.ToPartrec.Cont.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : List ℕ
a_1 : Cont
a_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval
v : List ℕ
⊢ ((cons₂ a a_1).then k').eval v = (cons₂ a a_1).eval v >>= k'.eval

Tactic:
simp only [Cont.eval, Cont.then, *]

Premises used: Turing.ToPartrec.Cont.eval, Turing.ToPartrec.Cont.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : Code
a_1 : Cont
k_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval
v : List ℕ
⊢ ((comp a a_1).then k').eval v = (comp a a_1).eval v >>= k'.eval

Tactic:
simp only [Cont.eval, Cont.then, bind_assoc, ← k_ih]

Premises used: Turing.ToPartrec.Cont.eval, LawfulMonad.bind_assoc, Turing.ToPartrec.Cont.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : Code
a_1 : Cont
k_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval
v : List ℕ
fix :
  (if v.headI = 0 then a_1.eval v.tail >>= k'.eval else a.fix.eval v.tail >>= (a_1.then k').eval) =
    (if v.headI = 0 then a_1.eval v.tail else a.fix.eval v.tail >>= a_1.eval) >>= k'.eval
⊢ ((Cont.fix a a_1).then k').eval v = (Cont.fix a a_1).eval v >>= k'.eval

Tactic:
simp only [Cont.eval, Cont.then, *]

Premises used: Turing.ToPartrec.Cont.eval, Turing.ToPartrec.Cont.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : Code
a_1 : Cont
k_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval
v : List ℕ
pos : v.headI = 0 → a_1.eval v.tail >>= k'.eval = a_1.eval v.tail >>= k'.eval
neg : ¬v.headI = 0 → a.fix.eval v.tail >>= (a_1.then k').eval = a.fix.eval v.tail >>= a_1.eval >>= k'.eval
⊢ (if v.headI = 0 then a_1.eval v.tail >>= k'.eval else a.fix.eval v.tail >>= (a_1.then k').eval) =
    (if v.headI = 0 then a_1.eval v.tail else a.fix.eval v.tail >>= a_1.eval) >>= k'.eval

Tactic:
split_ifs
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : Code
a_1 : Cont
k_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval
v : List ℕ
h : v.headI = 0
⊢ a_1.eval v.tail >>= k'.eval = a_1.eval v.tail >>= k'.eval

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : Code
a_1 : Cont
k_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval
v : List ℕ
h : ¬v.headI = 0
⊢ a.fix.eval v.tail >>= (a_1.then k').eval = a.fix.eval v.tail >>= a_1.eval >>= k'.eval

Tactic:
simp only [← k_ih, bind_assoc]

Premises used: LawfulMonad.bind_assoc
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : Code
a_1 : Cont
k_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval
v : List ℕ
pos : v.headI = 0 → a_1.eval v.tail >>= k'.eval = a_1.eval v.tail >>= k'.eval
neg : ¬v.headI = 0 → a.fix.eval v.tail >>= (a_1.then k').eval = a.fix.eval v.tail >>= a_1.eval >>= k'.eval
pos₁ : v.headI = 0 → a_1.eval v.tail >>= k'.eval = a_1.eval v.tail >>= k'.eval
neg₁ : ¬v.headI = 0 → a.fix.eval v.tail >>= (a_1.then k').eval = a.fix.eval v.tail >>= a_1.eval >>= k'.eval
⊢ (if v.headI = 0 then a_1.eval v.tail >>= k'.eval else a.fix.eval v.tail >>= (a_1.then k').eval) =
    (if v.headI = 0 then a_1.eval v.tail else a.fix.eval v.tail >>= a_1.eval) >>= k'.eval

Tactic:
split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]

Premises used: LawfulMonad.bind_assoc
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k k' : Cont
v : List ℕ
halt : ∀ {v : List ℕ}, (Cont.halt.then k').eval v = Cont.halt.eval v >>= k'.eval
cons₁ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, (a_2.then k').eval v = a_2.eval v >>= k'.eval) →
      ∀ {v : List ℕ}, ((Cont.cons₁ a a_1 a_2).then k').eval v = (Cont.cons₁ a a_1 a_2).eval v >>= k'.eval
cons₂ :
  ∀ (a : List ℕ) (a_1 : Cont),
    (∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval) →
      ∀ {v : List ℕ}, ((Cont.cons₂ a a_1).then k').eval v = (Cont.cons₂ a a_1).eval v >>= k'.eval
comp :
  ∀ (a : Code) (a_1 : Cont) (k_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval) {v : List ℕ},
    ((Cont.comp a a_1).then k').eval v = (Cont.comp a a_1).eval v >>= k'.eval
fix :
  ∀ (a : Code) (a_1 : Cont) (k_ih : ∀ {v : List ℕ}, (a_1.then k').eval v = a_1.eval v >>= k'.eval) {v : List ℕ},
    ((Cont.fix a a_1).then k').eval v = (Cont.fix a a_1).eval v >>= k'.eval
⊢ (k.then k').eval v = k.eval v >>= k'.eval

Tactic:
induction k generalizing v with
  | halt => simp only [Cont.eval, Cont.then, pure_bind]
  | cons₁ => simp only [Cont.eval, Cont.then, bind_assoc, *]
  | cons₂ => simp only [Cont.eval, Cont.then, *]
  | comp _ _ k_ih => simp only [Cont.eval, Cont.then, bind_assoc, ← k_ih]
  | fix _ _ k_ih =>
    simp only [Cont.eval, Cont.then, *]
    split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]

Premises used: Turing.ToPartrec.Cont.eval, LawfulMonad.bind_assoc, Turing.ToPartrec.Cont.halt, Turing.ToPartrec.Cont.comp, Turing.ToPartrec.Cont.fix, Turing.ToPartrec.Cont.cons₂, LawfulMonad.pure_bind, Turing.ToPartrec.Cont.cons₁, Turing.ToPartrec.Cont.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
c c' : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
cons : stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'
⊢ stepNormal (c.cons c') (k.then k') v = (stepNormal (c.cons c') k v).then k'

Tactic:
simp only [stepNormal, *]

Premises used: Turing.ToPartrec.stepNormal
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
c c' : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
cons : stepNormal c (Cont.cons₁ c' v (k.then k')) v = stepNormal c ((Cont.cons₁ c' v k).then k') v
cons₁ cons₂ :
  stepNormal c (Cont.cons₁ c' v (k.then k')) v = stepNormal c ((fun (k' : Cont) ↦ Cont.cons₁ c' v (k.then k')) k') v
⊢ stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'

Tactic:
rw [← ih, Cont.then]

Premises used: Turing.ToPartrec.Cont.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
c c' : Code
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
ih' : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
comp : stepNormal c' (Cont.comp c (k.then k')) v = (stepNormal c' (Cont.comp c k) v).then k'
⊢ stepNormal (c.comp c') (k.then k') v = (stepNormal (c.comp c') k v).then k'

Tactic:
simp only [stepNormal, *]

Premises used: Turing.ToPartrec.stepNormal
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
c c' : Code
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
ih' : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
comp : stepNormal c' (Cont.comp c (k.then k')) v = stepNormal c' ((Cont.comp c k).then k') v
comp₁ comp₂ :
  stepNormal c' (Cont.comp c (k.then k')) v = stepNormal c' ((fun (k' : Cont) ↦ Cont.comp c (k.then k')) k') v
⊢ stepNormal c' (Cont.comp c (k.then k')) v = (stepNormal c' (Cont.comp c k) v).then k'

Tactic:
rw [← ih', Cont.then]

Premises used: Turing.ToPartrec.Cont.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a a_1 : Code
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal a (k.then k') v = (stepNormal a k v).then k'
a_ih_1 : ∀ (k : Cont) (v : List ℕ), stepNormal a_1 (k.then k') v = (stepNormal a_1 k v).then k'
k : Cont
v : List ℕ
case :
  Nat.rec (motive := fun (x : ℕ) ↦ Cfg) ((stepNormal a k v.tail).then k')
      (fun (y : ℕ) (x : Cfg) ↦ (stepNormal a_1 k (y :: v.tail)).then k') v.headI =
    Cfg.then
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal a k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal a_1 k (y :: v.tail)) v.headI)
      k'
⊢ stepNormal (a.case a_1) (k.then k') v = (stepNormal (a.case a_1) k v).then k'

Tactic:
simp only [stepNormal, *]

Premises used: Turing.ToPartrec.stepNormal
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a a_1 : Code
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal a (k.then k') v = (stepNormal a k v).then k'
a_ih_1 : ∀ (k : Cont) (v : List ℕ), stepNormal a_1 (k.then k') v = (stepNormal a_1 k v).then k'
k : Cont
v : List ℕ
case :
  Nat.rec (motive := fun (x : ℕ) ↦ Cfg) ((stepNormal a k v.tail).then k')
      (fun (y : ℕ) (x : Cfg) ↦ (stepNormal a_1 k (y :: v.tail)).then k') 0 =
    Cfg.then
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal a k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal a_1 k (y :: v.tail)) 0)
      k'
case₁ :
  ∀ (n : ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) ((stepNormal a k v.tail).then k')
        (fun (y : ℕ) (x : Cfg) ↦ (stepNormal a_1 k (y :: v.tail)).then k') (n + 1) =
      Cfg.then
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal a k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal a_1 k (y :: v.tail)) (n + 1))
        k'
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Cfg) ((stepNormal a k v.tail).then k')
      (fun (y : ℕ) (x : Cfg) ↦ (stepNormal a_1 k (y :: v.tail)).then k') v.headI =
    Cfg.then
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal a k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal a_1 k (y :: v.tail)) v.headI)
      k'

Tactic:
cases v.headI

Premises used: List.headI
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a a_1 : Code
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal a (k.then k') v = (stepNormal a k v).then k'
a_ih_1 : ∀ (k : Cont) (v : List ℕ), stepNormal a_1 (k.then k') v = (stepNormal a_1 k v).then k'
k : Cont
v : List ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Cfg) ((stepNormal a k v.tail).then k')
      (fun (y : ℕ) (x : Cfg) ↦ (stepNormal a_1 k (y :: v.tail)).then k') 0 =
    Cfg.then
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal a k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal a_1 k (y :: v.tail)) 0)
      k'

Tactic:
simp only [Nat.rec_zero]

Premises used: Nat.rec_zero
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a a_1 : Code
a_ih : ∀ (k : Cont) (v : List ℕ), stepNormal a (k.then k') v = (stepNormal a k v).then k'
a_ih_1 : ∀ (k : Cont) (v : List ℕ), stepNormal a_1 (k.then k') v = (stepNormal a_1 k v).then k'
k : Cont
v : List ℕ
n : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Cfg) ((stepNormal a k v.tail).then k')
      (fun (y : ℕ) (x : Cfg) ↦ (stepNormal a_1 k (y :: v.tail)).then k') (n + 1) =
    Cfg.then
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal a k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal a_1 k (y :: v.tail)) (n + 1))
      k'

Tactic:
simp only [Nat.rec_zero]

Premises used: Nat.rec_zero
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
c : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
k : Cont
v : List ℕ
fix : stepNormal c (Cont.fix c (k.then k')) v = (stepNormal c (Cont.fix c k) v).then k'
⊢ stepNormal c.fix (k.then k') v = (stepNormal c.fix k v).then k'

Tactic:
simp only [stepNormal, *]

Premises used: Turing.ToPartrec.stepNormal
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
c : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
k : Cont
v : List ℕ
fix : stepNormal c (Cont.fix c (k.then k')) v = stepNormal c ((Cont.fix c k).then k') v
fix₁ fix₂ : stepNormal c (Cont.fix c (k.then k')) v = stepNormal c ((fun (k' : Cont) ↦ Cont.fix c (k.then k')) k') v
⊢ stepNormal c (Cont.fix c (k.then k')) v = (stepNormal c (Cont.fix c k) v).then k'

Tactic:
rw [← ih, Cont.then]

Premises used: Turing.ToPartrec.Cont.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' k : Cont
v : List ℕ
⊢ Cfg.ret (k.then k') (0 :: v) = (Cfg.ret k (0 :: v)).then k'

Tactic:
simp only [Cfg.then]

Premises used: Turing.ToPartrec.Cfg.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' k : Cont
v : List ℕ
⊢ Cfg.ret (k.then k') [v.headI.succ] = (Cfg.ret k [v.headI.succ]).then k'

Tactic:
simp only [Cfg.then]

Premises used: Turing.ToPartrec.Cfg.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' k : Cont
v : List ℕ
⊢ Cfg.ret (k.then k') v.tail = (Cfg.ret k v.tail).then k'

Tactic:
simp only [Cfg.then]

Premises used: Turing.ToPartrec.Cfg.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : Code
a_1 : List ℕ
a_2 : Cont
a_ih : ∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k'
v : List ℕ
cons₁ : stepNormal a (Cont.cons₂ v (a_2.then k')) a_1 = stepNormal a ((Cont.cons₂ v a_2).then k') a_1
⊢ stepNormal a (Cont.cons₂ v (a_2.then k')) a_1 = (stepNormal a (Cont.cons₂ v a_2) a_1).then k'

Tactic:
rw [← stepNormal_then]

Premises used: Turing.ToPartrec.stepNormal_then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : Code
a_1 : List ℕ
a_2 : Cont
a_ih : ∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k'
v : List ℕ
⊢ stepNormal a (Cont.cons₂ v (a_2.then k')) a_1 = stepNormal a ((Cont.cons₂ v a_2).then k') a_1

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : Code
a_1 : Cont
a_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k'
v : List ℕ
comp comp₁ : stepNormal a (a_1.then k') v = stepNormal a (a_1.then k') v
⊢ stepNormal a (a_1.then k') v = (stepNormal a a_1 v).then k'

Tactic:
rw [← stepNormal_then]

Premises used: Turing.ToPartrec.stepNormal_then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : Code
a_1 : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k'
v : List ℕ
fix :
  (if v.headI = 0 then (stepRet a_1 v.tail).then k' else stepNormal a (Cont.fix a (a_1.then k')) v.tail) =
    (if v.headI = 0 then stepRet a_1 v.tail else stepNormal a (Cont.fix a a_1) v.tail).then k'
⊢ stepRet ((Cont.fix a a_1).then k') v = (stepRet (Cont.fix a a_1) v).then k'

Tactic:
simp only [Cont.then, stepRet, *]

Premises used: Turing.ToPartrec.stepRet, Turing.ToPartrec.Cont.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : Code
a_1 : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k'
v : List ℕ
pos : v.headI = 0 → (stepRet a_1 v.tail).then k' = (stepRet a_1 v.tail).then k'
neg : ¬v.headI = 0 → stepNormal a (Cont.fix a (a_1.then k')) v.tail = (stepNormal a (Cont.fix a a_1) v.tail).then k'
⊢ (if v.headI = 0 then (stepRet a_1 v.tail).then k' else stepNormal a (Cont.fix a (a_1.then k')) v.tail) =
    (if v.headI = 0 then stepRet a_1 v.tail else stepNormal a (Cont.fix a a_1) v.tail).then k'

Tactic:
split_ifs
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : Code
a_1 : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k'
v : List ℕ
h : v.headI = 0
pos pos₁ : stepRet (a_1.then k') v.tail = stepRet (a_1.then k') v.tail
⊢ (stepRet a_1 v.tail).then k' = (stepRet a_1 v.tail).then k'

Tactic:
rw [← k_ih]
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : Code
a_1 : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k'
v : List ℕ
h : ¬v.headI = 0
neg : stepNormal a (Cont.fix a (a_1.then k')) v.tail = stepNormal a ((Cont.fix a a_1).then k') v.tail
⊢ stepNormal a (Cont.fix a (a_1.then k')) v.tail = (stepNormal a (Cont.fix a a_1) v.tail).then k'

Tactic:
rw [← stepNormal_then]

Premises used: Turing.ToPartrec.stepNormal_then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : Code
a_1 : Cont
k_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k'
v : List ℕ
h : ¬v.headI = 0
⊢ stepNormal a (Cont.fix a (a_1.then k')) v.tail = stepNormal a ((Cont.fix a a_1).then k') v.tail

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
v : List ℕ
halt : stepRet k' v = (Cfg.halt v).then k'
⊢ stepRet (Cont.halt.then k') v = (stepRet Cont.halt v).then k'

Tactic:
simp only [Cont.then, stepRet, *]

Premises used: Turing.ToPartrec.stepRet, Turing.ToPartrec.Cont.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
v : List ℕ
⊢ stepRet k' v = (Cfg.halt v).then k'

Tactic:
simp only [Cfg.then]

Premises used: Turing.ToPartrec.Cfg.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k' : Cont
a : List ℕ
a_1 : Cont
a_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k'
v : List ℕ
⊢ stepRet ((Cont.cons₂ a a_1).then k') v = (stepRet (Cont.cons₂ a a_1) v).then k'

Tactic:
simp only [Cont.then, stepRet, *]

Premises used: Turing.ToPartrec.stepRet, Turing.ToPartrec.Cont.then