internlm/Lean-Github huggingface dataset:
Theorem: RegMachine.halt_is_fixpoint
Proof 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
Proof 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
Theorem: RegMachine.halt_is_fixpoint
Proof 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
Proof state after:
no goals
Theorem: RegMachine.halt_is_fixpoint
Proof 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'
Proof state after:
no goals
Theorem: RegMachine.halt_is_fixpoint
Proof 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
Proof state after:
no goals
Theorem: RegMachine.halt_is_fixpoint
Proof 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'
Proof 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
Theorem: RegMachine.halt_is_fixpoint
Proof 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 ⊢
Proof 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
Theorem: RegMachine.halt_is_fixpoint
Proof 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
Proof 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
Theorem: RegMachine.halt_is_fixpoint
Proof 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
Proof 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
Theorem: RegMachine.halt_is_fixpoint
Proof 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'
Proof state after:
no goals
Theorem: RegMachine.halt_is_unique
Proof 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
Proof 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
Theorem: RegMachine.halt_is_unique
Proof 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
Proof state after:
no goals
Theorem: RegMachine.halt_is_unique
Proof 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
Proof state after:
no goals
Theorem: RegMachine.halt_is_unique
Proof 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
Proof state after:
no goals
Theorem: RegMachine.halt_is_unique
Proof 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
Proof 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
Theorem: RegMachine.halt_is_unique
Proof 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
Proof 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
Theorem: RegMachine.halt_is_unique
Proof 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
Proof 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
Theorem: RegMachine.halt_is_unique
Proof 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
Proof state after:
no goals
Theorem: RegMachine.halt_is_unique
Proof 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
Proof state after:
no goals
Theorem: RegMachine.halt_is_unique
Proof 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
Proof 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
Theorem: RegMachine.halt_is_unique
Proof 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
Proof 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
Theorem: RegMachine.halt_is_unique
Proof 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
Proof 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
Theorem: RegMachine.halt_is_unique
Proof 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
Proof state after:
no goals
Theorem: RegMachine.halt_is_unique
Proof 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
Proof 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
Theorem: RegMachine.halt_is_unique
Proof 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
Proof 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
Theorem: RegMachine.halt_is_unique
Proof 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
Proof state after:
no goals
Theorem: RegMachine.halt_is_unique
Proof 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
Proof state after:
no goals
Theorem: RegMachine.halt_is_unique
Proof 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
Proof state after:
no goals
Theorem: RegMachine.halt_is_unique
Proof 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⟩
Proof 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
Theorem: RegMachine.halt_is_unique
Proof 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
Proof 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
Theorem: RegMachine.halt_is_unique
Proof 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
Proof 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
Theorem: RegMachine.halt_is_unique
Proof 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
Proof state after:
no goals