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

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
ht : Disjoint (Reaction.Output.targets out₁) (Reaction.Output.targets out₂)
e₁ : s -[out₁]→ s₁
e₁₂ : s₁ -[out₂]→ s₁₂
e₂ : s -[out₂]→ s₂
e₂₁ : s₂ -[out₁]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
induction e₁ generalizing s₂ <;> cases e₁₂ <;> cases e₂ <;> cases e₂₁
State after:
case refl.refl.refl.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ : State α
c : Change
out out₁ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets [])
⊢ s₁₂ = s₁₂

case refl.trans.trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
s✝ : State α
hd✝ : Change
s₂✝¹ : State α
tl✝ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (hd✝ :: tl✝))
a✝³ : s✝ -[hd✝]→ s₂✝¹
a✝² : s₂✝¹ -[tl✝]→ s₁₂
s₂✝ : State α
a✝¹ : s✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

case trans.refl.refl.trans
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
ht : Disjoint (Reaction.Output.targets (hd✝ :: tl✝)) (Reaction.Output.targets [])
a✝² : s₂✝¹ -[tl✝]→ s₁₂
a_ih✝ :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl✝) (Reaction.Output.targets []) →
      s₁₂ -[[]]→ s₁₂ → s₂✝¹ -[[]]→ s₂ → s₂ -[tl✝]→ s₂₁ → s₁₂ = s₂₁
s₂✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

case trans.trans.trans.trans
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd✝¹ : Change
s₁✝ s₂✝³ : State α
tl✝¹ : Reaction.Output
s₃✝ : State α
a✝⁷ : s₁✝ -[hd✝¹]→ s₂✝³
a✝⁶ : s₂✝³ -[tl✝¹]→ s₃✝
s₂ : State α
hd✝ : Change
s₂✝² : State α
tl✝ : Reaction.Output
a_ih✝ :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl✝¹) (Reaction.Output.targets (hd✝ :: tl✝)) →
      s₃✝ -[hd✝ :: tl✝]→ s₁₂ → s₂✝³ -[hd✝ :: tl✝]→ s₂ → s₂ -[tl✝¹]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd✝¹ :: tl✝¹)) (Reaction.Output.targets (hd✝ :: tl✝))
a✝⁵ : s₃✝ -[hd✝]→ s₂✝²
a✝⁴ : s₂✝² -[tl✝]→ s₁₂
s₂✝¹ : State α
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
a✝² : s₂✝¹ -[tl✝]→ s₂
s₂✝ : State α
a✝¹ : s₂ -[hd✝¹]→ s₂✝
a✝ : s₂✝ -[tl✝¹]→ s₂₁
⊢ s₁₂ = s₂₁

State before:
α : Type
inst✝ : Proper α
s s₁ s₁₂ : State α
c : Change
out out₁ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets [])
⊢ s₁₂ = s₁₂
Tactic:
case refl.refl.refl.refl => rfl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
case trans.trans.trans.trans hd₁ s z₁ tl₁ _ e₁ e₁' hd₂ _ tl₂ hi e₂ e₂' _ f₂ f₂' _ f₁ f₁' =>
  have h₁ : ∀ {t}, hd₁.target = some t → ¬t ∈ Reaction.Output.targets (hd₂ :: tl₂) := by
    intro _ h hm₂
    have hm₁ := Reaction.Output.target_mem_targets (out := hd₁ :: tl₁) (by simp) h
    exact absurd rfl $ Set.disjoint_iff_forall_ne.mp ht hm₁ hm₂
  have h₂ : Disjoint tl₁.targets $ Reaction.Output.targets (hd₂ :: tl₂) := by
    simp [Set.disjoint_iff_forall_ne]
    intro _ _ hm₁ _ _ hm₂ h₁ h₂
    subst h₁ h₂
    exact Set.disjoint_left.mp ht (Reaction.Output.mem_targets_cons hm₁) hm₂
  have ⟨_, g₁⟩ := Apply.RTC.construct z₁ (hd₂ :: tl₂)
  cases ne_targets_comm_apply h₁ (trans f₂ f₂') f₁ e₁ g₁
  exact hi h₂ (.trans e₂ e₂') g₁ f₁'
State after:
no goals

State before:
case refl.trans.trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
s✝ : State α
hd✝ : Change
s₂✝¹ : State α
tl✝ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (hd✝ :: tl✝))
a✝³ : s✝ -[hd✝]→ s₂✝¹
a✝² : s₂✝¹ -[tl✝]→ s₁₂
s₂✝ : State α
a✝¹ : s✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

case trans.refl.refl.trans
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
ht : Disjoint (Reaction.Output.targets (hd✝ :: tl✝)) (Reaction.Output.targets [])
a✝² : s₂✝¹ -[tl✝]→ s₁₂
a_ih✝ :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl✝) (Reaction.Output.targets []) →
      s₁₂ -[[]]→ s₁₂ → s₂✝¹ -[[]]→ s₂ → s₂ -[tl✝]→ s₂₁ → s₁₂ = s₂₁
