Theorem: Execution.Step.Exec.applied_rtr_eq (ReactorModel/Execution/Theorems/Step/Exec.lean)

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ (applied e).rtr = s₂.rtr
Tactic:
cases e
State after:
case mk
α : Type
inst✝ : Hierarchical α
s₁ : State α
rcn✝ : ID
s₂✝ : State α
a✝² : Allows s₁ rcn✝
a✝¹ : Triggers s₁ rcn✝
a✝ : s₁ -[output s₁ rcn✝]→ s₂✝
⊢ (applied (mk a✝² a✝¹ a✝)).rtr = (record s₂✝ rcn✝).rtr

State before:
case mk
α : Type
inst✝ : Hierarchical α
s₁ : State α
rcn✝ : ID
s₂✝ : State α
a✝² : Allows s₁ rcn✝
a✝¹ : Triggers s₁ rcn✝
a✝ : s₁ -[output s₁ rcn✝]→ s₂✝
⊢ (applied (mk a✝² a✝¹ a✝)).rtr = (record s₂✝ rcn✝).rtr
Tactic:
simp [applied, record_preserves_rtr]
State after:
no goals