awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
h₃ : x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail)
⊢ ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
rw [stepRet] at h

Premises used: Turing.ToPartrec.stepRet
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
h₃ : x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail)
IH₁ :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
⊢ Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')

Tactic:
rw [stepRet] at h

Premises used: Turing.ToPartrec.stepRet
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
h₃ : x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail)
IH₁ :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr₁ : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
⊢ v' ∈ f.eval v

Tactic:
rw [stepRet] at h

Premises used: Turing.ToPartrec.stepRet
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
h₃ : x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail)
IH₁ :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr₁ : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₄ : v' ∈ f.eval v
⊢ Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')

Tactic:
rw [stepRet] at h

Premises used: Turing.ToPartrec.stepRet
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
h₃ : x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail)
IH₁ :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr₁ : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₄ : v' ∈ f.eval v
h₅ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
⊢ Cfg.halt v' ∈ eval step (stepRet Cont.halt v')

Tactic:
rw [stepRet] at h

Premises used: Turing.ToPartrec.stepRet
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail)
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
mp :
  ∀ (h : x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail)),
    ∃ v₂ ∈ if v'.headI = 0 then pure v'.tail else f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)
⊢ ∃ v₂ ∈ if v'.headI = 0 then pure v'.tail else f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
revert h
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
pos :
  ∀ (he : v'.headI = 0)
    (h : x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail)),
    ∃ v₂ ∈ if v'.headI = 0 then pure v'.tail else f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)
neg :
  ∀ (he : ¬v'.headI = 0)
    (h : x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail)),
    ∃ v₂ ∈ if v'.headI = 0 then pure v'.tail else f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)
⊢ ∀ (h : x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail)),
    ∃ v₂ ∈ if v'.headI = 0 then pure v'.tail else f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
by_cases he : v'.headI = 0

Premises used: List.headI
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : v'.headI = 0
pos :
  ∀ (h : x ∈ eval step (stepRet k v'.tail)),
    ∃ (v₂ : List ℕ), Membership.mem (γ := Part (List ℕ)) (pure v'.tail) v₂ ∧ x ∈ eval step (Cfg.ret k v₂)
⊢ ∀ (h : x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail)),
    ∃ v₂ ∈ if v'.headI = 0 then pure v'.tail else f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
simp only [if_pos, if_false, he]

Premises used: if_false, if_pos
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
neg :
  ∀ (h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)), ∃ v₂ ∈ f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)
⊢ ∀ (h : x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail)),
    ∃ v₂ ∈ if v'.headI = 0 then pure v'.tail else f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
simp only [if_pos, if_false, he]

Premises used: if_false, if_pos
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : v'.headI = 0
h : x ∈ eval step (stepRet k v'.tail)
⊢ ∃ (v₂ : List ℕ), Membership.mem (γ := Part (List ℕ)) (pure v'.tail) v₂ ∧ x ∈ eval step (Cfg.ret k v₂)

Tactic:
⟨_, Part.mem_some _, ?_⟩

Premises used: Part.mem_some, And.intro, Exists.intro
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : v'.headI = 0
h : x ∈ eval step (stepRet k v'.tail)
pos : x ∈ eval step (Cfg.ret k v'.tail)
⊢ ∃ (v₂ : List ℕ), Membership.mem (γ := Part (List ℕ)) (pure v'.tail) v₂ ∧ x ∈ eval step (Cfg.ret k v₂)

Tactic:
refine ⟨_, Part.mem_some _, ?_⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : v'.headI = 0
h pos : x ∈ eval step (stepRet k v'.tail)
pos₁ : Reaches step (Cfg.ret k v'.tail) (stepRet k v'.tail)
rw : Cfg
⊢ x ∈ eval step (Cfg.ret k v'.tail)

Tactic:
rw [reaches_eval]

Premises used: StateTransition.reaches_eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : v'.headI = 0
h : x ∈ eval step (stepRet k v'.tail)
⊢ x ∈ eval step (stepRet k v'.tail)

Tactic:
h
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : v'.headI = 0
h : x ∈ eval step (stepRet k v'.tail)
⊢ x ∈ eval step (stepRet k v'.tail)

Tactic:
exact h
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : v'.headI = 0
h : x ∈ eval step (stepRet k v'.tail)
⊢ Reaches step (Cfg.ret k v'.tail) (stepRet k v'.tail)

Tactic:
ReflTransGen.single rfl

Premises used: Relation.ReflTransGen.single, rfl, StateTransition.Reaches
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : v'.headI = 0
h : x ∈ eval step (stepRet k v'.tail)
⊢ Reaches step (Cfg.ret k v'.tail) (stepRet k v'.tail)

Tactic:
exact ReflTransGen.single rfl

Premises used: Relation.ReflTransGen.single, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
neg :
  ∀ (k₀ : Cont) (v₀ : List ℕ) (e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀),
    ∃ v₂ ∈ f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)
⊢ ∃ v₂ ∈ f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
obtain ⟨k₀, v₀, e₀⟩ := stepNormal.is_ret f Cont.halt v'.tail

Premises used: Turing.ToPartrec.Cont.halt, List.tail, Turing.ToPartrec.stepNormal.is_ret
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
⊢ stepNormal f (Cont.halt.then (Cont.fix f k)) v'.tail = (stepNormal f Cont.halt v'.tail).then (Cont.fix f k)

Tactic:
have e₁ := stepNormal_then f Cont.halt (Cont.fix f k) v'.tail
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.halt.then (Cont.fix f k)) v'.tail = (stepNormal f Cont.halt v'.tail).then (Cont.fix f k)
⊢ stepNormal f ((fun (k' : Cont) ↦ k') (Cont.fix f k)) v'.tail =
    (fun (k' : Cont) ↦ Cfg.ret (k₀.then k') v₀) (Cont.fix f k)

Tactic:
rw [e₀, Cont.then, Cfg.then] at e₁

Premises used: Turing.ToPartrec.Cfg.then, Turing.ToPartrec.Cont.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
rw : step (Cfg.ret (k₀.then (Cont.fix f k)) v₀) = some (stepRet (k₀.then (Cont.fix f k)) v₀)
⊢ step (stepRet (Cont.fix f k) v') = some (stepRet (k₀.then (Cont.fix f k)) v₀)

Tactic:
rw [stepRet, if_neg he, e₁]

Premises used: if_neg, Turing.ToPartrec.stepRet
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
⊢ step (Cfg.ret (k₀.then (Cont.fix f k)) v₀) = some (stepRet (k₀.then (Cont.fix f k)) v₀)

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
hab : stepRet k₀ v₀ ∈ step (stepNormal f Cont.halt v'.tail)
⊢ Reaches step (stepNormal f Cont.halt v'.tail) (stepRet k₀ v₀)

Tactic:
apply ReflTransGen.single

Premises used: Relation.ReflTransGen.single