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

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
⊢ Execution.Instantaneous.Step.rcn e :: rcns e' ≮[s₁.rtr] Execution.Instantaneous.Step.rcn e
Tactic:
by_contra hc
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
hc : ¬Execution.Instantaneous.Step.rcn e :: rcns e' ≮[s₁.rtr] Execution.Instantaneous.Step.rcn e
⊢ False

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
hc : ¬Execution.Instantaneous.Step.rcn e :: rcns e' ≮[s₁.rtr] Execution.Instantaneous.Step.rcn e
⊢ False
Tactic:
simp [Minimal] at hc
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
hc :
  (Execution.Instantaneous.Step.rcn e ≮[s₁.rtr] Execution.Instantaneous.Step.rcn e) →
    ∃ x ∈ rcns e', x <[s₁.rtr] Execution.Instantaneous.Step.rcn e
⊢ False

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
hc :
  (Execution.Instantaneous.Step.rcn e ≮[s₁.rtr] Execution.Instantaneous.Step.rcn e) →
    ∃ x ∈ rcns e', x <[s₁.rtr] Execution.Instantaneous.Step.rcn e
⊢ False
Tactic:
have ⟨_, hm, h⟩ := hc e.acyclic
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
hc :
  (Execution.Instantaneous.Step.rcn e ≮[s₁.rtr] Execution.Instantaneous.Step.rcn e) →
    ∃ x ∈ rcns e', x <[s₁.rtr] Execution.Instantaneous.Step.rcn e
w✝ : ID
hm : w✝ ∈ rcns e'
h : w✝ <[s₁.rtr] Execution.Instantaneous.Step.rcn e
⊢ False

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
hc :
  (Execution.Instantaneous.Step.rcn e ≮[s₁.rtr] Execution.Instantaneous.Step.rcn e) →
    ∃ x ∈ rcns e', x <[s₁.rtr] Execution.Instantaneous.Step.rcn e
w✝ : ID
hm : w✝ ∈ rcns e'
h : w✝ <[s₁.rtr] Execution.Instantaneous.Step.rcn e
⊢ False
Tactic:
replace hc := mt e.progress_monotonic $ e'.mem_rcns_not_mem_progress hm
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
w✝ : ID
hm : w✝ ∈ rcns e'
h : w✝ <[s₁.rtr] Execution.Instantaneous.Step.rcn e
hc : w✝ ∉ s₁.progress
⊢ False

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
w✝ : ID
hm : w✝ ∈ rcns e'
h : w✝ <[s₁.rtr] Execution.Instantaneous.Step.rcn e
hc : w✝ ∉ s₁.progress
⊢ False
Tactic:
exact hc $ e.allows_rcn.deps h
State after:
no goals