destruct_terminates_of_get?_terminates

English

If some get? s n terminates for a WSeq s, then the whole destruct structure of s terminates. In essence, termination of a get? index propagates to the destructed sequence.

Русский

Если на позиции n в последовательности s завершение get? имеет место, то завершается и структура разложения дескрт. В общем, завершение на позиции передаётся к разложенной последовательности.

LaTeX

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

Lean4

theorem destruct_terminates_of_get?_terminates {s : WSeq α} {n} (T : Terminates (get? s n)) : Terminates (destruct s) :=
  (head_terminates_iff _).1 <| head_terminates_of_get?_terminates T

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