English
Let s be a computation producing a at step m. For every n, if Results s a m holds, then Results (thinkN s n) a (m+n) holds.
Русский
Пусть s — вычисление, дающее a на шаге m. Тогда для любого n, если Results s a m, то Results (thinkN s n) a (m+n).
LaTeX
$$$$ \forall n,\ \operatorname{Results} s a m \rightarrow \operatorname{Results}(\mathrm{thinkN}\,s\,n)\ a\ (m+n). $$$$
Lean4
theorem results_thinkN {s : Computation α} {a m} : ∀ n, Results s a m → Results (thinkN s n) a (m + n)
| 0, h => h
| n + 1, h => results_think (results_thinkN n h)