awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
k k' : Cont
v : List ℕ
cons :
  ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
    (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
      ∀ (k : Cont) (v : List ℕ), stepNormal (c.cons c') (k.then k') v = (stepNormal (c.cons c') k v).then k'
⊢ stepNormal c (k.then k') v = (stepNormal c k v).then k'
have cons₁ : ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
  (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
    ∀ (k : Cont) (v : List ℕ),
      stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'
Tactic: induction c generalizing k v with simp only [stepNormal, *]
  | cons c c' ih _ => rw [← ih, Cont.then]
  | comp c c' _ ih' => rw [← ih', Cont.then]
  | case => cases v.headI <;> simp only [Nat.rec_zero]
  | fix c ih => rw [← ih, Cont.then]
  | _ => simp only [Cfg.then]
Cleared hypotheses: c, k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
k k' : Cont
v : List ℕ
cons :
  ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
    (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
      ∀ (k : Cont) (v : List ℕ), stepNormal (c.cons c') (k.then k') v = (stepNormal (c.cons c') k v).then k'
cons₁ :
  ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
    (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
      ∀ (k : Cont) (v : List ℕ),
        stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'
⊢ stepNormal c (k.then k') v = (stepNormal c k v).then k'
have comp : ∀ (c c' : Code),
  (∀ (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 ℕ), stepNormal (c.comp c') (k.then k') v = (stepNormal (c.comp c') k v).then k'
Tactic: induction c generalizing k v with simp only [stepNormal, *]
  | cons c c' ih _ => rw [← ih, Cont.then]
  | comp c c' _ ih' => rw [← ih', Cont.then]
  | case => cases v.headI <;> simp only [Nat.rec_zero]
  | fix c ih => rw [← ih, Cont.then]
  | _ => simp only [Cfg.then]
Cleared hypotheses: c, k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
k k' : Cont
v : List ℕ
cons :
  ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
    (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
      ∀ (k : Cont) (v : List ℕ), stepNormal (c.cons c') (k.then k') v = (stepNormal (c.cons c') k v).then k'
cons₁ :
  ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
    (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
      ∀ (k : Cont) (v : List ℕ),
        stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'
comp :
  ∀ (c c' : Code),
    (∀ (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 ℕ), stepNormal (c.comp c') (k.then k') v = (stepNormal (c.comp c') k v).then k'
⊢ stepNormal c (k.then k') v = (stepNormal c k v).then k'
have comp₁ : ∀ (c c' : Code),
  (∀ (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 ℕ), stepNormal c' (Cont.comp c (k.then k')) v = (stepNormal c' (Cont.comp c k) v).then k'
Tactic: induction c generalizing k v with simp only [stepNormal, *]
  | cons c c' ih _ => rw [← ih, Cont.then]
  | comp c c' _ ih' => rw [← ih', Cont.then]
  | case => cases v.headI <;> simp only [Nat.rec_zero]
  | fix c ih => rw [← ih, Cont.then]
  | _ => simp only [Cfg.then]
Cleared hypotheses: c, k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
k k' : Cont
v : List ℕ
cons :
  ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
    (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
      ∀ (k : Cont) (v : List ℕ), stepNormal (c.cons c') (k.then k') v = (stepNormal (c.cons c') k v).then k'
cons₁ :
  ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
    (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
      ∀ (k : Cont) (v : List ℕ),
        stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'
comp :
  ∀ (c c' : Code),
    (∀ (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 ℕ), stepNormal (c.comp c') (k.then k') v = (stepNormal (c.comp c') k v).then k'
comp₁ :
  ∀ (c c' : Code),
    (∀ (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 ℕ), stepNormal c' (Cont.comp c (k.then k')) v = (stepNormal c' (Cont.comp c k) v).then k'
⊢ stepNormal c (k.then k') v = (stepNormal c k v).then k'
have case : ∀ (a a_1 : Code),
  (∀ (k : Cont) (v : List ℕ), stepNormal a (k.then k') v = (stepNormal a k v).then k') →
    (∀ (k : Cont) (v : List ℕ), stepNormal a_1 (k.then k') v = (stepNormal a_1 k v).then k') →
      ∀ (k : Cont) (v : List ℕ), stepNormal (a.case a_1) (k.then k') v = (stepNormal (a.case a_1) k v).then k'
Tactic: induction c generalizing k v with simp only [stepNormal, *]
  | cons c c' ih _ => rw [← ih, Cont.then]
  | comp c c' _ ih' => rw [← ih', Cont.then]
  | case => cases v.headI <;> simp only [Nat.rec_zero]
  | fix c ih => rw [← ih, Cont.then]
  | _ => simp only [Cfg.then]
Cleared hypotheses: c, k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
k k' : Cont
v : List ℕ
cons :
  ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
    (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
      ∀ (k : Cont) (v : List ℕ), stepNormal (c.cons c') (k.then k') v = (stepNormal (c.cons c') k v).then k'
cons₁ :
  ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
    (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
      ∀ (k : Cont) (v : List ℕ),
        stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'
comp :
  ∀ (c c' : Code),
    (∀ (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 ℕ), stepNormal (c.comp c') (k.then k') v = (stepNormal (c.comp c') k v).then k'
comp₁ :
  ∀ (c c' : Code),
    (∀ (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 ℕ), stepNormal c' (Cont.comp c (k.then k')) v = (stepNormal c' (Cont.comp c k) v).then k'
case :
  ∀ (a a_1 : Code),
    (∀ (k : Cont) (v : List ℕ), stepNormal a (k.then k') v = (stepNormal a k v).then k') →
      (∀ (k : Cont) (v : List ℕ), stepNormal a_1 (k.then k') v = (stepNormal a_1 k v).then k') →
        ∀ (k : Cont) (v : List ℕ), stepNormal (a.case a_1) (k.then k') v = (stepNormal (a.case a_1) k v).then k'
⊢ stepNormal c (k.then k') v = (stepNormal c k v).then k'
have case₁ : ∀ (a a_1 : Code),
  (∀ (k : Cont) (v : List ℕ), stepNormal a (k.then k') v = (stepNormal a k v).then k') →
    (∀ (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') 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: induction c generalizing k v with simp only [stepNormal, *]
  | cons c c' ih _ => rw [← ih, Cont.then]
  | comp c c' _ ih' => rw [← ih', Cont.then]
  | case => cases v.headI <;> simp only [Nat.rec_zero]
  | fix c ih => rw [← ih, Cont.then]
  | _ => simp only [Cfg.then]
Cleared hypotheses: c, k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
k k' : Cont
v : List ℕ
cons :
  ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
    (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
      ∀ (k : Cont) (v : List ℕ), stepNormal (c.cons c') (k.then k') v = (stepNormal (c.cons c') k v).then k'
cons₁ :
  ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
    (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
      ∀ (k : Cont) (v : List ℕ),
        stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'
comp :
  ∀ (c c' : Code),
    (∀ (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 ℕ), stepNormal (c.comp c') (k.then k') v = (stepNormal (c.comp c') k v).then k'
comp₁ :
  ∀ (c c' : Code),
    (∀ (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 ℕ), stepNormal c' (Cont.comp c (k.then k')) v = (stepNormal c' (Cont.comp c k) v).then k'
case :
  ∀ (a a_1 : Code),
    (∀ (k : Cont) (v : List ℕ), stepNormal a (k.then k') v = (stepNormal a k v).then k') →
      (∀ (k : Cont) (v : List ℕ), stepNormal a_1 (k.then k') v = (stepNormal a_1 k v).then k') →
        ∀ (k : Cont) (v : List ℕ), stepNormal (a.case a_1) (k.then k') v = (stepNormal (a.case a_1) k v).then k'
case₁ :
  ∀ (a a_1 : Code),
    (∀ (k : Cont) (v : List ℕ), stepNormal a (k.then k') v = (stepNormal a k v).then k') →
      (∀ (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') 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 c (k.then k') v = (stepNormal c k v).then k'
have fix : ∀ (c : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k') (k : Cont)
  (v : List ℕ), stepNormal c.fix (k.then k') v = (stepNormal c.fix k v).then k'
Tactic: induction c generalizing k v with simp only [stepNormal, *]
  | cons c c' ih _ => rw [← ih, Cont.then]
  | comp c c' _ ih' => rw [← ih', Cont.then]
  | case => cases v.headI <;> simp only [Nat.rec_zero]
  | fix c ih => rw [← ih, Cont.then]
  | _ => simp only [Cfg.then]
Cleared hypotheses: c, k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
k k' : Cont
v : List ℕ
cons :
  ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
    (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
      ∀ (k : Cont) (v : List ℕ), stepNormal (c.cons c') (k.then k') v = (stepNormal (c.cons c') k v).then k'
cons₁ :
  ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
    (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
      ∀ (k : Cont) (v : List ℕ),
        stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'
comp :
  ∀ (c c' : Code),
    (∀ (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 ℕ), stepNormal (c.comp c') (k.then k') v = (stepNormal (c.comp c') k v).then k'
comp₁ :
  ∀ (c c' : Code),
    (∀ (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 ℕ), stepNormal c' (Cont.comp c (k.then k')) v = (stepNormal c' (Cont.comp c k) v).then k'
case :
  ∀ (a a_1 : Code),
    (∀ (k : Cont) (v : List ℕ), stepNormal a (k.then k') v = (stepNormal a k v).then k') →
      (∀ (k : Cont) (v : List ℕ), stepNormal a_1 (k.then k') v = (stepNormal a_1 k v).then k') →
        ∀ (k : Cont) (v : List ℕ), stepNormal (a.case a_1) (k.then k') v = (stepNormal (a.case a_1) k v).then k'
case₁ :
  ∀ (a a_1 : Code),
    (∀ (k : Cont) (v : List ℕ), stepNormal a (k.then k') v = (stepNormal a k v).then k') →
      (∀ (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') 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'
fix :
  ∀ (c : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k') (k : Cont)
    (v : List ℕ), stepNormal c.fix (k.then k') v = (stepNormal c.fix k v).then k'
⊢ stepNormal c (k.then k') v = (stepNormal c k v).then k'
have fix₁ : ∀ (c : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k') (k : Cont)
  (v : List ℕ), stepNormal c (Cont.fix c (k.then k')) v = (stepNormal c (Cont.fix c k) v).then k'
Tactic: induction c generalizing k v with simp only [stepNormal, *]
  | cons c c' ih _ => rw [← ih, Cont.then]
  | comp c c' _ ih' => rw [← ih', Cont.then]
  | case => cases v.headI <;> simp only [Nat.rec_zero]
  | fix c ih => rw [← ih, Cont.then]
  | _ => simp only [Cfg.then]
Cleared hypotheses: c, k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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) a_1).then k'
have cons₁ : stepNormal a (Cont.cons₂ v (a_2.then k')) a_1 = stepNormal a ((Cont.cons₂ v a_2).then k') a_1
Tactic: rw [← stepNormal_then]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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 ℕ
⊢ stepNormal a (a_1.then k') v = (stepNormal a a_1 v).then k'
have comp : stepNormal a (a_1.then k') v = stepNormal a (a_1.then k') v
Tactic: rw [← stepNormal_then]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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 ℕ
⊢ stepRet ((Cont.fix a a_1).then k') v = (stepRet (Cont.fix a a_1) v).then k'
have 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'
Tactic: simp only [Cont.then, stepRet, *]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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 ℕ
⊢ (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'
have pos : v.headI = 0 → (stepRet a_1 v.tail).then k' = (stepRet a_1 v.tail).then k'
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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'
⊢ (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'
have 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'
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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
⊢ (stepRet a_1 v.tail).then k' = (stepRet a_1 v.tail).then k'
have pos : stepRet (a_1.then k') v.tail = stepRet (a_1.then k') v.tail
Tactic: rw [← k_ih]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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) v.tail).then k'
have neg : stepNormal a (Cont.fix a (a_1.then k')) v.tail = stepNormal a ((Cont.fix a a_1).then k') v.tail
Tactic: rw [← stepNormal_then]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k' : Cont
v : List ℕ
⊢ stepRet (Cont.halt.then k') v = (stepRet Cont.halt v).then k'
have halt : stepRet k' v = (Cfg.halt v).then k'
Tactic: simp only [Cont.then, stepRet, *]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k k' : Cont
v : List ℕ
⊢ stepRet (k.then k') v = (stepRet k v).then k'
have cons₁ : ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
  (∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k') →
    ∀ {v : List ℕ}, stepRet ((Cont.cons₁ a a_1 a_2).then k') v = (stepRet (Cont.cons₁ a a_1 a_2) v).then k'
Tactic: induction k generalizing v with simp only [Cont.then, stepRet, *]
  | cons₁ =>
    rw [← stepNormal_then]
    rfl
  | comp =>
    rw [← stepNormal_then]
  | fix _ _ k_ih =>
    split_ifs
    · rw [← k_ih]
    · rw [← stepNormal_then]
      rfl
  | _ => simp only [Cfg.then]
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k k' : Cont
v : List ℕ
cons₁ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.cons₁ a a_1 a_2).then k') v = (stepRet (Cont.cons₁ a a_1 a_2) v).then k'
⊢ stepRet (k.then k') v = (stepRet k v).then k'
have cons₂ : ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
  (∀ {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) a_1).then k'
Tactic: induction k generalizing v with simp only [Cont.then, stepRet, *]
  | cons₁ =>
    rw [← stepNormal_then]
    rfl
  | comp =>
    rw [← stepNormal_then]
  | fix _ _ k_ih =>
    split_ifs
    · rw [← k_ih]
    · rw [← stepNormal_then]
      rfl
  | _ => simp only [Cfg.then]
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k k' : Cont
v : List ℕ
cons₁ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.cons₁ a a_1 a_2).then k') v = (stepRet (Cont.cons₁ a a_1 a_2) v).then k'
cons₂ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {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) a_1).then k'
⊢ stepRet (k.then k') v = (stepRet k v).then k'
have comp : ∀ (a : Code) (a_1 : Cont),
  (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
    ∀ {v : List ℕ}, stepRet ((Cont.comp a a_1).then k') v = (stepRet (Cont.comp a a_1) v).then k'
Tactic: induction k generalizing v with simp only [Cont.then, stepRet, *]
  | cons₁ =>
    rw [← stepNormal_then]
    rfl
  | comp =>
    rw [← stepNormal_then]
  | fix _ _ k_ih =>
    split_ifs
    · rw [← k_ih]
    · rw [← stepNormal_then]
      rfl
  | _ => simp only [Cfg.then]
Cleared hypotheses: k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
k k' : Cont
v : List ℕ
cons₁ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.cons₁ a a_1 a_2).then k') v = (stepRet (Cont.cons₁ a a_1 a_2) v).then k'
cons₂ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {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) a_1).then k'
comp :
  ∀ (a : Code) (a_1 : Cont),
    (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.comp a a_1).then k') v = (stepRet (Cont.comp a a_1) v).then k'
⊢ stepRet (k.then k') v = (stepRet k v).then k'
have comp₁ : ∀ (a : Code) (a_1 : Cont),
  (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
    ∀ {v : List ℕ}, stepNormal a (a_1.then k') v = (stepNormal a a_1 v).then k'
Tactic: induction k generalizing v with simp only [Cont.then, stepRet, *]
  | cons₁ =>
    rw [← stepNormal_then]
    rfl
  | comp =>
    rw [← stepNormal_then]
  | fix _ _ k_ih =>
    split_ifs
    · rw [← k_ih]
    · rw [← stepNormal_then]
      rfl
  | _ => simp only [Cfg.then]
Cleared hypotheses: k, v