Theorem: RegMachine.Prog.Start.evals_functional (RegMachine/Basic.lean)

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
i o1 o2 : ℕ
h1 : evals S i o1
h2 : evals S i o2
⊢ o1 = o2
Tactic:
match h1, h2 with
| ⟨regs1,h1'⟩, ⟨regs2,h2'⟩ =>
clear h1 h2
generalize Config.init _ _ = c1 at h1' h2'
clear i
induction h1' using Relation.ReflTransGen.head_induction_on
  <;> clear c1
case refl =>
  have : o1 = (Config.haltedOn (L := L) o1 regs1).regs .io :=
    by simp [Config.haltedOn]
  rw [this]
  have := halt_is_fixpoint _ h2' (by simp)
  rw [this]
  simp
case head c d h _ ih =>
  apply ih; clear ih
  cases Relation.ReflTransGen.cases_head h2' <;> clear h2'
  case inl h2' =>
    cases h2'
    have : _ = d := by
      apply halt_is_fixpoint _ (Relation.ReflTransGen.single h)
      simp
    rw [←this]
  case inr h2' =>
    rcases h2' with ⟨c',hc,h⟩
    have : c' = d := stepsTo_functional _ hc ‹_›
    rw [←this]
    exact h
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
i o1 o2 : ℕ
h1 : evals S i o1
h2 : evals S i o2
regs1 : R → ℕ
h1' : Config.init i (some S.start) [S.prog]==>* Config.haltedOn o1 regs1
regs2 : R → ℕ
h2' : Config.init i (some S.start) [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Tactic:
clear h1 h2
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
i o1 o2 : ℕ
regs1 : R → ℕ
h1' : Config.init i (some S.start) [S.prog]==>* Config.haltedOn o1 regs1
regs2 : R → ℕ
h2' : Config.init i (some S.start) [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
i o1 o2 : ℕ
regs1 : R → ℕ
h1' : Config.init i (some S.start) [S.prog]==>* Config.haltedOn o1 regs1
regs2 : R → ℕ
h2' : Config.init i (some S.start) [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Tactic:
generalize Config.init _ _ = c1 at h1' h2'
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
i o1 o2 : ℕ
regs1 regs2 : R → ℕ
c1 : Config (WithIO R) L
h1' : c1 [S.prog]==>* Config.haltedOn o1 regs1
h2' : c1 [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
i o1 o2 : ℕ
regs1 regs2 : R → ℕ
c1 : Config (WithIO R) L
h1' : c1 [S.prog]==>* Config.haltedOn o1 regs1
h2' : c1 [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Tactic:
clear i
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c1 : Config (WithIO R) L
h1' : c1 [S.prog]==>* Config.haltedOn o1 regs1
h2' : c1 [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c1 : Config (WithIO R) L
h1' : c1 [S.prog]==>* Config.haltedOn o1 regs1
h2' : c1 [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Tactic:
induction h1' using Relation.ReflTransGen.head_induction_on
  <;> clear c1
State after:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2

case head
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
a✝¹ c✝ : Config (WithIO R) L
h'✝ : a✝¹ [S.prog]==> c✝
h✝ : Relation.ReflTransGen (stepsTo S.prog) c✝ (Config.haltedOn o1 regs1)
a✝ : c✝ [S.prog]==>* Config.haltedOn o2 regs2 → o1 = o2
h2' : a✝¹ [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Tactic:
case refl =>
  have : o1 = (Config.haltedOn (L := L) o1 regs1).regs .io :=
    by simp [Config.haltedOn]
  rw [this]
  have := halt_is_fixpoint _ h2' (by simp)
  rw [this]
  simp
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
ih : d [S.prog]==>* Config.haltedOn o2 regs2 → o1 = o2
h2' : c [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Tactic:
case head c d h _ ih =>
  apply ih; clear ih
  cases Relation.ReflTransGen.cases_head h2' <;> clear h2'
  case inl h2' =>
    cases h2'
    have : _ = d := by
      apply halt_is_fixpoint _ (Relation.ReflTransGen.single h)
      simp
    rw [←this]
  case inr h2' =>
    rcases h2' with ⟨c',hc,h⟩
    have : c' = d := stepsTo_functional _ hc ‹_›
    rw [←this]
    exact h
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Tactic:
have : o1 = (Config.haltedOn (L := L) o1 regs1).regs .io :=
  by simp [Config.haltedOn]
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
⊢ o1 = o2

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
⊢ o1 = o2
Tactic:
rw [this]
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
⊢ Config.regs (Config.haltedOn o1 regs1) WithIO.io = o2

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
⊢ Config.regs (Config.haltedOn o1 regs1) WithIO.io = o2
Tactic:
have := halt_is_fixpoint _ h2' (by simp)
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this✝ : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
this : Config.haltedOn o1 regs1 = Config.haltedOn o2 regs2
⊢ Config.regs (Config.haltedOn o1 regs1) WithIO.io = o2

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this✝ : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
this : Config.haltedOn o1 regs1 = Config.haltedOn o2 regs2
⊢ Config.regs (Config.haltedOn o1 regs1) WithIO.io = o2
Tactic:
rw [this]
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this✝ : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
this : Config.haltedOn o1 regs1 = Config.haltedOn o2 regs2
⊢ Config.regs (Config.haltedOn o2 regs2) WithIO.io = o2

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this✝ : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
this : Config.haltedOn o1 regs1 = Config.haltedOn o2 regs2
⊢ Config.regs (Config.haltedOn o2 regs2) WithIO.io = o2
Tactic:
simp
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
Tactic:
simp [Config.haltedOn]
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
⊢ Config.is_halted (Config.haltedOn o1 regs1) = true
Tactic:
simp
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
ih : d [S.prog]==>* Config.haltedOn o2 regs2 → o1 = o2
h2' : c [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Tactic:
apply ih
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
ih : d [S.prog]==>* Config.haltedOn o2 regs2 → o1 = o2
h2' : c [S.prog]==>* Config.haltedOn o2 regs2
⊢ d [S.prog]==>* Config.haltedOn o2 regs2

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
ih : d [S.prog]==>* Config.haltedOn o2 regs2 → o1 = o2
h2' : c [S.prog]==>* Config.haltedOn o2 regs2
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
clear ih
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h2' : c [S.prog]==>* Config.haltedOn o2 regs2
⊢ d [S.prog]==>* Config.haltedOn o2 regs2

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h2' : c [S.prog]==>* Config.haltedOn o2 regs2
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
cases Relation.ReflTransGen.cases_head h2' <;> clear h2'
State after:
case inl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝¹ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h✝ : c = Config.haltedOn o2 regs2
⊢ d [S.prog]==>* Config.haltedOn o2 regs2

