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

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂ s₂' s₁₂ s₂₁ : State α
c : Change
e : s₁ -[c]→ s₂
⊢ s₁.rtr ≈ s₂.rtr
Tactic:
cases e
State after:
case inp
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr ≈ { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr

case out
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr ≈ { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr

case stv
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr ≈ { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr

case act
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
t✝ : _root_.Time
v✝ : Value
⊢ s₁.rtr ≈ (schedule s₁ i✝ t✝ v✝).rtr

case mut
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
x✝ : Change.Mutation
⊢ s₁.rtr ≈ s₁.rtr

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
x✝ : Change.Mutation
⊢ s₁.rtr ≈ s₁.rtr
Tactic:
case «mut» => exact .refl _
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
t✝ : _root_.Time
v✝ : Value
⊢ s₁.rtr ≈ (schedule s₁ i✝ t✝ v✝).rtr
Tactic:
case act => simp [schedule_preserves_rtr]; exact .refl _
State after:
no goals

State before:
case inp
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr ≈ { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr

case out
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr ≈ { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr

case stv
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr ≈ { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr
Tactic:
all_goals exact LawfulUpdate.equiv ‹_›
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
x✝ : Change.Mutation
⊢ s₁.rtr ≈ s₁.rtr
Tactic:
exact .refl _
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
t✝ : _root_.Time
v✝ : Value
⊢ s₁.rtr ≈ (schedule s₁ i✝ t✝ v✝).rtr
Tactic:
simp [schedule_preserves_rtr]
State after:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
t✝ : _root_.Time
v✝ : Value
⊢ s₁.rtr ≈ s₁.rtr

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
t✝ : _root_.Time
v✝ : Value
⊢ s₁.rtr ≈ s₁.rtr
Tactic:
exact .refl _
State after:
no goals

State before:
case stv
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr ≈ { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr
Tactic:
exact LawfulUpdate.equiv ‹_›
State after:
no goals