Theorem: Execution.Instantaneous.Step.prepend_indep' (ReactorModel/Execution/Theorems/Grouped/Instantaneous.lean)

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
h : rcn e₁ ≮[s₁.rtr] rcn e₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁ ∧ s₃' = s₃
Tactic:
replace h : _ ≮[_]≯ _ := { not_eq := e₁.seq_rcn_ne e₂, left := h, right := e₁.seq_wellordered e₂ }
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
h : rcn e₁ ≮[s₁.rtr]≯ rcn e₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁ ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
h : rcn e₁ ≮[s₁.rtr]≯ rcn e₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁ ∧ s₃' = s₃
Tactic:
cases e₁ <;> cases e₂
State after:
case skip.skip
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
s✝¹ : s₁ ↓ₛ s₂
s✝ : s₂ ↓ₛ s₃
h : rcn (skip s✝¹) ≮[s₁.rtr]≯ rcn (skip s✝)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip s✝) ∧ rcn e₂' = rcn (skip s✝¹) ∧ s₃' = s₃

case skip.exec
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
s✝ : s₁ ↓ₛ s₂
e✝ : s₂ ↓ₑ s₃
h : rcn (skip s✝) ≮[s₁.rtr]≯ rcn (exec e✝)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e✝) ∧ rcn e₂' = rcn (skip s✝) ∧ s₃' = s₃

case exec.skip
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e✝ : s₁ ↓ₑ s₂
s✝ : s₂ ↓ₛ s₃
h : rcn (exec e✝) ≮[s₁.rtr]≯ rcn (skip s✝)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip s✝) ∧ rcn e₂' = rcn (exec e✝) ∧ s₃' = s₃

case exec.exec
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e✝¹ : s₁ ↓ₑ s₂
e✝ : s₂ ↓ₑ s₃
h : rcn (exec e✝¹) ≮[s₁.rtr]≯ rcn (exec e✝)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e✝) ∧ rcn e₂' = rcn (exec e✝¹) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
case skip.skip e₁ e₂ =>
  have ha₁ := e₁.indep_allows_iff h.symm |>.mpr e₂.allows_rcn
  have ht₁ := e₁.triggers_iff.not.mpr e₂.not_triggers_rcn
  let s₂' := s₁.record e₂.rcn
  let f₁ : s₁ ↓ₛ s₂' := ⟨ha₁, ht₁⟩
  have ha₂ := f₁.indep_allows_iff h |>.mp e₁.allows_rcn
  have ht₂ := f₁.triggers_iff.not.mp e₁.not_triggers_rcn
  let s₃' := s₂'.record e₁.rcn
  let f₂ : s₂' ↓ₛ s₃' := ⟨ha₂, ht₂⟩
  refine ⟨_, _, .skip f₁, .skip f₂, rfl, rfl, ?_⟩
  exact Step.Skip.comm e₁ e₂ f₁ f₂ rfl rfl |>.symm
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
case skip.exec e₁ e₂ =>
  have ⟨z₂, a₁⟩ := Step.Apply.RTC.construct s₁ (s₁.output e₂.rcn)
  have ha₁ := e₁.indep_allows_iff h.symm |>.mpr e₂.allows_rcn
  have ht₁ := e₁.triggers_iff.mpr e₂.triggers_rcn
  let s₂' := z₂.record e₂.rcn
  let f₁ : s₁ ↓ₑ s₂' := ⟨ha₁, ht₁, a₁⟩
  have ha₂ := f₁.indep_allows_iff h |>.mp e₁.allows_rcn
  have ht₂ := f₁.indep_triggers_iff h |>.not.mp e₁.not_triggers_rcn
  let s₃' := s₂'.record e₁.rcn
  let f₂ : s₂' ↓ₛ s₃' := ⟨ha₂, ht₂⟩
  refine ⟨_, _, .exec f₁, .skip f₂, rfl, rfl, ?_⟩
  simp [e₂.dst_eq, f₂.dst_eq]
  rw [State.record_comm]
  congr!
  have a₂ := e₂.apply
  simp [e₁.dst_eq] at a₂
  exact a₁.comm_record a₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