case inr
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝¹ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h✝ : ∃ c_1, (c [S.prog]==> c_1) ∧ Relation.ReflTransGen (stepsTo S.prog) c_1 (Config.haltedOn o2 regs2)
⊢ d [S.prog]==>* Config.haltedOn o2 regs2

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h2' : c = Config.haltedOn o2 regs2
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
case inl h2' =>
  cases h2'
  have : _ = d := by
    apply halt_is_fixpoint _ (Relation.ReflTransGen.single h)
    simp
  rw [←this]
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h2' : ∃ c_1, (c [S.prog]==> c_1) ∧ Relation.ReflTransGen (stepsTo S.prog) c_1 (Config.haltedOn o2 regs2)
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
case inr h2' =>
  rcases h2' with ⟨c',hc,h⟩
  have : c' = d := stepsTo_functional _ hc ‹_›
  rw [←this]
  exact h
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h2' : c = Config.haltedOn o2 regs2
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
cases h2'
State after:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
d : Config (WithIO R) L
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h : Config.haltedOn o2 regs2 [S.prog]==> d
⊢ d [S.prog]==>* Config.haltedOn o2 regs2

State before:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
d : Config (WithIO R) L
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h : Config.haltedOn o2 regs2 [S.prog]==> d
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
have : _ = d := by
  apply halt_is_fixpoint _ (Relation.ReflTransGen.single h)
  simp
State after:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
d : Config (WithIO R) L
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h : Config.haltedOn o2 regs2 [S.prog]==> d
this : Config.haltedOn o2 regs2 = d
⊢ d [S.prog]==>* Config.haltedOn o2 regs2

State before:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
d : Config (WithIO R) L
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h : Config.haltedOn o2 regs2 [S.prog]==> d
this : Config.haltedOn o2 regs2 = d
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
rw [←this]
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
d : Config (WithIO R) L
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h : Config.haltedOn o2 regs2 [S.prog]==> d
⊢ ?m.54568 = d
Tactic:
apply halt_is_fixpoint _ (Relation.ReflTransGen.single h)
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
d : Config (WithIO R) L
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h : Config.haltedOn o2 regs2 [S.prog]==> d
⊢ Config.is_halted (Config.haltedOn o2 regs2) = true

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
d : Config (WithIO R) L
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h : Config.haltedOn o2 regs2 [S.prog]==> d
⊢ Config.is_halted (Config.haltedOn o2 regs2) = true
Tactic:
simp
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h2' : ∃ c_1, (c [S.prog]==> c_1) ∧ Relation.ReflTransGen (stepsTo S.prog) c_1 (Config.haltedOn o2 regs2)
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
rcases h2' with ⟨c',hc,h⟩
State after:
case intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h✝¹ : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
c' : Config (WithIO R) L
hc : c [S.prog]==> c'
h : Relation.ReflTransGen (stepsTo S.prog) c' (Config.haltedOn o2 regs2)
⊢ d [S.prog]==>* Config.haltedOn o2 regs2

State before:
case intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h✝¹ : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
c' : Config (WithIO R) L
hc : c [S.prog]==> c'
h : Relation.ReflTransGen (stepsTo S.prog) c' (Config.haltedOn o2 regs2)
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
have : c' = d := stepsTo_functional _ hc ‹_›
State after:
case intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h✝¹ : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
c' : Config (WithIO R) L
hc : c [S.prog]==> c'
h : Relation.ReflTransGen (stepsTo S.prog) c' (Config.haltedOn o2 regs2)
this : c' = d
⊢ d [S.prog]==>* Config.haltedOn o2 regs2

State before:
case intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h✝¹ : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
c' : Config (WithIO R) L
hc : c [S.prog]==> c'
h : Relation.ReflTransGen (stepsTo S.prog) c' (Config.haltedOn o2 regs2)
this : c' = d
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
rw [←this]
State after:
case intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h✝¹ : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
c' : Config (WithIO R) L
hc : c [S.prog]==> c'
h : Relation.ReflTransGen (stepsTo S.prog) c' (Config.haltedOn o2 regs2)
this : c' = d
⊢ c' [S.prog]==>* Config.haltedOn o2 regs2

State before:
case intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h✝¹ : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
c' : Config (WithIO R) L
hc : c [S.prog]==> c'
h : Relation.ReflTransGen (stepsTo S.prog) c' (Config.haltedOn o2 regs2)
this : c' = d
⊢ c' [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
exact h
State after:
no goals