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

State before:
R✝ L✝ : Type
Start✝ : ?m.45031
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.45045) true
R L : Type
x✝ : Sort ?u.45030
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.45045) true
c d : Config R L
h : c [P]==>* d
⊢ Config.is_halted c = true → c = d
Tactic:
induction h using Relation.ReflTransGen.head_induction_on
State after:
case refl
R✝ L✝ : Type
Start✝ : ?m.45031
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.45045) true
R L : Type
x✝ : Sort ?u.45030
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.45045) true
c d : Config R L
⊢ Config.is_halted d = true → d = d

case head
R✝ L✝ : Type
Start✝ : ?m.45031
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.45045) true
R L : Type
x✝ : Sort ?u.45030
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.45045) true
c d a✝¹ c✝ : Config R L
h'✝ : a✝¹ [P]==> c✝
h✝ : Relation.ReflTransGen (stepsTo P) c✝ d
a✝ : Config.is_halted c✝ = true → c✝ = d
⊢ Config.is_halted a✝¹ = true → a✝¹ = d

State before:
R✝ L✝ : Type
Start✝ : ?m.45031
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.45045) true
R L : Type
x✝ : Sort ?u.45030
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.45045) true
c d : Config R L
⊢ Config.is_halted d = true → d = d
Tactic:
case refl => simp
State after:
no goals

State before:
R✝ L✝ : Type
Start✝ : ?m.45031
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.45045) true
R L : Type
x✝ : Sort ?u.45030
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.45045) true
c d c' d' : Config R L
h : c' [P]==> d'
h✝ : Relation.ReflTransGen (stepsTo P) d' d
ih : Config.is_halted d' = true → d' = d
⊢ Config.is_halted c' = true → c' = d
Tactic:
case head c' d' h _ ih =>
  intro hc'
  simp [Config.is_halted] at hc' ih ⊢
  simp [step, hc'] at h
  cases h
  apply ih hc'
State after:
no goals

State before:
R✝ L✝ : Type
Start✝ : ?m.45031
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.45045) true
R L : Type
x✝ : Sort ?u.45030
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.45045) true
c d : Config R L
⊢ Config.is_halted d = true → d = d
Tactic:
simp
State after:
no goals

State before:
R✝ L✝ : Type
Start✝ : ?m.45031
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.45045) true
R L : Type
x✝ : Sort ?u.45030
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.45045) true
c d c' d' : Config R L
h : c' [P]==> d'
h✝ : Relation.ReflTransGen (stepsTo P) d' d
ih : Config.is_halted d' = true → d' = d
⊢ Config.is_halted c' = true → c' = d
Tactic:
intro hc'
State after:
R✝ L✝ : Type
Start✝ : ?m.45031
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.45045) true
R L : Type
x✝ : Sort ?u.45030
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.45045) true
c d c' d' : Config R L
h : c' [P]==> d'
h✝ : Relation.ReflTransGen (stepsTo P) d' d
ih : Config.is_halted d' = true → d' = d
hc' : Config.is_halted c' = true
⊢ c' = d

State before:
R✝ L✝ : Type
Start✝ : ?m.45031
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.45045) true
R L : Type
x✝ : Sort ?u.45030
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.45045) true
c d c' d' : Config R L
h : c' [P]==> d'
h✝ : Relation.ReflTransGen (stepsTo P) d' d
ih : Config.is_halted d' = true → d' = d
hc' : Config.is_halted c' = true
⊢ c' = d
Tactic:
simp [Config.is_halted] at hc' ih ⊢
State after:
R✝ L✝ : Type
Start✝ : ?m.45031
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.45045) true
R L : Type
x✝ : Sort ?u.45030
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.45045) true
c d c' d' : Config R L
h : c' [P]==> d'
h✝ : Relation.ReflTransGen (stepsTo P) d' d
hc' : c'.ip = none
ih : d'.ip = none → d' = d
⊢ c' = d

State before:
R✝ L✝ : Type
Start✝ : ?m.45031
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.45045) true
R L : Type
x✝ : Sort ?u.45030
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.45045) true
c d c' d' : Config R L
h : c' [P]==> d'
h✝ : Relation.ReflTransGen (stepsTo P) d' d
hc' : c'.ip = none
ih : d'.ip = none → d' = d
⊢ c' = d
Tactic:
simp [step, hc'] at h
State after:
R✝ L✝ : Type
Start✝ : ?m.45031
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.45045) true
R L : Type
x✝ : Sort ?u.45030
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.45045) true
c d c' d' : Config R L
h✝ : Relation.ReflTransGen (stepsTo P) d' d
hc' : c'.ip = none
ih : d'.ip = none → d' = d
h : c' = d'
⊢ c' = d

State before:
R✝ L✝ : Type
Start✝ : ?m.45031
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.45045) true
R L : Type
x✝ : Sort ?u.45030
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.45045) true
c d c' d' : Config R L
h✝ : Relation.ReflTransGen (stepsTo P) d' d
hc' : c'.ip = none
ih : d'.ip = none → d' = d
h : c' = d'
⊢ c' = d
Tactic:
cases h
State after:
case refl
R✝ L✝ : Type
Start✝ : ?m.45031
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.45045) true
R L : Type
x✝ : Sort ?u.45030
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.45045) true
c d c' : Config R L
hc' : c'.ip = none
h✝ : Relation.ReflTransGen (stepsTo P) c' d
ih : c'.ip = none → c' = d
⊢ c' = d

State before:
case refl
R✝ L✝ : Type
Start✝ : ?m.45031
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.45045) true
R L : Type
x✝ : Sort ?u.45030
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.45045) true
c d c' : Config R L
hc' : c'.ip = none
h✝ : Relation.ReflTransGen (stepsTo P) c' d
ih : c'.ip = none → c' = d
⊢ c' = d
Tactic:
apply ih hc'
State after:
no goals