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

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
out : Reaction.Output
rcn : ID
e₁ : s -[out]→ s₁
e₂ : (record s rcn) -[out]→ s₂
⊢ record s₁ rcn = s₂
Tactic:
induction e₁ <;> cases e₂
State after:
case refl.refl
α : Type
inst✝ : Readable α
s s₁ : State α
out : Reaction.Output
rcn : ID
s✝ : State α
⊢ record s✝ rcn = record s✝ rcn

case trans.trans
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
out : Reaction.Output
rcn : ID
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
s₃✝ : State α
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
a✝² : s₂✝¹ -[tl✝]→ s₃✝
a_ih✝ : (record s₂✝¹ rcn) -[tl✝]→ s₂ → record s₃✝ rcn = s₂
s₂✝ : State α
a✝¹ : (record s₁✝ rcn) -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂
⊢ record s₃✝ rcn = s₂

State before:
α : Type
inst✝ : Readable α
s s₁ : State α
out : Reaction.Output
rcn : ID
s✝ : State α
⊢ record s✝ rcn = record s✝ rcn
Tactic:
case refl.refl => rfl
State after:
no goals

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
out : Reaction.Output
rcn : ID
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e₁ : s₁✝ -[hd✝]→ s₂✝¹
a✝ : s₂✝¹ -[tl✝]→ s₃✝
hi : (record s₂✝¹ rcn) -[tl✝]→ s₂ → record s₃✝ rcn = s₂
s₂✝ : State α
e₂ : (record s₁✝ rcn) -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂
⊢ record s₃✝ rcn = s₂
Tactic:
case trans.trans e₁ _ hi _ e₂ e₂' => exact hi $ (e₁.comm_record e₂).symm ▸ e₂'
State after:
no goals

State before:
α : Type
inst✝ : Readable α
s s₁ : State α
out : Reaction.Output
rcn : ID
s✝ : State α
⊢ record s✝ rcn = record s✝ rcn
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
out : Reaction.Output
rcn : ID
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e₁ : s₁✝ -[hd✝]→ s₂✝¹
a✝ : s₂✝¹ -[tl✝]→ s₃✝
hi : (record s₂✝¹ rcn) -[tl✝]→ s₂ → record s₃✝ rcn = s₂
s₂✝ : State α
e₂ : (record s₁✝ rcn) -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂
⊢ record s₃✝ rcn = s₂
Tactic:
exact hi $ (e₁.comm_record e₂).symm ▸ e₂'
State after:
no goals