Theorem: Execution.to_timeStepRTC (ReactorModel/Execution/Theorems/Trivial.lean)

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
triv : State.Trivial s₁
e : s₁ ⇓ s₂
⊢ Step.Time.RTC s₁ s₂
Tactic:
induction e <;> try cases ‹_ ↓ _›
State after:
case refl
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
triv : State.Trivial s✝
⊢ Step.Time.RTC s✝ s✝

case trans.skip
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
s✝ : s₁✝ ↓ₛ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝

case trans.exec
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e✝ : s₁✝ ↓ₑ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝

case trans.time
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
t✝ : s₁✝ ↓ₜ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
triv : State.Trivial s✝
⊢ Step.Time.RTC s✝ s✝
Tactic:
case refl            => exact .refl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e : s₁✝ ↓ₛ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝
Tactic:
case trans.skip e    => exact absurd triv e.not_trivial
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e : s₁✝ ↓ₑ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝
Tactic:
case trans.exec e    => exact absurd triv e.not_trivial
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
hi : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e : s₁✝ ↓ₜ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝
Tactic:
case trans.time hi e => exact .trans e (hi $ e.preserves_trivial triv)
State after:
no goals

State before:
case trans
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ s₂✝
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
⊢ Step.Time.RTC s₁✝ s₃✝
Tactic:
cases ‹_ ↓ _›
State after:
case trans.skip
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
s✝ : s₁✝ ↓ₛ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝

case trans.exec
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e✝ : s₁✝ ↓ₑ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝

case trans.time
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
t✝ : s₁✝ ↓ₜ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
triv : State.Trivial s✝
⊢ Step.Time.RTC s✝ s✝
Tactic:
exact .refl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e : s₁✝ ↓ₛ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝
Tactic:
exact absurd triv e.not_trivial
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e : s₁✝ ↓ₑ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝
Tactic:
exact absurd triv e.not_trivial
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
hi : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e : s₁✝ ↓ₜ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝
Tactic:
exact .trans e (hi $ e.preserves_trivial triv)
State after:
no goals