s₂✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
case' refl.trans.trans.refl e₁ e₁' _ e₂ e₂' => skip
State after:
case refl.trans.trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
s✝ : State α
hd✝ : Change
s₂✝¹ : State α
tl✝ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (hd✝ :: tl✝))
e₁ : s✝ -[hd✝]→ s₂✝¹
e₁' : s₂✝¹ -[tl✝]→ s₁₂
s₂✝ : State α
e₂ : s✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

case trans.refl.refl.trans
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
ht : Disjoint (Reaction.Output.targets (hd✝ :: tl✝)) (Reaction.Output.targets [])
a✝² : s₂✝¹ -[tl✝]→ s₁₂
a_ih✝ :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl✝) (Reaction.Output.targets []) →
      s₁₂ -[[]]→ s₁₂ → s₂✝¹ -[[]]→ s₂ → s₂ -[tl✝]→ s₂₁ → s₁₂ = s₂₁
s₂✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

State before:
case refl.trans.trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
s✝ : State α
hd✝ : Change
s₂✝¹ : State α
tl✝ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (hd✝ :: tl✝))
e₁ : s✝ -[hd✝]→ s₂✝¹
e₁' : s₂✝¹ -[tl✝]→ s₁₂
s₂✝ : State α
e₂ : s✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

case trans.refl.refl.trans
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
ht : Disjoint (Reaction.Output.targets (hd✝ :: tl✝)) (Reaction.Output.targets [])
a✝² : s₂✝¹ -[tl✝]→ s₁₂
a_ih✝ :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl✝) (Reaction.Output.targets []) →
      s₁₂ -[[]]→ s₁₂ → s₂✝¹ -[[]]→ s₂ → s₂ -[tl✝]→ s₂₁ → s₁₂ = s₂₁
s₂✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
case' trans.refl.refl.trans e₁ e₁' _ _ e₂ e₂' => skip
State after:
case trans.refl.refl.trans
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
e₁ : s₁✝ -[hd✝]→ s₂✝¹
ht : Disjoint (Reaction.Output.targets (hd✝ :: tl✝)) (Reaction.Output.targets [])
e₁' : s₂✝¹ -[tl✝]→ s₁₂
a_ih✝ :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl✝) (Reaction.Output.targets []) →
      s₁₂ -[[]]→ s₁₂ → s₂✝¹ -[[]]→ s₂ → s₂ -[tl✝]→ s₂₁ → s₁₂ = s₂₁
s₂✝ : State α
e₂ : s₁✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

case refl.trans.trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
s✝ : State α
hd✝ : Change
s₂✝¹ : State α
tl✝ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (hd✝ :: tl✝))
e₁ : s✝ -[hd✝]→ s₂✝¹
e₁' : s₂✝¹ -[tl✝]→ s₁₂
s₂✝ : State α
e₂ : s✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

State before:
case trans.refl.refl.trans
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
e₁ : s₁✝ -[hd✝]→ s₂✝¹
ht : Disjoint (Reaction.Output.targets (hd✝ :: tl✝)) (Reaction.Output.targets [])
e₁' : s₂✝¹ -[tl✝]→ s₁₂
a_ih✝ :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl✝) (Reaction.Output.targets []) →
      s₁₂ -[[]]→ s₁₂ → s₂✝¹ -[[]]→ s₂ → s₂ -[tl✝]→ s₂₁ → s₁₂ = s₂₁