case exec.skip e₁ e₂ =>
  have ha₁ := e₁.indep_allows_iff h.symm |>.mpr e₂.allows_rcn
  have ht₁ := e₁.indep_triggers_iff h.symm |>.not.mpr e₂.not_triggers_rcn
  let s₂' := s₁.record e₂.rcn
  let f₁ : s₁ ↓ₛ s₂' := ⟨ha₁, ht₁⟩
  have ⟨z₃, a₂⟩ := Step.Apply.RTC.construct s₂' (s₂'.output e₁.rcn)
  have ha₂ := f₁.indep_allows_iff h |>.mp e₁.allows_rcn
  have ht₂ := f₁.triggers_iff.mp e₁.triggers_rcn
  let s₃' := z₃.record e₁.rcn
  let f₂ : s₂' ↓ₑ s₃' := ⟨ha₂, ht₂, a₂⟩
  refine ⟨_, _, .skip f₁, .exec f₂, rfl, rfl, ?_⟩
  simp [e₂.dst_eq, e₁.dst_eq]
  rw [State.record_comm]
  congr!
  have a₁ := e₁.apply
  rw [s₁.record_preserves_output] at a₂
  exact a₁.comm_record a₂ |>.symm
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
case exec.exec e₁ e₂ =>
  have ⟨z₂, a₁⟩ := Step.Apply.RTC.construct s₁ (s₁.output e₂.rcn)
  have ha₁ := e₁.indep_allows_iff h.symm |>.mpr e₂.allows_rcn
  have ht₁ := e₁.indep_triggers_iff h.symm |>.mpr e₂.triggers_rcn
  let s₂' := z₂.record e₂.rcn
  let f₁ : s₁ ↓ₑ s₂' := ⟨ha₁, ht₁, a₁⟩
  have ⟨z₃, a₂⟩ := Step.Apply.RTC.construct s₂' (s₂'.output e₁.rcn)
  have ha₂ := f₁.indep_allows_iff h |>.mp e₁.allows_rcn
  have ht₂ := f₁.indep_triggers_iff h |>.mp e₁.triggers_rcn
  let s₃' := z₃.record e₁.rcn
  let f₂ : s₂' ↓ₑ s₃' := ⟨ha₂, ht₂, a₂⟩
  refine ⟨_, _, .exec f₁, .exec f₂, rfl, rfl, ?_⟩
  exact Step.Exec.indep_comm e₁ e₂ f₁ f₂ rfl rfl h |>.symm
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ha₁ := e₁.indep_allows_iff h.symm |>.mpr e₂.allows_rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ht₁ := e₁.triggers_iff.not.mpr e₂.not_triggers_rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
let s₂' := s₁.record e₂.rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
let f₁ : s₁ ↓ₛ s₂' := ⟨ha₁, ht₁⟩
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ha₂ := f₁.indep_allows_iff h |>.mp e₁.allows_rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ht₂ := f₁.triggers_iff.not.mp e₁.not_triggers_rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
let s₃' := s₂'.record e₁.rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
let f₂ : s₂' ↓ₛ s₃' := ⟨ha₂, ht₂⟩
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
refine ⟨_, _, .skip f₁, .skip f₂, rfl, rfl, ?_⟩
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (Step.Skip.rcn e₂)
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (Step.Skip.rcn e₁)
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ s₃' = s₃
Tactic:
exact Step.Skip.comm e₁ e₂ f₁ f₂ rfl rfl |>.symm
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ⟨z₂, a₁⟩ := Step.Apply.RTC.construct s₁ (s₁.output e₂.rcn)
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ha₁ := e₁.indep_allows_iff h.symm |>.mpr e₂.allows_rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ht₁ := e₁.triggers_iff.mpr e₂.triggers_rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
let s₂' := z₂.record e₂.rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
let f₁ : s₁ ↓ₑ s₂' := ⟨ha₁, ht₁, a₁⟩
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ha₂ := f₁.indep_allows_iff h |>.mp e₁.allows_rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
have ht₂ := f₁.indep_triggers_iff h |>.not.mp e₁.not_triggers_rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
let s₃' := s₂'.record e₁.rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
let f₂ : s₂' ↓ₛ s₃' := ⟨ha₂, ht₂⟩
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (skip e₁) ∧ s₃' = s₃
Tactic:
refine ⟨_, _, .exec f₁, .skip f₂, rfl, rfl, ?_⟩
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ s₃' = s₃
Tactic:
simp [e₂.dst_eq, f₂.dst_eq]
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ record s₂' (Step.Skip.rcn f₂) = record (Step.Exec.applied e₂) (Step.Exec.rcn e₂)

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ record s₂' (Step.Skip.rcn f₂) = record (Step.Exec.applied e₂) (Step.Exec.rcn e₂)
Tactic:
rw [State.record_comm]
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ record (record z₂ (Step.Skip.rcn f₂)) (Step.Exec.rcn e₂) = record (Step.Exec.applied e₂) (Step.Exec.rcn e₂)

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ record (record z₂ (Step.Skip.rcn f₂)) (Step.Exec.rcn e₂) = record (Step.Exec.applied e₂) (Step.Exec.rcn e₂)
Tactic:
congr!
State after:
case h.e'_2
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ record z₂ (Step.Skip.rcn f₂) = Step.Exec.applied e₂

