Theorem: Execution.Step.Exec.indep_comm (ReactorModel/Execution/Theorems/Step/Exec.lean)

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₑ s₁
e₁₂ : s₁ ↓ₑ s₁₂
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn e₁ = Execution.Step.Exec.rcn e₂₁
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
hi : Execution.Step.Exec.rcn e₁ ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
⊢ s₁₂ = s₂₁
Tactic:
have ho₁ := e₁.indep_output_eq hi
State after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₑ s₁
e₁₂ : s₁ ↓ₑ s₁₂
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn e₁ = Execution.Step.Exec.rcn e₂₁
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
hi : Execution.Step.Exec.rcn e₁ ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output s₁ (Execution.Step.Exec.rcn e₂)
⊢ s₁₂ = s₂₁

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₑ s₁
e₁₂ : s₁ ↓ₑ s₁₂
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn e₁ = Execution.Step.Exec.rcn e₂₁
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
hi : Execution.Step.Exec.rcn e₁ ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output s₁ (Execution.Step.Exec.rcn e₂)
⊢ s₁₂ = s₂₁
Tactic:
have ho₂ := e₂.indep_output_eq hi.symm
State after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₑ s₁
e₁₂ : s₁ ↓ₑ s₁₂
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn e₁ = Execution.Step.Exec.rcn e₂₁
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
hi : Execution.Step.Exec.rcn e₁ ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output s₁ (Execution.Step.Exec.rcn e₂)
ho₂ : output s (Execution.Step.Exec.rcn e₁) = output s₂ (Execution.Step.Exec.rcn e₁)
⊢ s₁₂ = s₂₁

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₑ s₁
e₁₂ : s₁ ↓ₑ s₁₂
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn e₁ = Execution.Step.Exec.rcn e₂₁
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
hi : Execution.Step.Exec.rcn e₁ ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output s₁ (Execution.Step.Exec.rcn e₂)
ho₂ : output s (Execution.Step.Exec.rcn e₁) = output s₂ (Execution.Step.Exec.rcn e₁)
⊢ s₁₂ = s₂₁
Tactic:
cases e₁
State after:
case mk
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
rcn✝ : ID
s₂✝ : State α
a✝² : Allows s rcn✝
a✝¹ : Triggers s rcn✝
a✝ : s -[output s rcn✝]→ s₂✝
e₁₂ : (record s₂✝ rcn✝) ↓ₑ s₁₂
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output (record s₂✝ rcn✝) (Execution.Step.Exec.rcn e₂)
hr₁ : Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝) = Execution.Step.Exec.rcn e₂₁
hi : Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝) ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₂ : output s (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)) = output s₂ (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝))
⊢ s₁₂ = s₂₁

State before:
case mk
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
rcn✝ : ID
s₂✝ : State α
a✝² : Allows s rcn✝
a✝¹ : Triggers s rcn✝
a✝ : s -[output s rcn✝]→ s₂✝
e₁₂ : (record s₂✝ rcn✝) ↓ₑ s₁₂
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output (record s₂✝ rcn✝) (Execution.Step.Exec.rcn e₂)
hr₁ : Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝) = Execution.Step.Exec.rcn e₂₁
hi : Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝) ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₂ : output s (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)) = output s₂ (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝))
⊢ s₁₂ = s₂₁
Tactic:
cases e₁₂
State after:
case mk.mk
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
s₂ s₂₁ : State α
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
rcn✝¹ : ID
s₂✝¹ : State α
a✝⁵ : Allows s rcn✝¹
a✝⁴ : Triggers s rcn✝¹
a✝³ : s -[output s rcn✝¹]→ s₂✝¹
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output (record s₂✝¹ rcn✝¹) (Execution.Step.Exec.rcn e₂)
hr₁ : Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³) = Execution.Step.Exec.rcn e₂₁
hi : Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³) ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₂ : output s (Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³)) = output s₂ (Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³))
rcn✝ : ID
s₂✝ : State α
a✝² : Allows (record s₂✝¹ rcn✝¹) rcn✝
a✝¹ : Triggers (record s₂✝¹ rcn✝¹) rcn✝
a✝ : (record s₂✝¹ rcn✝¹) -[output (record s₂✝¹ rcn✝¹) rcn✝]→ s₂✝
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)
⊢ record s₂✝ rcn✝ = s₂₁

