Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
case inp.inp.inp.inp
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.inp i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.inp i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ rtr✝² = rtr✝

case inp.out.out.inp
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.out i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.inp i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case inp.stv.stv.inp
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.inp i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case inp.mut.mut.inp
α : Type
inst✝ : Proper α
s : State α
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝¹
x✝ : Change.Mutation
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝

case out.inp.inp.out
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.inp i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.out i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case out.out.out.out
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.out i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.out i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ rtr✝² = rtr✝

case out.stv.stv.out
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.out i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case out.mut.mut.out
α : Type
inst✝ : Proper α
s : State α
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝¹
x✝ : Change.Mutation
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝

case stv.inp.inp.stv
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.inp i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case stv.out.out.stv
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.out i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case stv.stv.stv.stv
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ rtr✝² = rtr✝

case stv.mut.mut.stv
α : Type
inst✝ : Proper α
s : State α
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
x✝ : Change.Mutation
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝

case mut.inp.inp.mut
α : Type
inst✝ : Proper α
s : State α
x✝ : Change.Mutation
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✝
ht : True
⊢ rtr✝¹ = rtr✝

case mut.out.out.mut
α : Type
inst✝ : Proper α
s : State α
x✝ : Change.Mutation
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✝
ht : True
⊢ rtr✝¹ = rtr✝

case mut.stv.stv.mut
α : Type
inst✝ : Proper α
s : State α
x✝ : Change.Mutation
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✝
ht : True
⊢ rtr✝¹ = rtr✝
Tactic:
all_goals
  try exact LawfulUpdate.unique ‹_› ‹_›
  try case _ u₁ _ _ _ u₂ _ u₃ _ u₄ => exact LawfulUpdate.ne_comm u₁ u₂ u₃ u₄ $ by simp [ht]
Proof state after:
no goals