Theorem: Execution.Step.Apply.RTC.allows_iff (ReactorModel/Execution/Theorems/Step/Apply.lean)

State before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
e : s₁ -[out]→ s₂
⊢ Allows s₁ i ↔ Allows s₂ i
Tactic:
induction e
State after:
case refl
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
s✝ : State α
⊢ Allows s✝ i ↔ Allows s✝ i

case trans
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
a_ih✝ : Allows s₂✝ i ↔ Allows s₃✝ i
⊢ Allows s₁✝ i ↔ Allows s₃✝ i

State before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
s✝ : State α
⊢ Allows s✝ i ↔ Allows s✝ i
Tactic:
case refl => rfl
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : Allows s₂✝ i ↔ Allows s₃✝ i
⊢ Allows s₁✝ i ↔ Allows s₃✝ i
Tactic:
case trans e _ hi => exact e.allows_iff.trans hi
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
s✝ : State α
⊢ Allows s✝ i ↔ Allows s✝ i
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : Allows s₂✝ i ↔ Allows s₃✝ i
⊢ Allows s₁✝ i ↔ Allows s₃✝ i
Tactic:
exact e.allows_iff.trans hi
State after:
no goals