Theorem: Execution.State.Terminal.not_elim (ReactorModel/Execution/Theorems/State.lean)

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
t : ¬Terminal s
⊢ ¬Closed s ∨ ∃ g, NextTag s g
Tactic:
by_contra h
State after:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
t : ¬Terminal s
h : ¬(¬Closed s ∨ ∃ g, NextTag s g)
⊢ False

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
t : ¬Terminal s
h : ¬(¬Closed s ∨ ∃ g, NextTag s g)
⊢ False
Tactic:
push_neg at h
State after:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
t : ¬Terminal s
h : Closed s ∧ ∀ (g : Time.Tag), ¬NextTag s g
⊢ False

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
t : ¬Terminal s
h : Closed s ∧ ∀ (g : Time.Tag), ¬NextTag s g
⊢ False
Tactic:
exact t ⟨h.left, h.right⟩
State after:
no goals