Theorem: Execution.Step.Time.RTC.deterministic (ReactorModel/Execution/Theorems/Trivial.lean)

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
ht : s₁.tag = s₂.tag
e₁ : RTC s s₁
e₂ : RTC s s₂
⊢ s₁ = s₂
Tactic:
induction e₁ generalizing s₂ <;> cases e₂
State after:
case refl.refl
α : Type
inst✝ : Proper α
s s₁ s✝ : State α
ht : s✝.tag = s✝.tag
⊢ s✝ = s✝

case refl.trans
α : Type
inst✝ : Proper α
s s₁ s✝ s₂ : State α
ht : s✝.tag = s₂.tag
s₂✝ : State α
a✝¹ : s✝ ↓ₜ s₂✝
a✝ : RTC s₂✝ s₂
⊢ s✝ = s₂

case trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ₜ s₂✝
a✝ : RTC s₂✝ s₃✝
a_ih✝ : ∀ {s₂ : State α}, s₃✝.tag = s₂.tag → RTC s₂✝ s₂ → s₃✝ = s₂
ht : s₃✝.tag = s₁✝.tag
⊢ s₃✝ = s₁✝

case trans.trans
α : Type
inst✝ : Proper α
s s₁ s₁✝ s₂✝¹ s₃✝ : State α
a✝³ : s₁✝ ↓ₜ s₂✝¹
a✝² : RTC s₂✝¹ s₃✝
a_ih✝ : ∀ {s₂ : State α}, s₃✝.tag = s₂.tag → RTC s₂✝¹ s₂ → s₃✝ = s₂
s₂ : State α
ht : s₃✝.tag = s₂.tag
s₂✝ : State α
a✝¹ : s₁✝ ↓ₜ s₂✝
a✝ : RTC s₂✝ s₂
⊢ s₃✝ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s✝ : State α
ht : s✝.tag = s✝.tag
⊢ s✝ = s✝
Tactic:
case refl.refl         => rfl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s✝ s₂ : State α
ht : s✝.tag = s₂.tag
s₂✝ : State α
e : s✝ ↓ₜ s₂✝
e' : RTC s₂✝ s₂
⊢ s✝ = s₂
Tactic:
case refl.trans e e'   => exact absurd ht      (ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le)
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ₜ s₂✝
e' : RTC s₂✝ s₃✝
a_ih✝ : ∀ {s₂ : State α}, s₃✝.tag = s₂.tag → RTC s₂✝ s₂ → s₃✝ = s₂
ht : s₃✝.tag = s₁✝.tag
⊢ s₃✝ = s₁✝
Tactic:
case trans.refl e e' _ => exact absurd ht.symm (ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le)
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₁✝ s₂✝¹ s₃✝ : State α
e₁ : s₁✝ ↓ₜ s₂✝¹
e₁' : RTC s₂✝¹ s₃✝
hi : ∀ {s₂ : State α}, s₃✝.tag = s₂.tag → RTC s₂✝¹ s₂ → s₃✝ = s₂
s₂ : State α
ht : s₃✝.tag = s₂.tag
s₂✝ : State α
e₂ : s₁✝ ↓ₜ s₂✝
e₂' : RTC s₂✝ s₂
⊢ s₃✝ = s₂
Tactic:
case trans.trans e₁ e₁' hi _ e₂ e₂' => exact hi ht (e₂.deterministic e₁ ▸ e₂')
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s✝ : State α
ht : s✝.tag = s✝.tag
⊢ s✝ = s✝
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s✝ s₂ : State α
ht : s✝.tag = s₂.tag
s₂✝ : State α
e : s✝ ↓ₜ s₂✝
e' : RTC s₂✝ s₂
⊢ s✝ = s₂
Tactic:
exact absurd ht      (ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le)
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ₜ s₂✝
e' : RTC s₂✝ s₃✝
a_ih✝ : ∀ {s₂ : State α}, s₃✝.tag = s₂.tag → RTC s₂✝ s₂ → s₃✝ = s₂
ht : s₃✝.tag = s₁✝.tag
⊢ s₃✝ = s₁✝
Tactic:
exact absurd ht.symm (ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le)
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₁✝ s₂✝¹ s₃✝ : State α
e₁ : s₁✝ ↓ₜ s₂✝¹
e₁' : RTC s₂✝¹ s₃✝
hi : ∀ {s₂ : State α}, s₃✝.tag = s₂.tag → RTC s₂✝¹ s₂ → s₃✝ = s₂
s₂ : State α
ht : s₃✝.tag = s₂.tag
s₂✝ : State α
e₂ : s₁✝ ↓ₜ s₂✝
e₂' : RTC s₂✝ s₂
⊢ s₃✝ = s₂
Tactic:
exact hi ht (e₂.deterministic e₁ ▸ e₂')
State after:
no goals