State before:
case h.e'_2
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
⊢ record z₂ (Step.Skip.rcn f₂) = Step.Exec.applied e₂
Tactic:
have a₂ := e₂.apply
State after:
case h.e'_2
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
a₂ : s₂ -[output s₂ (Step.Exec.rcn e₂)]→ (Step.Exec.applied e₂)
⊢ record z₂ (Step.Skip.rcn f₂) = Step.Exec.applied e₂

State before:
case h.e'_2
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
a₂ : s₂ -[output s₂ (Step.Exec.rcn e₂)]→ (Step.Exec.applied e₂)
⊢ record z₂ (Step.Skip.rcn f₂) = Step.Exec.applied e₂
Tactic:
simp [e₁.dst_eq] at a₂
State after:
case h.e'_2
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
a₂ : (record s₁ (Step.Skip.rcn e₁)) -[output (record s₁ (Step.Skip.rcn e₁)) (Step.Exec.rcn e₂)]→ (Step.Exec.applied e₂)
⊢ record z₂ (Step.Skip.rcn f₂) = Step.Exec.applied e₂

State before:
case h.e'_2
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₛ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (skip e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (Step.Exec.rcn e₂)
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
ha₂ : Allows s₂' (rcn (skip e₁))
ht₂ : ¬Triggers s₂' (rcn (skip e₁))
s₃' : State α := record s₂' (Step.Skip.rcn e₁)
f₂ : s₂' ↓ₛ s₃' := Step.Skip.mk ha₂ ht₂
a₂ : (record s₁ (Step.Skip.rcn e₁)) -[output (record s₁ (Step.Skip.rcn e₁)) (Step.Exec.rcn e₂)]→ (Step.Exec.applied e₂)
⊢ record z₂ (Step.Skip.rcn f₂) = Step.Exec.applied e₂
Tactic:
exact a₁.comm_record a₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
have ha₁ := e₁.indep_allows_iff h.symm |>.mpr e₂.allows_rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
have ht₁ := e₁.indep_triggers_iff h.symm |>.not.mpr e₂.not_triggers_rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
let s₂' := s₁.record e₂.rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
let f₁ : s₁ ↓ₛ s₂' := ⟨ha₁, ht₁⟩
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
have ⟨z₃, a₂⟩ := Step.Apply.RTC.construct s₂' (s₂'.output e₁.rcn)
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
have ha₂ := f₁.indep_allows_iff h |>.mp e₁.allows_rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
have ht₂ := f₁.triggers_iff.mp e₁.triggers_rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
let s₃' := z₃.record e₁.rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
let f₂ : s₂' ↓ₑ s₃' := ⟨ha₂, ht₂, a₂⟩
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (skip e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
refine ⟨_, _, .skip f₁, .exec f₂, rfl, rfl, ?_⟩
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂
⊢ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂
⊢ s₃' = s₃
Tactic:
simp [e₂.dst_eq, e₁.dst_eq]
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂
⊢ s₃' = record (record (Step.Exec.applied e₁) (Step.Exec.rcn e₁)) (Step.Skip.rcn e₂)

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂
⊢ s₃' = record (record (Step.Exec.applied e₁) (Step.Exec.rcn e₁)) (Step.Skip.rcn e₂)
Tactic:
rw [State.record_comm]
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂
⊢ s₃' = record (record (Step.Exec.applied e₁) (Step.Skip.rcn e₂)) (Step.Exec.rcn e₁)

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂
⊢ s₃' = record (record (Step.Exec.applied e₁) (Step.Skip.rcn e₂)) (Step.Exec.rcn e₁)
Tactic:
congr!
State after:
case h.e'_2
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂
⊢ z₃ = record (Step.Exec.applied e₁) (Step.Skip.rcn e₂)

State before:
case h.e'_2
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂
⊢ z₃ = record (Step.Exec.applied e₁) (Step.Skip.rcn e₂)
Tactic:
have a₁ := e₁.apply
State after:
case h.e'_2
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₁)]→ (Step.Exec.applied e₁)
⊢ z₃ = record (Step.Exec.applied e₁) (Step.Skip.rcn e₂)

