head_terminates_of_head_tail_terminates

English

If the head of the tail terminates, then the head terminates.

Русский

Если terminates у head(tail s), тогда terminates у head s.

LaTeX

$$$$\operatorname{Terminates}(\operatorname{head}(\operatorname{tail}(s))) \Rightarrow \operatorname{Terminates}(\operatorname{head}(s)).$$$$

Lean4

theorem head_terminates_of_head_tail_terminates (s : WSeq α) [T : Terminates (head (tail s))] : Terminates (head s) :=
  (head_terminates_iff _).2 <| by
    rcases (head_terminates_iff _).1 T with ⟨⟨a, h⟩⟩
    simp? [tail]  at h says simp only [tail, destruct_flatten, bind_map_left] at h
    rcases exists_of_mem_bind h with ⟨s', h1, _⟩
    exact terminates_of_mem h1

Похожие утверждения