results_think_iff — Mathlib

English

Let s be a computation and a, n. Then think s yields a at step n+1 iff s yields a at step n.

Русский

Пусть s — вычисление и a, n — индексы. Тогда think s даёт a на шаге n+1 тогда и только тогда, когда s даёт a на шаге n.

LaTeX

$$$$ \operatorname{Results}(\mathrm{think}\,s)\ a\ (n+1) \leftrightarrow \operatorname{Results}s\ a\ n $$$$

Lean4

@[simp]
theorem results_think_iff {s : Computation α} {a n} : Results (think s) a (n + 1) ↔ Results s a n :=
  ⟨fun h => by
    let ⟨n', r, e⟩ := of_results_think h
    injection e with h'; rwa [h'], results_think⟩

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