s₂✝ : State α
e₂ : s₁✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

case refl.trans.trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
s✝ : State α
hd✝ : Change
s₂✝¹ : State α
tl✝ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (hd✝ :: tl✝))
e₁ : s✝ -[hd✝]→ s₂✝¹
e₁' : s₂✝¹ -[tl✝]→ s₁₂
s₂✝ : State α
e₂ : s✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
all_goals cases e₁.deterministic e₂; exact e₁'.deterministic e₂'
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₁₂ : State α
c : Change
out out₁ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets [])
⊢ s₁₂ = s₁₂
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
have h₁ : ∀ {t}, hd₁.target = some t → ¬t ∈ Reaction.Output.targets (hd₂ :: tl₂) := by
  intro _ h hm₂
  have hm₁ := Reaction.Output.target_mem_targets (out := hd₁ :: tl₁) (by simp) h
  exact absurd rfl $ Set.disjoint_iff_forall_ne.mp ht hm₁ hm₂
State after:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
⊢ s₁₂ = s₂₁

State before:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
⊢ s₁₂ = s₂₁
Tactic:
have h₂ : Disjoint tl₁.targets $ Reaction.Output.targets (hd₂ :: tl₂) := by
  simp [Set.disjoint_iff_forall_ne]
  intro _ _ hm₁ _ _ hm₂ h₁ h₂
  subst h₁ h₂
  exact Set.disjoint_left.mp ht (Reaction.Output.mem_targets_cons hm₁) hm₂
State after:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
h₂ : Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂))
⊢ s₁₂ = s₂₁

State before:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
h₂ : Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂))
⊢ s₁₂ = s₂₁
Tactic:
have ⟨_, g₁⟩ := Apply.RTC.construct z₁ (hd₂ :: tl₂)
State after:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
h₂ : Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂))
fst✝ : State α
g₁ : z₁ -[hd₂ :: tl₂]→ fst✝
⊢ s₁₂ = s₂₁

State before:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
h₂ : Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂))
fst✝ : State α
g₁ : z₁ -[hd₂ :: tl₂]→ fst✝
⊢ s₁₂ = s₂₁
Tactic:
cases ne_targets_comm_apply h₁ (trans f₂ f₂') f₁ e₁ g₁
State after:
case refl
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
h₂ : Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂))
g₁ : z₁ -[hd₂ :: tl₂]→ s₂✝
⊢ s₁₂ = s₂₁

State before:
case refl
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
h₂ : Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂))
g₁ : z₁ -[hd₂ :: tl₂]→ s₂✝
⊢ s₁₂ = s₂₁
Tactic:
exact hi h₂ (.trans e₂ e₂') g₁ f₁'
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
⊢ ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
Tactic:
intro _ h hm₂
State after:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
t✝ : Component.Valued × ID
h : Change.target hd₁ = some t✝
hm₂ : t✝ ∈ Reaction.Output.targets (hd₂ :: tl₂)
⊢ False

State before:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
t✝ : Component.Valued × ID
h : Change.target hd₁ = some t✝
hm₂ : t✝ ∈ Reaction.Output.targets (hd₂ :: tl₂)
⊢ False
Tactic:
have hm₁ := Reaction.Output.target_mem_targets (out := hd₁ :: tl₁) (by simp) h
State after:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
t✝ : Component.Valued × ID
h : Change.target hd₁ = some t✝
hm₂ : t✝ ∈ Reaction.Output.targets (hd₂ :: tl₂)
hm₁ : t✝ ∈ Reaction.Output.targets (hd₁ :: tl₁)
⊢ False

State before:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
t✝ : Component.Valued × ID
h : Change.target hd₁ = some t✝
hm₂ : t✝ ∈ Reaction.Output.targets (hd₂ :: tl₂)
hm₁ : t✝ ∈ Reaction.Output.targets (hd₁ :: tl₁)
⊢ False
Tactic:
exact absurd rfl $ Set.disjoint_iff_forall_ne.mp ht hm₁ hm₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
t✝ : Component.Valued × ID
h : Change.target hd₁ = some t✝
hm₂ : t✝ ∈ Reaction.Output.targets (hd₂ :: tl₂)
⊢ hd₁ ∈ hd₁ :: tl₁
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
⊢ Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂))
Tactic:
simp [Set.disjoint_iff_forall_ne]
State after:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
⊢ ∀ (a : Component.Valued) (b : ID),
    (a, b) ∈ Reaction.Output.targets tl₁ →
      ∀ (a_2 : Component.Valued) (b_1 : ID), (a_2, b_1) ∈ Reaction.Output.targets (hd₂ :: tl₂) → a = a_2 → ¬b = b_1

