Theorem: Execution.State.Over.forcing_exec_step_rcn_eq (ReactorModel/Execution/Theorems/StateOver.lean)

State before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s✝ : State.Over rtr✝
rtr : α
rcn : ID
s : State α
e : (forcing rtr rcn).toState ↓ₑ s
⊢ Step.Exec.rcn e = rcn
Tactic:
have h := e.allows_rcn.unprocessed
State after:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s✝ : State.Over rtr✝
rtr : α
rcn : ID
s : State α
e : (forcing rtr rcn).toState ↓ₑ s
h : Step.Exec.rcn e ∉ (forcing rtr rcn).progress
⊢ Step.Exec.rcn e = rcn

State before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s✝ : State.Over rtr✝
rtr : α
rcn : ID
s : State α
e : (forcing rtr rcn).toState ↓ₑ s
h : Step.Exec.rcn e ∉ (forcing rtr rcn).progress
⊢ Step.Exec.rcn e = rcn
Tactic:
simp [forcing] at h
State after:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s✝ : State.Over rtr✝
rtr : α
rcn : ID
s : State α
e : (forcing rtr rcn).toState ↓ₑ s
h : Step.Exec.rcn e ∈ Partial.ids (rtr[Component.rcn]) → Step.Exec.rcn e = rcn
⊢ Step.Exec.rcn e = rcn

State before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s✝ : State.Over rtr✝
rtr : α
rcn : ID
s : State α
e : (forcing rtr rcn).toState ↓ₑ s
h : Step.Exec.rcn e ∈ Partial.ids (rtr[Component.rcn]) → Step.Exec.rcn e = rcn
⊢ Step.Exec.rcn e = rcn
Tactic:
exact h e.allows_rcn.mem
State after:
no goals