terminates_iff

Mathlib.Data.Seq.Computation

URI: https://scilib.ai/kg/mathlib#Computation.terminates_iff

English

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

Русский

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

LaTeX

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

Lean4

theorem terminates_iff (s : Computation α) : Terminates s ↔ ∃ a, a ∈ s :=
  ⟨fun h => h.1, Terminates.mk⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru