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

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ rcn e
⊢ Allows s₁ i ↔ Allows s₂ i
Tactic:
have a := e.apply
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ rcn e
a : s₁ -[output s₁ (rcn e)]→ (applied e)
⊢ Allows s₁ i ↔ Allows s₂ i

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ rcn e
a : s₁ -[output s₁ (rcn e)]→ (applied e)
⊢ Allows s₁ i ↔ Allows s₂ i
Tactic:
simp [e.dst_eq, ←Allows.iff_record_indep (a.preserves_independent hi).symm, a.allows_iff]
State after:
no goals