get_thinkN

Mathlib.Data.Seq.Computation

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

English

For terminating s, get(thinkN(s,n)) = get(s) for every n.

Русский

Для завершающегося s, get(thinkN(s,n)) = get(s) при любом n.

LaTeX

$$$\forall s\,[h:\,\text{Terminates}(s)],\; \forall n,\; \text{get}(\text{thinkN } s\; n) = \text{get } s$$$

Lean4

@[simp]
theorem get_thinkN (n) : get (thinkN s n) = get s :=
  get_eq_of_mem _ <| (thinkN_mem _).2 (get_mem _)

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

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

Разделы

Аффилиация

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