length_thinkN — Mathlib

English

If s terminates, then length(thinkN s n) = length s + n.

Русский

Если s завершается, то длина thinkN s n равна длине s плюс n.

LaTeX

$$$$ \text{If } s \text{ Terminates},\quad \operatorname{length}(\mathrm{thinkN}\,s\,n) = \operatorname{length}(s) + n. $$$$

Lean4

@[simp]
theorem length_thinkN (s : Computation α) [_h : Terminates s] (n) : length (thinkN s n) = length s + n :=
  (results_thinkN n (results_of_terminates _)).length

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