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

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e₁ : s ↓ᵢ s₁
e₂ : s ↓ᵢ s₂
h : rcn e₁ = rcn e₂
⊢ s₁ = s₂
Tactic:
cases e₁ <;> cases e₂ <;> simp [rcn] at h
State after:
case skip.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
s✝¹ : s ↓ₛ s₁
s✝ : s ↓ₛ s₂
h : Step.Skip.rcn s✝¹ = Step.Skip.rcn s✝
⊢ s₁ = s₂

case skip.exec
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
s✝ : s ↓ₛ s₁
e✝ : s ↓ₑ s₂
h : Step.Skip.rcn s✝ = Step.Exec.rcn e✝
⊢ s₁ = s₂

case exec.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝ : s ↓ₑ s₁
s✝ : s ↓ₛ s₂
h : Step.Exec.rcn e✝ = Step.Skip.rcn s✝
⊢ s₁ = s₂

case exec.exec
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝¹ : s ↓ₑ s₁
e✝ : s ↓ₑ s₂
h : Step.Exec.rcn e✝¹ = Step.Exec.rcn e✝
⊢ s₁ = s₂

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e₁ : s ↓ₛ s₁
e₂ : s ↓ₛ s₂
h : Step.Skip.rcn e₁ = Step.Skip.rcn e₂
⊢ s₁ = s₂
Tactic:
case skip.skip e₁ e₂ => simp [e₁.dst_eq, e₂.dst_eq, h]
State after:
no goals

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e₁ : s ↓ₑ s₁
e₂ : s ↓ₑ s₂
h : Step.Exec.rcn e₁ = Step.Exec.rcn e₂
⊢ s₁ = s₂
Tactic:
case exec.exec e₁ e₂ => simp [e₁.dst_eq, e₂.dst_eq, h, e₁.apply.deterministic (h.symm ▸ e₂.apply)]
State after:
no goals

State before:
case skip.exec
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
s✝ : s ↓ₛ s₁
e✝ : s ↓ₑ s₂
h : Step.Skip.rcn s✝ = Step.Exec.rcn e✝
⊢ s₁ = s₂

case exec.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝ : s ↓ₑ s₁
s✝ : s ↓ₛ s₂
h : Step.Exec.rcn e✝ = Step.Skip.rcn s✝
⊢ s₁ = s₂
Tactic:
all_goals
  have := ‹_ ↓ₛ _›.not_triggers_rcn
  have := ‹_ ↓ₑ _›.triggers_rcn
  simp_all
State after:
no goals

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e₁ : s ↓ₛ s₁
e₂ : s ↓ₛ s₂
h : Step.Skip.rcn e₁ = Step.Skip.rcn e₂
⊢ s₁ = s₂
Tactic:
simp [e₁.dst_eq, e₂.dst_eq, h]
State after:
no goals

State before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e₁ : s ↓ₑ s₁
e₂ : s ↓ₑ s₂
h : Step.Exec.rcn e₁ = Step.Exec.rcn e₂
⊢ s₁ = s₂
Tactic:
simp [e₁.dst_eq, e₂.dst_eq, h, e₁.apply.deterministic (h.symm ▸ e₂.apply)]
State after:
no goals

State before:
case exec.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝ : s ↓ₑ s₁
s✝ : s ↓ₛ s₂
h : Step.Exec.rcn e✝ = Step.Skip.rcn s✝
⊢ s₁ = s₂
Tactic:
have := ‹_ ↓ₛ _›.not_triggers_rcn
State after:
case exec.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝ : s ↓ₑ s₁
s✝ : s ↓ₛ s₂
h : Step.Exec.rcn e✝ = Step.Skip.rcn s✝
this : ¬State.Triggers s (Step.Skip.rcn s✝)
⊢ s₁ = s₂

State before:
case exec.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝ : s ↓ₑ s₁
s✝ : s ↓ₛ s₂
h : Step.Exec.rcn e✝ = Step.Skip.rcn s✝
this : ¬State.Triggers s (Step.Skip.rcn s✝)
⊢ s₁ = s₂
Tactic:
have := ‹_ ↓ₑ _›.triggers_rcn
State after:
case exec.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝ : s ↓ₑ s₁
s✝ : s ↓ₛ s₂
h : Step.Exec.rcn e✝ = Step.Skip.rcn s✝
this✝ : ¬State.Triggers s (Step.Skip.rcn s✝)
this : State.Triggers s (Step.Exec.rcn e✝)
⊢ s₁ = s₂

State before:
case exec.skip
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
e✝ : s ↓ₑ s₁
s✝ : s ↓ₛ s₂
h : Step.Exec.rcn e✝ = Step.Skip.rcn s✝
this✝ : ¬State.Triggers s (Step.Skip.rcn s✝)
this : State.Triggers s (Step.Exec.rcn e✝)
⊢ s₁ = s₂
Tactic:
simp_all
State after:
no goals