State before:
case h.e'_2
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₁)]→ (Step.Exec.applied e₁)
⊢ z₃ = record (Step.Exec.applied e₁) (Step.Skip.rcn e₂)
Tactic:
rw [s₁.record_preserves_output] at a₂
State after:
case h.e'_2
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂✝ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
a₂ : s₂' -[output s₁ (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂✝
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₁)]→ (Step.Exec.applied e₁)
⊢ z₃ = record (Step.Exec.applied e₁) (Step.Skip.rcn e₂)

State before:
case h.e'_2
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₛ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (skip e₂)
ha₁ : Allows s₁ (rcn (skip e₂))
ht₁ : ¬Triggers s₁ (rcn (skip e₂))
s₂' : State α := record s₁ (Step.Skip.rcn e₂)
f₁ : s₁ ↓ₛ s₂' := Step.Skip.mk ha₁ ht₁
z₃ : State α
a₂✝ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
a₂ : s₂' -[output s₁ (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (Step.Exec.rcn e₁)
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂✝
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₁)]→ (Step.Exec.applied e₁)
⊢ z₃ = record (Step.Exec.applied e₁) (Step.Skip.rcn e₂)
Tactic:
exact a₁.comm_record a₂ |>.symm
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
have ⟨z₂, a₁⟩ := Step.Apply.RTC.construct s₁ (s₁.output e₂.rcn)
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
have ha₁ := e₁.indep_allows_iff h.symm |>.mpr e₂.allows_rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
have ht₁ := e₁.indep_triggers_iff h.symm |>.mpr e₂.triggers_rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
let s₂' := z₂.record e₂.rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
let f₁ : s₁ ↓ₑ s₂' := ⟨ha₁, ht₁, a₁⟩
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
have ⟨z₃, a₂⟩ := Step.Apply.RTC.construct s₂' (s₂'.output e₁.rcn)
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
have ha₂ := f₁.indep_allows_iff h |>.mp e₁.allows_rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
have ht₂ := f₁.indep_triggers_iff h |>.mp e₁.triggers_rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (rcn (exec e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (rcn (exec e₁))
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
let s₃' := z₃.record e₁.rcn
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (rcn (exec e₁))
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (rcn (exec e₁))
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
let f₂ : s₂' ↓ₑ s₃' := ⟨ha₂, ht₂, a₂⟩
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (rcn (exec e₁))
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (rcn (exec e₁))
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂
⊢ ∃ s₂' s₃' e₁' e₂', rcn e₁' = rcn (exec e₂) ∧ rcn e₂' = rcn (exec e₁) ∧ s₃' = s₃
Tactic:
refine ⟨_, _, .exec f₁, .exec f₂, rfl, rfl, ?_⟩
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (rcn (exec e₁))
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂
⊢ s₃' = s₃

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ₑ s₂
e₂ : s₂ ↓ₑ s₃
h : rcn (exec e₁) ≮[s₁.rtr]≯ rcn (exec e₂)
z₂ : State α
a₁ : s₁ -[output s₁ (Step.Exec.rcn e₂)]→ z₂
ha₁ : Allows s₁ (rcn (exec e₂))
ht₁ : Triggers s₁ (rcn (exec e₂))
s₂' : State α := record z₂ (Step.Exec.rcn e₂)
f₁ : s₁ ↓ₑ s₂' := Step.Exec.mk ha₁ ht₁ a₁
z₃ : State α
a₂ : s₂' -[output s₂' (Step.Exec.rcn e₁)]→ z₃
ha₂ : Allows s₂' (rcn (exec e₁))
ht₂ : Triggers s₂' (rcn (exec e₁))
s₃' : State α := record z₃ (Step.Exec.rcn e₁)
f₂ : s₂' ↓ₑ s₃' := Step.Exec.mk ha₂ ht₂ a₂
⊢ s₃' = s₃
Tactic:
exact Step.Exec.indep_comm e₁ e₂ f₁ f₂ rfl rfl h |>.symm
State after:
no goals