Theorem: RegMachine.halt_is_unique (RegMachine/Basic.lean)

State before:
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
c d1 d2 : Config R L
h1 : c [P]==>* d1
h2 : c [P]==>* d2
hd1 : Config.is_halted d1 = true
hd2 : Config.is_halted d2 = true
⊢ d1 = d2
Tactic:
induction h1 using Relation.ReflTransGen.head_induction_on
State after:
case refl
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
c d1 d2 : Config R L
hd1 : Config.is_halted d1 = true
hd2 : Config.is_halted d2 = true
h2 : d1 [P]==>* d2
⊢ d1 = d2

case head
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
c d1 d2 : Config R L
hd1 : Config.is_halted d1 = true
hd2 : Config.is_halted d2 = true
a✝¹ c✝ : Config R L
h'✝ : a✝¹ [P]==> c✝
h✝ : Relation.ReflTransGen (stepsTo P) c✝ d1
a✝ : c✝ [P]==>* d2 → d1 = d2
h2 : a✝¹ [P]==>* d2
⊢ d1 = d2

State before:
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
c d1 d2 : Config R L
hd1 : Config.is_halted d1 = true
hd2 : Config.is_halted d2 = true
h2 : d1 [P]==>* d2
⊢ d1 = d2
Tactic:
case refl =>
  apply halt_is_fixpoint _ h2 hd1
State after:
no goals

State before:
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
c d1 d2 : Config R L
hd1 : Config.is_halted d1 = true
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h : c' [P]==> d'
_h : Relation.ReflTransGen (stepsTo P) d' d1
ih : d' [P]==>* d2 → d1 = d2
h2 : c' [P]==>* d2
⊢ d1 = d2
Tactic:
case head c' d' h _h ih =>
  apply ih
  clear ih _h hd1 d1 c
  cases Relation.ReflTransGen.cases_head h2 <;> clear h2
  case inl h2 =>
    cases h2
    have : d2 = d' := by
      apply halt_is_fixpoint
      . exact Relation.ReflTransGen.single h
      . exact hd2
    cases this; apply Relation.ReflTransGen.refl
  case inr h2 =>
    rcases h2 with ⟨c,hc,h2⟩
    have : c = d' := stepsTo_functional _ hc h
    cases this
    exact h2
State after:
no goals

State before:
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
c d1 d2 : Config R L
hd1 : Config.is_halted d1 = true
hd2 : Config.is_halted d2 = true
h2 : d1 [P]==>* d2
⊢ d1 = d2
Tactic:
apply halt_is_fixpoint _ h2 hd1
State after:
no goals

State before:
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
c d1 d2 : Config R L
hd1 : Config.is_halted d1 = true
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h : c' [P]==> d'
_h : Relation.ReflTransGen (stepsTo P) d' d1
ih : d' [P]==>* d2 → d1 = d2
h2 : c' [P]==>* d2
⊢ d1 = d2
Tactic:
apply ih
State after:
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
c d1 d2 : Config R L
hd1 : Config.is_halted d1 = true
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h : c' [P]==> d'
_h : Relation.ReflTransGen (stepsTo P) d' d1
ih : d' [P]==>* d2 → d1 = d2
h2 : c' [P]==>* d2
⊢ d' [P]==>* d2

State before:
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
c d1 d2 : Config R L
hd1 : Config.is_halted d1 = true
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h : c' [P]==> d'
_h : Relation.ReflTransGen (stepsTo P) d' d1
ih : d' [P]==>* d2 → d1 = d2
h2 : c' [P]==>* d2
⊢ d' [P]==>* d2
Tactic:
clear ih _h hd1 d1 c
State after:
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h : c' [P]==> d'
h2 : c' [P]==>* d2
⊢ d' [P]==>* d2

State before:
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h : c' [P]==> d'
h2 : c' [P]==>* d2
⊢ d' [P]==>* d2
Tactic:
cases Relation.ReflTransGen.cases_head h2 <;> clear h2
State after:
case inl
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h : c' [P]==> d'
h✝ : c' = d2
⊢ d' [P]==>* d2

