of_thinkN_terminates — Mathlib

English

Let s be a computation and n a natural number. If the thinkN transformation of s terminates after n steps, then the original computation s terminates.

Русский

Пусть s — вычисление и n — натуральное число. Если thinkN(s, n) завершается, тогда исходное вычисление s завершается.

LaTeX

$$$ \forall s\, \forall n\, \operatorname{Terminates}(\text{thinkN}(s,n)) \rightarrow \operatorname{Terminates}(s) $$$

Lean4

theorem of_thinkN_terminates (s : Computation α) (n) : Terminates (thinkN s n) → Terminates s
  | ⟨⟨a, h⟩⟩ => ⟨⟨a, (thinkN_mem _).1 h⟩⟩

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