Theorem: Execution.Instantaneous.Step.TC.acyclic (ReactorModel/Execution/Theorems/Grouped/Instantaneous.lean)

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
h : rcn ∈ rcns e
⊢ rcn ≮[s₁.rtr] rcn
Tactic:
induction e <;> simp [rcns] at h <;> try cases ‹_ ∨ _›
State after:
case single
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
h : rcn = Execution.Instantaneous.Step.rcn a✝
⊢ rcn ≮[s₁✝.rtr] rcn

case trans.inl
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h✝ : rcn = Execution.Instantaneous.Step.rcn a✝¹
⊢ rcn ≮[s₁✝.rtr] rcn

case trans.inr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h✝ : rcn ∈ rcns a✝
⊢ rcn ≮[s₁✝.rtr] rcn

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
h : rcn = Execution.Instantaneous.Step.rcn e
⊢ rcn ≮[s₁✝.rtr] rcn
Tactic:
case single e           => exact h ▸ e.acyclic
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h : rcn = Execution.Instantaneous.Step.rcn e
⊢ rcn ≮[s₁✝.rtr] rcn
Tactic:
case trans.inl e _ _ h  => exact h ▸ e.acyclic
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h : rcn ∈ rcns a✝
⊢ rcn ≮[s₁✝.rtr] rcn
Tactic:
case trans.inr e _ hi h => exact (hi h).equiv (Reactor.Equivalent.symm e.equiv)
State after:
no goals

State before:
case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h : rcn = Execution.Instantaneous.Step.rcn a✝¹ ∨ rcn ∈ rcns a✝
⊢ rcn ≮[s₁✝.rtr] rcn
Tactic:
cases ‹_ ∨ _›
State after:
case trans.inl
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h✝ : rcn = Execution.Instantaneous.Step.rcn a✝¹
⊢ rcn ≮[s₁✝.rtr] rcn

case trans.inr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h✝ : rcn ∈ rcns a✝
⊢ rcn ≮[s₁✝.rtr] rcn

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
h : rcn = Execution.Instantaneous.Step.rcn e
⊢ rcn ≮[s₁✝.rtr] rcn
Tactic:
exact h ▸ e.acyclic
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h : rcn = Execution.Instantaneous.Step.rcn e
⊢ rcn ≮[s₁✝.rtr] rcn
Tactic:
exact h ▸ e.acyclic
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h : rcn ∈ rcns a✝
⊢ rcn ≮[s₁✝.rtr] rcn
Tactic:
exact (hi h).equiv (Reactor.Equivalent.symm e.equiv)
State after:
no goals