terminates

Mathlib.Data.Seq.Computation

URI: https://scilib.ai/kg/mathlib#Computation.Results.terminates

English

If s has a Results a n, then s terminates.

Русский

Если у s есть результаты a n, то s завершается.

LaTeX

$$$\forall s\, {a}\, {n},\; \text{Results } s a n \rightarrow \text{Terminates } s$$$

Lean4

theorem terminates {s : Computation α} {a n} (h : Results s a n) : Terminates s :=
  terminates_of_mem h.mem

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

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

Разделы

Аффилиация

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