case inr
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h : c' [P]==> d'
h✝ : ∃ c, (c' [P]==> c) ∧ Relation.ReflTransGen (stepsTo P) c d2
⊢ d' [P]==>* d2

State before:
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h : c' [P]==> d'
h2 : c' = d2
⊢ d' [P]==>* d2
Tactic:
case inl h2 =>
  cases h2
  have : d2 = d' := by
    apply halt_is_fixpoint
    . exact Relation.ReflTransGen.single h
    . exact hd2
  cases this; apply Relation.ReflTransGen.refl
State after:
no goals

State before:
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h : c' [P]==> d'
h2 : ∃ c, (c' [P]==> c) ∧ Relation.ReflTransGen (stepsTo P) c d2
⊢ d' [P]==>* d2
Tactic:
case inr h2 =>
  rcases h2 with ⟨c,hc,h2⟩
  have : c = d' := stepsTo_functional _ hc h
  cases this
  exact h2
State after:
no goals

State before:
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h : c' [P]==> d'
h2 : c' = d2
⊢ d' [P]==>* d2
Tactic:
cases h2
State after:
case refl
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
d' : Config R L
h : d2 [P]==> d'
⊢ d' [P]==>* d2

State before:
case refl
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
d' : Config R L
h : d2 [P]==> d'
⊢ d' [P]==>* d2
Tactic:
have : d2 = d' := by
  apply halt_is_fixpoint
  . exact Relation.ReflTransGen.single h
  . exact hd2
State after:
case refl
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
d' : Config R L
h : d2 [P]==> d'
this : d2 = d'
⊢ d' [P]==>* d2

State before:
case refl
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
d' : Config R L
h : d2 [P]==> d'
this : d2 = d'
⊢ d' [P]==>* d2
Tactic:
cases this
State after:
case refl.refl
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
h : d2 [P]==> d2
⊢ d2 [P]==>* d2

State before:
case refl.refl
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
h : d2 [P]==> d2
⊢ d2 [P]==>* d2
Tactic:
apply Relation.ReflTransGen.refl
State after:
no goals

State before:
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
d' : Config R L
h : d2 [P]==> d'
⊢ d2 = d'
Tactic:
apply halt_is_fixpoint
State after:
case h
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
d' : Config R L
h : d2 [P]==> d'
⊢ d2 [?P]==>* d'

case a
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
d' : Config R L
h : d2 [P]==> d'
⊢ Config.is_halted d2 = true

case P
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
d' : Config R L
h : d2 [P]==> d'
⊢ Prog R L

State before:
case h
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
d' : Config R L
h : d2 [P]==> d'
⊢ d2 [?P]==>* d'

case a
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
d' : Config R L
h : d2 [P]==> d'
⊢ Config.is_halted d2 = true

case P
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
d' : Config R L
h : d2 [P]==> d'
⊢ Prog R L
Tactic:
. exact Relation.ReflTransGen.single h
State after:
case a
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
d' : Config R L
h : d2 [P]==> d'
⊢ Config.is_halted d2 = true

State before:
case a
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
d' : Config R L
h : d2 [P]==> d'
⊢ Config.is_halted d2 = true
Tactic:
. exact hd2
State after:
no goals

State before:
case h
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
d' : Config R L
h : d2 [P]==> d'
⊢ d2 [?P]==>* d'
Tactic:
exact Relation.ReflTransGen.single h
State after:
no goals

State before:
case a
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
d' : Config R L
h : d2 [P]==> d'
⊢ Config.is_halted d2 = true
Tactic:
exact hd2
State after:
no goals

State before:
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h : c' [P]==> d'
h2 : ∃ c, (c' [P]==> c) ∧ Relation.ReflTransGen (stepsTo P) c d2
⊢ d' [P]==>* d2
Tactic:
rcases h2 with ⟨c,hc,h2⟩
State after:
case intro.intro
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h : c' [P]==> d'
c : Config R L
hc : c' [P]==> c
h2 : Relation.ReflTransGen (stepsTo P) c d2
⊢ d' [P]==>* d2

State before:
case intro.intro
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h : c' [P]==> d'
c : Config R L
hc : c' [P]==> c
h2 : Relation.ReflTransGen (stepsTo P) c d2
⊢ d' [P]==>* d2
Tactic:
have : c = d' := stepsTo_functional _ hc h
State after:
case intro.intro
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h : c' [P]==> d'
c : Config R L
hc : c' [P]==> c
h2 : Relation.ReflTransGen (stepsTo P) c d2
this : c = d'
⊢ d' [P]==>* d2

State before:
case intro.intro
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h : c' [P]==> d'
c : Config R L
hc : c' [P]==> c
h2 : Relation.ReflTransGen (stepsTo P) c d2
this : c = d'
⊢ d' [P]==>* d2
Tactic:
cases this
State after:
case intro.intro.refl
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h hc : c' [P]==> d'
h2 : Relation.ReflTransGen (stepsTo P) d' d2
⊢ d' [P]==>* d2

State before:
case intro.intro.refl
R✝ L✝ : Type
Start✝ : ?m.50738
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.50752) true
R L : Type
x✝ : Sort ?u.50737
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.50752) true
d2 : Config R L
hd2 : Config.is_halted d2 = true
c' d' : Config R L
h hc : c' [P]==> d'
h2 : Relation.ReflTransGen (stepsTo P) d' d2
⊢ d' [P]==>* d2
Tactic:
exact h2
State after:
no goals