case mk.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
T : Terminates (head (tail s))
a : Option (α × WSeq α)
h : a ∈ destruct (tail s)
⊢ Terminates (destruct s)
α : Type u
β : Type v
γ : Type w
s : WSeq α
T : Terminates (head (tail s))
⊢ Terminates (destruct s)
rcases (head_terminates_iff _).1 T with ⟨⟨a, h⟩⟩
case mk.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
T : Terminates (head (tail s))
a : Option (α × WSeq α)
h : a ∈ (fun o => Option.rec nil Prod.snd o) <$> destruct s >>= destruct
⊢ Terminates (destruct s)
case mk.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
T : Terminates (head (tail s))
a : Option (α × WSeq α)
h : a ∈ destruct (tail s)
⊢ Terminates (destruct s)
simp [tail] at h
case mk.intro.intro.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
T : Terminates (head (tail s))
a : Option (α × WSeq α)
h : a ∈ (fun o => Option.rec nil Prod.snd o) <$> destruct s >>= destruct
s' : WSeq α
h1 : s' ∈ (fun o => Option.rec nil Prod.snd o) <$> destruct s
right✝ : a ∈ destruct s'
⊢ Terminates (destruct s)
case mk.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
T : Terminates (head (tail s))
a : Option (α × WSeq α)
h : a ∈ (fun o => Option.rec nil Prod.snd o) <$> destruct s >>= destruct
⊢ Terminates (destruct s)
rcases exists_of_mem_bind h with ⟨s', h1, _⟩
case mk.intro.intro.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
T : Terminates (head (tail s))
a : Option (α × WSeq α)
h : a ∈ (fun o => Option.rec nil Prod.snd o) <$> destruct s >>= destruct
s' : WSeq α
h1 : s' ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) (destruct s)
right✝ : a ∈ destruct s'
⊢ Terminates (destruct s)
case mk.intro.intro.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
T : Terminates (head (tail s))
a : Option (α × WSeq α)
h : a ∈ (fun o => Option.rec nil Prod.snd o) <$> destruct s >>= destruct
s' : WSeq α
h1 : s' ∈ (fun o => Option.rec nil Prod.snd o) <$> destruct s
right✝ : a ∈ destruct s'
⊢ Terminates (destruct s)
unfold Functor.map at h1
no goals
case mk.intro.intro.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
T : Terminates (head (tail s))
a : Option (α × WSeq α)
h : a ∈ (fun o => Option.rec nil Prod.snd o) <$> destruct s >>= destruct
s' : WSeq α
h1 : s' ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) (destruct s)
right✝ : a ∈ destruct s'
⊢ Terminates (destruct s)
exact
  let ⟨t, h3, _⟩ := Computation.exists_of_mem_map h1
  Computation.terminates_of_mem h3