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

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
s₁' s₂' : State α
e : s₁ -[c]→ s₂
e' : s₁' -[c]→ s₂'
h : s₁.rtr = s₁'.rtr
⊢ s₂.rtr = s₂'.rtr
Tactic:
cases e <;> cases e' <;> simp [State.schedule_preserves_rtr, h]
State after:
case inp.inp
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s₁.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝

case out.out
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s₁.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝

case stv.stv
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝

State before:
case inp.inp
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s₁.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝

case out.out
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s₁.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝

case stv.stv
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝
Tactic:
all_goals rw [h] at *; exact LawfulUpdate.unique ‹_› ‹_›
State after:
no goals

State before:
case stv.stv
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝
Tactic:
rw [h] at *
State after:
case stv.stv
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁'.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁'.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝

State before:
case stv.stv
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁'.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁'.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝
Tactic:
exact LawfulUpdate.unique ‹_› ‹_›
State after:
no goals