Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case refl.refine_3
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
this : a [S.prog]==>+ Config.haltedOn m regs
⊢ step S.prog a [S.prog]==>* Config.haltedOn m regs

case refl.refine_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ ¬Config.is_halted a = true

case refl.refine_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ Config.is_halted (Config.haltedOn m regs) = true
Tactic:
. rcases Relation.TransGen.head'_iff.mp this with ⟨e,rfl,he⟩
  exact he
Proof state after:
case refl.refine_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ ¬Config.is_halted a = true

case refl.refine_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ Config.is_halted (Config.haltedOn m regs) = true