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

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
⊢ rcn e₂ ≮[s₁.rtr] rcn e₁
Tactic:
by_contra d
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
d : rcn e₂ <[s₁.rtr] rcn e₁
⊢ False

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
d : rcn e₂ <[s₁.rtr] rcn e₁
⊢ False
Tactic:
exact e₂.allows_rcn.unprocessed $ e₁.progress_monotonic $ e₁.allows_rcn.deps d
State after:
no goals