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

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
h : i ∈ rcns e'
⊢ Execution.Instantaneous.Step.rcn e ≠ i
Tactic:
intro hc
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
h : i ∈ rcns e'
hc : Execution.Instantaneous.Step.rcn e = i
⊢ False

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
h : i ∈ rcns e'
hc : Execution.Instantaneous.Step.rcn e = i
⊢ False
Tactic:
have := trans e e' |>.rcns_nodup
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
h : i ∈ rcns e'
hc : Execution.Instantaneous.Step.rcn e = i
this : Nodup (rcns (trans e e'))
⊢ False

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
h : i ∈ rcns e'
hc : Execution.Instantaneous.Step.rcn e = i
this : Nodup (rcns (trans e e'))
⊢ False
Tactic:
have := hc.symm ▸ List.not_nodup_cons_of_mem h
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
h : i ∈ rcns e'
hc : Execution.Instantaneous.Step.rcn e = i
this✝ : Nodup (rcns (trans e e'))
this : ¬Nodup (Execution.Instantaneous.Step.rcn e :: rcns e')
⊢ False

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₃ : State α
i : ID
e : s₁ ↓ᵢ s₂
e' : s₂ ↓ᵢ+ s₃
h : i ∈ rcns e'
hc : Execution.Instantaneous.Step.rcn e = i
this✝ : Nodup (rcns (trans e e'))
this : ¬Nodup (Execution.Instantaneous.Step.rcn e :: rcns e')
⊢ False
Tactic:
contradiction
State after:
no goals