State before:
case mk.mk
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
s₂ s₂₁ : State α
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
rcn✝¹ : ID
s₂✝¹ : State α
a✝⁵ : Allows s rcn✝¹
a✝⁴ : Triggers s rcn✝¹
a✝³ : s -[output s rcn✝¹]→ s₂✝¹
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output (record s₂✝¹ rcn✝¹) (Execution.Step.Exec.rcn e₂)
hr₁ : Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³) = Execution.Step.Exec.rcn e₂₁
hi : Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³) ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₂ : output s (Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³)) = output s₂ (Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³))
rcn✝ : ID
s₂✝ : State α
a✝² : Allows (record s₂✝¹ rcn✝¹) rcn✝
a✝¹ : Triggers (record s₂✝¹ rcn✝¹) rcn✝
a✝ : (record s₂✝¹ rcn✝¹) -[output (record s₂✝¹ rcn✝¹) rcn✝]→ s₂✝
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)
⊢ record s₂✝ rcn✝ = s₂₁
Tactic:
cases e₂
State after:
case mk.mk.mk
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
s₂₁ : State α
rcn✝² : ID
s₂✝² : State α
a✝⁸ : Allows s rcn✝²
a✝⁷ : Triggers s rcn✝²
a✝⁶ : s -[output s rcn✝²]→ s₂✝²
rcn✝¹ : ID
s₂✝¹ : State α
a✝⁵ : Allows (record s₂✝² rcn✝²) rcn✝¹
a✝⁴ : Triggers (record s₂✝² rcn✝²) rcn✝¹
a✝³ : (record s₂✝² rcn✝²) -[output (record s₂✝² rcn✝²) rcn✝¹]→ s₂✝¹
rcn✝ : ID
s₂✝ : State α
a✝² : Allows s rcn✝
a✝¹ : Triggers s rcn✝
a✝ : s -[output s rcn✝]→ s₂✝
e₂₁ : (record s₂✝ rcn✝) ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶) = Execution.Step.Exec.rcn e₂₁
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶)) =
    output (record s₂✝ rcn✝) (Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)) =
    output (record s₂✝² rcn✝²) (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝))
hi : Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)
hr₂ : Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝) = Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³)
⊢ record s₂✝¹ rcn✝¹ = s₂₁

State before:
case mk.mk.mk
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
s₂₁ : State α
rcn✝² : ID
s₂✝² : State α
a✝⁸ : Allows s rcn✝²
a✝⁷ : Triggers s rcn✝²
a✝⁶ : s -[output s rcn✝²]→ s₂✝²
rcn✝¹ : ID
s₂✝¹ : State α
a✝⁵ : Allows (record s₂✝² rcn✝²) rcn✝¹
a✝⁴ : Triggers (record s₂✝² rcn✝²) rcn✝¹
a✝³ : (record s₂✝² rcn✝²) -[output (record s₂✝² rcn✝²) rcn✝¹]→ s₂✝¹
rcn✝ : ID
s₂✝ : State α
a✝² : Allows s rcn✝
a✝¹ : Triggers s rcn✝
a✝ : s -[output s rcn✝]→ s₂✝
e₂₁ : (record s₂✝ rcn✝) ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶) = Execution.Step.Exec.rcn e₂₁
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶)) =
    output (record s₂✝ rcn✝) (Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)) =
    output (record s₂✝² rcn✝²) (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝))
hi : Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)
hr₂ : Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝) = Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³)
⊢ record s₂✝¹ rcn✝¹ = s₂₁
Tactic:
cases e₂₁
State after:
case mk.mk.mk.mk
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn✝³ : ID
s₂✝³ : State α
a✝¹¹ : Allows s rcn✝³
a✝¹⁰ : Triggers s rcn✝³
a✝⁹ : s -[output s rcn✝³]→ s₂✝³
rcn✝² : ID
s₂✝² : State α
a✝⁸ : Allows (record s₂✝³ rcn✝³) rcn✝²
a✝⁷ : Triggers (record s₂✝³ rcn✝³) rcn✝²
a✝⁶ : (record s₂✝³ rcn✝³) -[output (record s₂✝³ rcn✝³) rcn✝²]→ s₂✝²
rcn✝¹ : ID
s₂✝¹ : State α
a✝⁵ : Allows s rcn✝¹
a✝⁴ : Triggers s rcn✝¹
a✝³ : s -[output s rcn✝¹]→ s₂✝¹
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝¹¹ a✝¹⁰ a✝⁹)) =
    output (record s₂✝¹ rcn✝¹) (Execution.Step.Exec.rcn (mk a✝¹¹ a✝¹⁰ a✝⁹))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³)) =
    output (record s₂✝³ rcn✝³) (Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³))
