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

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ record s₁ rcn = s₂
Tactic:
ext1
State after:
case rtr
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).rtr = s₂.rtr

case tag
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).tag = s₂.tag

case progress
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).progress = s₂.progress

case events
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).events = s₂.events

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).rtr = s₂.rtr
Tactic:
case rtr      => exact e₁.rtr_congr e₂ (s.record_preserves_rtr rcn)
State after:
no goals

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).tag = s₂.tag
Tactic:
case tag      => simp [record_preserves_tag, ←e₁.preserves_tag, ←e₂.preserves_tag]
State after:
no goals

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).progress = s₂.progress
Tactic:
case progress => simp [record_progress_eq, ←e₂.preserves_progress, e₁.preserves_progress]
State after:
no goals

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).events = s₂.events
Tactic:
case events   => exact e₁.events_congr e₂ (s.record_preserves_events rcn)
State after:
no goals

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).rtr = s₂.rtr
Tactic:
exact e₁.rtr_congr e₂ (s.record_preserves_rtr rcn)
State after:
no goals

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).tag = s₂.tag
Tactic:
simp [record_preserves_tag, ←e₁.preserves_tag, ←e₂.preserves_tag]
State after:
no goals

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).progress = s₂.progress
Tactic:
simp [record_progress_eq, ←e₂.preserves_progress, e₁.preserves_progress]
State after:
no goals

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).events = s₂.events
Tactic:
exact e₁.events_congr e₂ (s.record_preserves_events rcn)
State after:
no goals