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

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
h : rcn ∈ s₁.progress
⊢ rcn ∉ rcns e
Tactic:
induction e <;> simp [rcns]
State after:
case single
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
h : rcn ∈ s₁✝.progress
⊢ ¬rcn = Execution.Instantaneous.Step.rcn a✝

case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ s₂✝.progress → rcn ∉ rcns a✝
h : rcn ∈ s₁✝.progress
⊢ ¬(rcn = Execution.Instantaneous.Step.rcn a✝¹ ∨ rcn ∈ rcns a✝)

State before:
case single
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
h : rcn ∈ s₁✝.progress
⊢ ¬rcn = Execution.Instantaneous.Step.rcn a✝

case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ s₂✝.progress → rcn ∉ rcns a✝
h : rcn ∈ s₁✝.progress
⊢ ¬(rcn = Execution.Instantaneous.Step.rcn a✝¹ ∨ rcn ∈ rcns a✝)
Tactic:
case' trans e e' hi => simp [hi $ e.progress_monotonic h]
State after:
case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ s₂✝.progress → rcn ∉ rcns e'
h : rcn ∈ s₁✝.progress
⊢ ¬rcn = Execution.Instantaneous.Step.rcn e

case single
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
h : rcn ∈ s₁✝.progress
⊢ ¬rcn = Execution.Instantaneous.Step.rcn a✝

State before:
case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ s₂✝.progress → rcn ∉ rcns e'
h : rcn ∈ s₁✝.progress
⊢ ¬(rcn = Execution.Instantaneous.Step.rcn e ∨ rcn ∈ rcns e')
Tactic:
simp [hi $ e.progress_monotonic h]
State after:
case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ s₂✝.progress → rcn ∉ rcns e'
h : rcn ∈ s₁✝.progress
⊢ ¬rcn = Execution.Instantaneous.Step.rcn e