α : Type u
β : Type v
S : WSeq (Computation α)
h : WSeq.head S ~> none
x✝ : Terminates (parallel S)
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right✝ : a ∈ c
⊢ False
α : Type u
β : Type v
S : WSeq (Computation α)
h : WSeq.head S ~> none
x✝ : Terminates (parallel S)
a : α
m : a ∈ parallel S
⊢ False
let ⟨c, cs, _⟩ := exists_of_mem_parallel m
α : Type u
β : Type v
S : WSeq (Computation α)
h : WSeq.head S ~> none
x✝ : Terminates (parallel S)
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right✝ : a ∈ c
n : ℕ
nm : some c ∈ WSeq.get? S n
⊢ False
α : Type u
β : Type v
S : WSeq (Computation α)
h : WSeq.head S ~> none
x✝ : Terminates (parallel S)
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right✝ : a ∈ c
⊢ False
let ⟨n, nm⟩ := WSeq.exists_get?_of_mem cs
α : Type u
β : Type v
S : WSeq (Computation α)
h : WSeq.head S ~> none
x✝ : Terminates (parallel S)
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right✝ : a ∈ c
n : ℕ
nm : some c ∈ WSeq.get? S n
c' : Computation α
h' : some c' ∈ WSeq.head S
⊢ False
α : Type u
β : Type v
S : WSeq (Computation α)
h : WSeq.head S ~> none
x✝ : Terminates (parallel S)
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right✝ : a ∈ c
n : ℕ
nm : some c ∈ WSeq.get? S n
⊢ False
let ⟨c', h'⟩ := WSeq.head_some_of_get?_some nm
no goals
α : Type u
β : Type v
S : WSeq (Computation α)
h : WSeq.head S ~> none
x✝ : Terminates (parallel S)
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right✝ : a ∈ c
n : ℕ
nm : some c ∈ WSeq.get? S n
c' : Computation α
h' : some c' ∈ WSeq.head S
⊢ False
injection h h'