State before:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
⊢ ∀ (a : Component.Valued) (b : ID),
    (a, b) ∈ Reaction.Output.targets tl₁ →
      ∀ (a_2 : Component.Valued) (b_1 : ID), (a_2, b_1) ∈ Reaction.Output.targets (hd₂ :: tl₂) → a = a_2 → ¬b = b_1
Tactic:
intro _ _ hm₁ _ _ hm₂ h₁ h₂
State after:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
h₁✝ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
a✝¹ : Component.Valued
b✝¹ : ID
hm₁ : (a✝¹, b✝¹) ∈ Reaction.Output.targets tl₁
a✝ : Component.Valued
b✝ : ID
hm₂ : (a✝, b✝) ∈ Reaction.Output.targets (hd₂ :: tl₂)
h₁ : a✝¹ = a✝
h₂ : b✝¹ = b✝
⊢ False

State before:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
h₁✝ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
a✝¹ : Component.Valued
b✝¹ : ID
hm₁ : (a✝¹, b✝¹) ∈ Reaction.Output.targets tl₁
a✝ : Component.Valued
b✝ : ID
hm₂ : (a✝, b✝) ∈ Reaction.Output.targets (hd₂ :: tl₂)
h₁ : a✝¹ = a✝
h₂ : b✝¹ = b✝
⊢ False
Tactic:
subst h₁ h₂
State after:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
a✝ : Component.Valued
b✝ : ID
hm₁ : (a✝, b✝) ∈ Reaction.Output.targets tl₁
hm₂ : (a✝, b✝) ∈ Reaction.Output.targets (hd₂ :: tl₂)
⊢ False

State before:
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
h₁ : ∀ {t : Component.Valued × ID}, Change.target hd₁ = some t → t ∉ Reaction.Output.targets (hd₂ :: tl₂)
a✝ : Component.Valued
b✝ : ID
hm₁ : (a✝, b✝) ∈ Reaction.Output.targets tl₁
hm₂ : (a✝, b✝) ∈ Reaction.Output.targets (hd₂ :: tl₂)
⊢ False
Tactic:
exact Set.disjoint_left.mp ht (Reaction.Output.mem_targets_cons hm₁) hm₂
State after:
no goals

State before:
case refl.trans.trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
s✝ : State α
hd✝ : Change
s₂✝¹ : State α
tl✝ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (hd✝ :: tl✝))
e₁ : s✝ -[hd✝]→ s₂✝¹
e₁' : s₂✝¹ -[tl✝]→ s₁₂
s₂✝ : State α
e₂ : s✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
cases e₁.deterministic e₂
State after:
case refl.trans.trans.refl.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
s✝ : State α
hd✝ : Change
s₂✝ : State α
tl✝ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (hd✝ :: tl✝))
e₁ : s✝ -[hd✝]→ s₂✝
e₁' : s₂✝ -[tl✝]→ s₁₂
e₂ : s✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

State before:
case refl.trans.trans.refl.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
s✝ : State α
hd✝ : Change
s₂✝ : State α
tl✝ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (hd✝ :: tl✝))
e₁ : s✝ -[hd✝]→ s₂✝
e₁' : s₂✝ -[tl✝]→ s₁₂
e₂ : s✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
exact e₁'.deterministic e₂'
State after:
no goals