hi : Execution.Step.Exec.rcn (mk a✝¹¹ a✝¹⁰ a✝⁹) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³)
hr₂ : Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a✝³) = Execution.Step.Exec.rcn (mk a✝⁸ a✝⁷ a✝⁶)
rcn✝ : ID
s₂✝ : State α
a✝² : Allows (record s₂✝¹ rcn✝¹) rcn✝
a✝¹ : Triggers (record s₂✝¹ rcn✝¹) rcn✝
a✝ : (record s₂✝¹ rcn✝¹) -[output (record s₂✝¹ rcn✝¹) rcn✝]→ s₂✝
hr₁ : Execution.Step.Exec.rcn (mk a✝¹¹ a✝¹⁰ a✝⁹) = Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)
⊢ record s₂✝² rcn✝² = record s₂✝ rcn✝

State before:
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
rcn✝¹ : ID
s₂ : State α
a✝³ : Allows s rcn✝¹
a✝² : Triggers s rcn✝¹
a₂ : s -[output s rcn✝¹]→ s₂
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁)) =
    output (record s₂ rcn✝¹) (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)) = output (record s₁ rcn₁) (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂))
hi : Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)
hr₂ : Execution.Step.Exec.rcn (mk a✝³ a✝² a₂) = Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a₁₂)
rcn✝ : ID
s₂₁ : State α
a✝¹ : Allows (record s₂ rcn✝¹) rcn✝
a✝ : Triggers (record s₂ rcn✝¹) rcn✝
a₂₁ : (record s₂ rcn✝¹) -[output (record s₂ rcn✝¹) rcn✝]→ s₂₁
hr₁ : Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁) = Execution.Step.Exec.rcn (mk a✝¹ a✝ a₂₁)
⊢ record s₁₂ rcn₂ = record s₂₁ rcn✝
Tactic:
case _ rcn₁ s₁ _ _ a₁ rcn₂ s₁₂ _ _ a₁₂ _ s₂ _ _ a₂ _ s₂₁ _ _ a₂₁ => 
  cases hr₁; cases hr₂; simp [Exec.rcn] at *
  have ⟨z₁₂, f₁₂⟩ := Apply.RTC.construct s₁ (s.output rcn₂)
  have ⟨z₂₁, f₂₁⟩ := Apply.RTC.construct s₂ (s.output rcn₁)
  rw [←ho₁] at a₁₂; rw [←ho₂] at a₂₁
  cases f₁₂.comm_record a₁₂; cases f₂₁.comm_record a₂₁
  rw [record_comm]; congr
  exact Apply.RTC.disjoint_targets_comm (s.indep_output_disjoint_targets hi) a₁ f₁₂ a₂ f₂₁
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
rcn✝¹ : ID
s₂ : State α
a✝³ : Allows s rcn✝¹
a✝² : Triggers s rcn✝¹
a₂ : s -[output s rcn✝¹]→ s₂
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁)) =
    output (record s₂ rcn✝¹) (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)) = output (record s₁ rcn₁) (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂))
hi : Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)
hr₂ : Execution.Step.Exec.rcn (mk a✝³ a✝² a₂) = Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a₁₂)
rcn✝ : ID
s₂₁ : State α
a✝¹ : Allows (record s₂ rcn✝¹) rcn✝
a✝ : Triggers (record s₂ rcn✝¹) rcn✝
a₂₁ : (record s₂ rcn✝¹) -[output (record s₂ rcn✝¹) rcn✝]→ s₂₁
hr₁ : Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁) = Execution.Step.Exec.rcn (mk a✝¹ a✝ a₂₁)
⊢ record s₁₂ rcn₂ = record s₂₁ rcn✝
Tactic:
cases hr₁
State after:
case refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
rcn✝ : ID
s₂ : State α
a✝³ : Allows s rcn✝
a✝² : Triggers s rcn✝
a₂ : s -[output s rcn✝]→ s₂
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁)) = output (record s₂ rcn✝) (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)) = output (record s₁ rcn₁) (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂))
hi : Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)
hr₂ : Execution.Step.Exec.rcn (mk a✝³ a✝² a₂) = Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a₁₂)
s₂₁ : State α
a✝¹ : Allows (record s₂ rcn✝) rcn₁
a✝ : Triggers (record s₂ rcn✝) rcn₁
a₂₁ : (record s₂ rcn✝) -[output (record s₂ rcn✝) rcn₁]→ s₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁

