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

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
h : rcn ∈ rcns e
⊢ rcn ∉ s₁.progress
Tactic:
induction e
State after:
case single
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
a✝ : s₁✝ ↓ᵢ s₂✝
h : rcn ∈ rcns (single a✝)
⊢ rcn ∉ s₁✝.progress

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₂✝.progress
h : rcn ∈ rcns (trans a✝¹ a✝)
⊢ rcn ∉ s₁✝.progress

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
h : rcn ∈ rcns (single e)
⊢ rcn ∉ s₁✝.progress
Tactic:
case single e =>
  simp [rcns] at h
  exact h ▸ e.rcn_not_mem_progress
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ rcns e' → rcn ∉ s₂✝.progress
h : rcn ∈ rcns (trans e e')
⊢ rcn ∉ s₁✝.progress
Tactic:
case trans e e' hi =>
  cases e'.rcns_trans_eq_cons e ▸ h
  case head   => exact e.rcn_not_mem_progress
  case tail h => exact mt e.progress_monotonic (hi h)
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
h : rcn ∈ rcns (single e)
⊢ rcn ∉ s₁✝.progress
Tactic:
simp [rcns] at h
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
h : rcn = Execution.Instantaneous.Step.rcn e
⊢ rcn ∉ s₁✝.progress

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₁✝.progress
Tactic:
exact h ▸ e.rcn_not_mem_progress
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ rcns e' → rcn ∉ s₂✝.progress
h : rcn ∈ rcns (trans e e')
⊢ rcn ∉ s₁✝.progress
Tactic:
cases e'.rcns_trans_eq_cons e ▸ h
State after:
case head
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn e ∈ rcns e' → rcn e ∉ s₂✝.progress
h : rcn e ∈ rcns (trans e e')
⊢ rcn e ∉ s₁✝.progress

case tail
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ rcns e' → rcn ∉ s₂✝.progress
h : rcn ∈ rcns (trans e e')
a✝ : Mem rcn (rcns e')
⊢ rcn ∉ s₁✝.progress

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn e ∈ rcns e' → rcn e ∉ s₂✝.progress
h : rcn e ∈ rcns (trans e e')
⊢ rcn e ∉ s₁✝.progress
Tactic:
case head   => exact e.rcn_not_mem_progress
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ rcns e' → rcn ∉ s₂✝.progress
h✝ : rcn ∈ rcns (trans e e')
h : Mem rcn (rcns e')
⊢ rcn ∉ s₁✝.progress
Tactic:
case tail h => exact mt e.progress_monotonic (hi h)
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn e ∈ rcns e' → rcn e ∉ s₂✝.progress
h : rcn e ∈ rcns (trans e e')
⊢ rcn e ∉ s₁✝.progress
Tactic:
exact e.rcn_not_mem_progress
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₃✝
hi : rcn ∈ rcns e' → rcn ∉ s₂✝.progress
h✝ : rcn ∈ rcns (trans e e')
h : Mem rcn (rcns e')
⊢ rcn ∉ s₁✝.progress
Tactic:
exact mt e.progress_monotonic (hi h)
State after:
no goals