Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
c₁ c₂ : Change
s s₁ s₂ s₁₂ s₂₁ : State α
ht : Change.target c₁ ≠ Change.target c₂ ∨ Change.target c₁ = none
e₁ : s -[c₁]→ s₁
e₁₂ : s₁ -[c₂]→ s₁₂
e₂ : s -[c₂]→ s₂
e₂₁ : s₂ -[c₁]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
cases e₁ <;> cases e₁₂ <;> cases e₂ <;> cases e₂₁ <;> simp [Change.target] at ht ⊢
Proof state after:
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.act.act.inp
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }

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.act.act.out
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }

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.act.act.stv
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }

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 act.inp.inp.act
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹

case act.out.out.act
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹

case act.stv.stv.act
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹

case act.act.act.act
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝¹ : _root_.Time
v✝¹ : Value
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : ¬i✝¹ = i✝
⊢ schedule (schedule s i✝¹ t✝¹ v✝¹) i✝ t✝ v✝ = schedule (schedule s i✝ t✝ v✝) i✝¹ t✝¹ v✝¹

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✝