English
Let s be a well‑infinite sequence (WSeq) with indices in natural numbers. If m ≤ n and the retrieval at position n terminates, then the retrieval at position m also terminates. In other words, termination of get? at a later index implies termination at any earlier index.
Русский
Пусть s — бесконечная последовательность вида WSeq. Если m ≤ n и завершение получения значения на позиции n имеет место, то завершение получения на позиции m тоже имеет место. Иными словами, завершение get? на более позднем индексе следует из завершения на более раннем.
LaTeX
$$$$\forall s:\\mathrm{WSeq}\,\alpha,\ \forall m,n\in\mathbb{N},\ m \le n \;\to\; \operatorname{Terminates}(\mathrm{get?}\,s\,n) \to \operatorname{Terminates}(\mathrm{get?}\,s\,m).$$$$
Lean4
theorem get?_terminates_le {s : WSeq α} {m n} (h : m ≤ n) : Terminates (get? s n) → Terminates (get? s m) := by
induction h with
| refl => exact id
| step _ IH => exact fun T ↦ IH (@head_terminates_of_head_tail_terminates _ _ T)
