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

State before:
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
⊢ c [P]==>+ d
Tactic:
cases Relation.ReflTransGen.cases_head h
State after:
case inl
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
h✝ : c = d
⊢ c [P]==>+ d

case inr
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
h✝ : ∃ c_1, (c [P]==> c_1) ∧ Relation.ReflTransGen (stepsTo P) c_1 d
⊢ c [P]==>+ d

State before:
case inl
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
h✝ : c = d
⊢ c [P]==>+ d

case inr
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
h✝ : ∃ c_1, (c [P]==> c_1) ∧ Relation.ReflTransGen (stepsTo P) c_1 d
⊢ c [P]==>+ d
Tactic:
clear h
State after:
case inl
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
h✝ : c = d
⊢ c [P]==>+ d

case inr
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
h✝ : ∃ c_1, (c [P]==> c_1) ∧ Relation.ReflTransGen (stepsTo P) c_1 d
⊢ c [P]==>+ d

State before:
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
heq : c = d
⊢ c [P]==>+ d
Tactic:
case inl heq =>
  cases heq; contradiction
State after:
no goals

State before:
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h✝ : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
h : ∃ c_1, (c [P]==> c_1) ∧ Relation.ReflTransGen (stepsTo P) c_1 d
⊢ c [P]==>+ d
Tactic:
case inr h =>
  rcases h with ⟨c',hc_c',hc'_d⟩
  exact Relation.TransGen.head' hc_c' hc'_d
State after:
no goals

State before:
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
heq : c = d
⊢ c [P]==>+ d
Tactic:
cases heq
State after:
case refl
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c : Config R L
hc : ¬Config.is_halted c = true
hd : Config.is_halted c = true
⊢ c [P]==>+ c

State before:
case refl
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c : Config R L
hc : ¬Config.is_halted c = true
hd : Config.is_halted c = true
⊢ c [P]==>+ c
Tactic:
contradiction
State after:
no goals

State before:
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h✝ : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
h : ∃ c_1, (c [P]==> c_1) ∧ Relation.ReflTransGen (stepsTo P) c_1 d
⊢ c [P]==>+ d
Tactic:
rcases h with ⟨c',hc_c',hc'_d⟩
State after:
case intro.intro
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
c' : Config R L
hc_c' : c [P]==> c'
hc'_d : Relation.ReflTransGen (stepsTo P) c' d
⊢ c [P]==>+ d

State before:
case intro.intro
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
c' : Config R L
hc_c' : c [P]==> c'
hc'_d : Relation.ReflTransGen (stepsTo P) c' d
⊢ c [P]==>+ d
Tactic:
exact Relation.TransGen.head' hc_c' hc'_d
State after:
no goals