State before:
case refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
rcn✝ : ID
s₂ : State α
a✝³ : Allows s rcn✝
a✝² : Triggers s rcn✝
a₂ : s -[output s rcn✝]→ s₂
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁)) = output (record s₂ rcn✝) (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)) = output (record s₁ rcn₁) (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂))
hi : Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)
hr₂ : Execution.Step.Exec.rcn (mk a✝³ a✝² a₂) = Execution.Step.Exec.rcn (mk a✝⁵ a✝⁴ a₁₂)
s₂₁ : State α
a✝¹ : Allows (record s₂ rcn✝) rcn₁
a✝ : Triggers (record s₂ rcn✝) rcn₁
a₂₁ : (record s₂ rcn✝) -[output (record s₂ rcn✝) rcn₁]→ s₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Tactic:
cases hr₂
State after:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁)) = output (record s₂ rcn₂) (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)) = output (record s₁ rcn₁) (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂))
hi : Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁

State before:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ :
  output s (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁)) = output (record s₂ rcn₂) (Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁))
ho₁ :
  output s (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)) = output (record s₁ rcn₁) (Execution.Step.Exec.rcn (mk a✝³ a✝² a₂))
hi : Execution.Step.Exec.rcn (mk a✝⁷ a✝⁶ a₁) ≮[s.rtr]≯ Execution.Step.Exec.rcn (mk a✝³ a✝² a₂)
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Tactic:
simp [Exec.rcn] at *
State after:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁

State before:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Tactic:
have ⟨z₁₂, f₁₂⟩ := Apply.RTC.construct s₁ (s.output rcn₂)
State after:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁

State before:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Tactic:
have ⟨z₂₁, f₂₁⟩ := Apply.RTC.construct s₂ (s.output rcn₁)
State after:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁

State before:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output (record s₁ rcn₁) rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Tactic:
rw [←ho₁] at a₁₂
State after:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁

State before:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Tactic:
rw [←ho₂] at a₂₁
State after:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁

State before:
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
s₁₂ : State α
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ s₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
Tactic:
cases f₁₂.comm_record a₁₂
State after:
case refl.refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
⊢ record (record z₁₂ rcn₁) rcn₂ = record s₂₁ rcn₁

State before:
case refl.refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ s₂₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
⊢ record (record z₁₂ rcn₁) rcn₂ = record s₂₁ rcn₁
Tactic:
cases f₂₁.comm_record a₂₁
State after:
case refl.refl.refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ (record z₂₁ rcn₂)
⊢ record (record z₁₂ rcn₁) rcn₂ = record (record z₂₁ rcn₂) rcn₁

State before:
case refl.refl.refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ (record z₂₁ rcn₂)
⊢ record (record z₁₂ rcn₁) rcn₂ = record (record z₂₁ rcn₂) rcn₁
Tactic:
rw [record_comm]
State after:
case refl.refl.refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ (record z₂₁ rcn₂)
⊢ record (record z₁₂ rcn₂) rcn₁ = record (record z₂₁ rcn₂) rcn₁

State before:
case refl.refl.refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ (record z₂₁ rcn₂)
⊢ record (record z₁₂ rcn₂) rcn₁ = record (record z₂₁ rcn₂) rcn₁
Tactic:
congr
State after:
case refl.refl.refl.refl.e_s.e_s
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ (record z₂₁ rcn₂)
⊢ z₁₂ = z₂₁

State before:
case refl.refl.refl.refl.e_s.e_s
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ (record z₂₁ rcn₂)
⊢ z₁₂ = z₂₁
Tactic:
exact Apply.RTC.disjoint_targets_comm (s.indep_output_disjoint_targets hi) a₁ f₁₂ a₂ f₂₁
State after:
no goals