head_terminates_of_get?_terminates

English

If some get? s n terminates for some index n, then the head of the sequence s terminates. In short, termination of a retrieval somewhere implies the head step is terminating.

Русский

Если для некоторого индекса n завершение get? s n имеет место, то головной элемент последовательности s завершается.

LaTeX

$$$$\forall s:\\mathrm{WSeq}\,\alpha,\forall n:\\mathbb{N},\ \operatorname{Terminates}(\mathrm{get?}\,s\,n) \Rightarrow \operatorname{Terminates}(\mathrm{head}\,s).$$$$

Lean4

theorem head_terminates_of_get?_terminates {s : WSeq α} {n} : Terminates (get? s n) → Terminates (head s) :=
  get?_terminates_le (Nat.zero_le n)

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