eq_thinkN'

Mathlib.Data.Seq.Computation

URI: https://scilib.ai/kg/mathlib#Computation.eq_thinkN'

English

If s terminates, then s = thinkN (pure (get s)) (length s).

Русский

Если s завершается, то s = thinkN (pure (get s)) (length s).

LaTeX

$$$$ \text{If } \operatorname{Terminates} s,\quad s = \mathrm{thinkN}(\mathrm{pure}(\mathrm{get}\,s))\ \mathrm{length}(s). $$$$

Lean4

theorem eq_thinkN' (s : Computation α) [_h : Terminates s] : s = thinkN (pure (get s)) (length s) :=
  eq_thinkN (results_of_terminates _)

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

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

Разделы

Аффилиация

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