results_think — Mathlib

English

If h is a Results for think s, there exists m with s having Results a m and n = m+1.

Русский

Если h — результаты think s, существует m, что s имеет результаты a m и n = m+1.

LaTeX

$$$\forall {s} {a} {n}\; (\text{Results } (\text{think } s) a n) \rightarrow \exists m,\; \text{Results } s a m \wedge n = m + 1$$$

Lean4

theorem results_think {s : Computation α} {a n} (h : Results s a n) : Results (think s) a (n + 1) :=
  haveI := h.terminates
  ⟨think_mem h.mem, by rw [length_think, h.length]⟩

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