Theorem: Execution.Step.Skip.comm (ReactorModel/Execution/Theorems/Step/Skip.lean)

State before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂ = s₂₁
Tactic:
ext1
State after:
case rtr
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.rtr = s₂₁.rtr

case tag
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.tag = s₂₁.tag

case progress
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.progress = s₂₁.progress

case events
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.events = s₂₁.events

State before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.rtr = s₂₁.rtr
Tactic:
case rtr => 
  exact e₁₂.preserves_rtr ▸ e₁.preserves_rtr ▸ e₂₁.preserves_rtr ▸ e₂.preserves_rtr
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.tag = s₂₁.tag
Tactic:
case tag => 
  exact e₁₂.preserves_tag ▸ e₁.preserves_tag ▸ e₂₁.preserves_tag ▸ e₂.preserves_tag
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.events = s₂₁.events
Tactic:
case events => 
  exact e₁₂.preserves_events ▸ e₁.preserves_events ▸ e₂₁.preserves_events ▸ e₂.preserves_events
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.progress = s₂₁.progress
Tactic:
case progress  =>
  have h₁ := e₁.progress_eq ▸ e₁₂.progress_eq
  have h₂ := e₂.progress_eq ▸ e₂₁.progress_eq
  rw [hr₁, hr₂] at *
  simp [h₁, h₂]
  apply Set.insert_comm
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.rtr = s₂₁.rtr
Tactic:
exact e₁₂.preserves_rtr ▸ e₁.preserves_rtr ▸ e₂₁.preserves_rtr ▸ e₂.preserves_rtr
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.tag = s₂₁.tag
Tactic:
exact e₁₂.preserves_tag ▸ e₁.preserves_tag ▸ e₂₁.preserves_tag ▸ e₂.preserves_tag
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.events = s₂₁.events
Tactic:
exact e₁₂.preserves_events ▸ e₁.preserves_events ▸ e₂₁.preserves_events ▸ e₂.preserves_events
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
⊢ s₁₂.progress = s₂₁.progress
Tactic:
have h₁ := e₁.progress_eq ▸ e₁₂.progress_eq
State after:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₁) s.progress)
⊢ s₁₂.progress = s₂₁.progress

State before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₁) s.progress)
⊢ s₁₂.progress = s₂₁.progress
Tactic:
have h₂ := e₂.progress_eq ▸ e₂₁.progress_eq
State after:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₁) s.progress)
h₂ : s₂₁.progress = Set.insert (rcn e₂₁) (Set.insert (rcn e₂) s.progress)
⊢ s₁₂.progress = s₂₁.progress

State before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₁ = rcn e₂₁
hr₂ : rcn e₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₁) s.progress)
h₂ : s₂₁.progress = Set.insert (rcn e₂₁) (Set.insert (rcn e₂) s.progress)
⊢ s₁₂.progress = s₂₁.progress
Tactic:
rw [hr₁, hr₂] at *
State after:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₂₁ = rcn e₂₁
hr₂ : rcn e₁₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₂₁) s.progress)
h₂ : s₂₁.progress = Set.insert (rcn e₂₁) (Set.insert (rcn e₁₂) s.progress)
⊢ s₁₂.progress = s₂₁.progress

State before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₂₁ = rcn e₂₁
hr₂ : rcn e₁₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₂₁) s.progress)
h₂ : s₂₁.progress = Set.insert (rcn e₂₁) (Set.insert (rcn e₁₂) s.progress)
⊢ s₁₂.progress = s₂₁.progress
Tactic:
simp [h₁, h₂]
State after:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₂₁ = rcn e₂₁
hr₂ : rcn e₁₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₂₁) s.progress)
h₂ : s₂₁.progress = Set.insert (rcn e₂₁) (Set.insert (rcn e₁₂) s.progress)
⊢ Set.insert (rcn e₁₂) (Set.insert (rcn e₂₁) s.progress) = Set.insert (rcn e₂₁) (Set.insert (rcn e₁₂) s.progress)

State before:
α : Type
inst✝ : Hierarchical α
s₁ s s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₛ s₁
e₁₂ : s₁ ↓ₛ s₁₂
e₂ : s ↓ₛ s₂
e₂₁ : s₂ ↓ₛ s₂₁
hr₁ : rcn e₂₁ = rcn e₂₁
hr₂ : rcn e₁₂ = rcn e₁₂
h₁ : s₁₂.progress = Set.insert (rcn e₁₂) (Set.insert (rcn e₂₁) s.progress)
h₂ : s₂₁.progress = Set.insert (rcn e₂₁) (Set.insert (rcn e₁₂) s.progress)
⊢ Set.insert (rcn e₁₂) (Set.insert (rcn e₂₁) s.progress) = Set.insert (rcn e₂₁) (Set.insert (rcn e₁₂) s.progress)
Tactic:
apply Set.insert_comm
State after:
no goals