terminates_def — Mathlib

English

For a computation s, Terminates s is equivalent to the existence of an index n such that (s.1 n).isSome.

Русский

Для вычисления s существует индекс n такой, что (s.1 n).isSome.

LaTeX

$$$\mathrm{Terminates}(s) \iff \exists n, (s.1\,n).isSome$$$

Lean4

theorem terminates_def (s : Computation α) : Terminates s ↔ ∃ n, (s.1 n).isSome :=
  ⟨fun ⟨⟨a, n, h⟩⟩ =>
    ⟨n, by
      dsimp [Stream'.get] at h
      rw [← h]
      exact rfl⟩,
    fun ⟨n, h⟩ => ⟨⟨Option.get _ h, n, (Option.eq_some_of_isSome h).symm⟩⟩⟩

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