internlm/Lean-Github huggingface dataset:
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof 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
Proof 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₂)
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof 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₂
Proof 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₂)
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof 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
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof 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)
Proof 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₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof 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
Proof 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₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof 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
Proof 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₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof 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
Proof 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₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof 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₁⟩
Proof 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₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof 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)
Proof 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₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof 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
Proof 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₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof 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
Proof 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₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof 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
Proof 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₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof 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₂⟩
Proof 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₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof 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, ?_⟩
Proof 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₃
Theorem: Execution.Instantaneous.Step.prepend_indep'
Proof 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
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.prepend_indep
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
h : rcn e₁ ≮[s₁.rtr] rcn e₂
⊢ ∃ s₂' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁
Tactic:
have ⟨s₂', _, e₁', e₂', h₁, h₂, h⟩ := prepend_indep' e₁ e₂ h
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
h✝ : rcn e₁ ≮[s₁.rtr] rcn e₂
s₂' w✝ : State α
e₁' : s₁ ↓ᵢ s₂'
e₂' : s₂' ↓ᵢ w✝
h₁ : rcn e₁' = rcn e₂
h₂ : rcn e₂' = rcn e₁
h : w✝ = s₃
⊢ ∃ s₂' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁
Theorem: Execution.Instantaneous.Step.prepend_indep
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
h✝ : rcn e₁ ≮[s₁.rtr] rcn e₂
s₂' w✝ : State α
e₁' : s₁ ↓ᵢ s₂'
e₂' : s₂' ↓ᵢ w✝
h₁ : rcn e₁' = rcn e₂
h₂ : rcn e₂' = rcn e₁
h : w✝ = s₃
⊢ ∃ s₂' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁
Tactic:
subst h
Proof state after:
α : Type
inst✝ : Proper α
s₁ s₂ : State α
e₁ : s₁ ↓ᵢ s₂
s₂' w✝ : State α
e₁' : s₁ ↓ᵢ s₂'
e₂' : s₂' ↓ᵢ w✝
h₂ : rcn e₂' = rcn e₁
e₂ : s₂ ↓ᵢ w✝
h : rcn e₁ ≮[s₁.rtr] rcn e₂
h₁ : rcn e₁' = rcn e₂
⊢ ∃ s₂' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁
Theorem: Execution.Instantaneous.Step.prepend_indep
Proof state before:
α : Type
inst✝ : Proper α
s₁ s₂ : State α
e₁ : s₁ ↓ᵢ s₂
s₂' w✝ : State α
e₁' : s₁ ↓ᵢ s₂'
e₂' : s₂' ↓ᵢ w✝
h₂ : rcn e₂' = rcn e₁
e₂ : s₂ ↓ᵢ w✝
h : rcn e₁ ≮[s₁.rtr] rcn e₂
h₁ : rcn e₁' = rcn e₂
⊢ ∃ s₂' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁
Tactic:
exists s₂', e₁', e₂'
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.preserves_nontrivial
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
n : State.Nontrivial s₁
e : s₁ ↓ᵢ+ s₂
⊢ State.Nontrivial s₂
Tactic:
induction e
Proof state after:
case single
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
n : State.Nontrivial s₁✝
⊢ State.Nontrivial s₂✝

case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → State.Nontrivial s₃✝
n : State.Nontrivial s₁✝
⊢ State.Nontrivial s₃✝
Theorem: Execution.Instantaneous.Step.TC.preserves_nontrivial
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
n : State.Nontrivial s₁✝
⊢ State.Nontrivial s₂✝
Tactic:
case single e     => exact e.preserves_nontrivial n
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.preserves_nontrivial
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : State.Nontrivial s₂✝ → State.Nontrivial s₃✝
n : State.Nontrivial s₁✝
⊢ State.Nontrivial s₃✝
Tactic:
case trans e _ hi => exact hi $ e.preserves_nontrivial n
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.preserves_nontrivial
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
n : State.Nontrivial s₁✝
⊢ State.Nontrivial s₂✝
Tactic:
exact e.preserves_nontrivial n
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.preserves_nontrivial
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : State.Nontrivial s₂✝ → State.Nontrivial s₃✝
n : State.Nontrivial s₁✝
⊢ State.Nontrivial s₃✝
Tactic:
exact hi $ e.preserves_nontrivial n
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
h : rcn ∈ rcns e
⊢ rcn ≮[s₁.rtr] rcn
Tactic:
induction e <;> simp [rcns] at h <;> try cases ‹_ ∨ _›
Proof state after:
case single
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
h : rcn = Execution.Instantaneous.Step.rcn a✝
⊢ rcn ≮[s₁✝.rtr] rcn

