of_think_terminates

Mathlib.Data.Seq.Computation

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

English

Terminates (think s) implies Terminates s.

Русский

Терминирование (think s) ⇒ Терминирование s.

LaTeX

$$$\mathrm{Terminates}(\mathrm{think}(s)) \Rightarrow \mathrm{Terminates}(s)$$$

Lean4

theorem of_think_terminates {s : Computation α} : Terminates (think s) → Terminates s
  | ⟨⟨a, h⟩⟩ => ⟨⟨a, of_think_mem h⟩⟩

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

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

Разделы

Аффилиация

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