case trans.inl
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h✝ : rcn = Execution.Instantaneous.Step.rcn a✝¹
⊢ rcn ≮[s₁✝.rtr] rcn

case trans.inr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h✝ : rcn ∈ rcns a✝
⊢ rcn ≮[s₁✝.rtr] rcn
Theorem: Execution.Instantaneous.Step.TC.acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
h : rcn = Execution.Instantaneous.Step.rcn e
⊢ rcn ≮[s₁✝.rtr] rcn
Tactic:
case single e           => exact h ▸ e.acyclic
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h : rcn = Execution.Instantaneous.Step.rcn e
⊢ rcn ≮[s₁✝.rtr] rcn
Tactic:
case trans.inl e _ _ h  => exact h ▸ e.acyclic
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h : rcn ∈ rcns a✝
⊢ rcn ≮[s₁✝.rtr] rcn
Tactic:
case trans.inr e _ hi h => exact (hi h).equiv (Reactor.Equivalent.symm e.equiv)
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.acyclic
Proof state before:
case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h : rcn = Execution.Instantaneous.Step.rcn a✝¹ ∨ rcn ∈ rcns a✝
⊢ rcn ≮[s₁✝.rtr] rcn
Tactic:
cases ‹_ ∨ _›
Proof state after:
case trans.inl
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h✝ : rcn = Execution.Instantaneous.Step.rcn a✝¹
⊢ rcn ≮[s₁✝.rtr] rcn

case trans.inr
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h✝ : rcn ∈ rcns a✝
⊢ rcn ≮[s₁✝.rtr] rcn
Theorem: Execution.Instantaneous.Step.TC.acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
h : rcn = Execution.Instantaneous.Step.rcn e
⊢ rcn ≮[s₁✝.rtr] rcn
Tactic:
exact h ▸ e.acyclic
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h : rcn = Execution.Instantaneous.Step.rcn e
⊢ rcn ≮[s₁✝.rtr] rcn
Tactic:
exact h ▸ e.acyclic
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.acyclic
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ rcns a✝ → rcn ≮[s₂✝.rtr] rcn
h : rcn ∈ rcns a✝
⊢ rcn ≮[s₁✝.rtr] rcn
Tactic:
exact (hi h).equiv (Reactor.Equivalent.symm e.equiv)
Proof state after:
no goals
Theorem: Execution.Instantaneous.Step.TC.progress_not_mem_rcns
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
h : rcn ∈ s₁.progress
⊢ rcn ∉ rcns e
Tactic:
induction e <;> simp [rcns]
Proof state after:
case single
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
h : rcn ∈ s₁✝.progress
⊢ ¬rcn = Execution.Instantaneous.Step.rcn a✝

case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ s₂✝.progress → rcn ∉ rcns a✝
h : rcn ∈ s₁✝.progress
⊢ ¬(rcn = Execution.Instantaneous.Step.rcn a✝¹ ∨ rcn ∈ rcns a✝)
Theorem: Execution.Instantaneous.Step.TC.progress_not_mem_rcns
Proof state before:
case single
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
h : rcn ∈ s₁✝.progress
⊢ ¬rcn = Execution.Instantaneous.Step.rcn a✝

case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ : rcn ∈ s₂✝.progress → rcn ∉ rcns a✝
h : rcn ∈ s₁✝.progress
⊢ ¬(rcn = Execution.Instantaneous.Step.rcn a✝¹ ∨ rcn ∈ rcns a✝)
Tactic:
case' trans e e' hi => simp [hi $ e.progress_monotonic h]
Proof state after:
case trans
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ s₂✝.progress → rcn ∉ rcns e'
h : rcn ∈ s₁✝.progress
⊢ ¬rcn = Execution.Instantaneous.Step.rcn e

case single
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
h : rcn ∈ s₁✝.progress
⊢ ¬rcn = Execution.Instantaneous.Step.rcn a✝