get_think

Mathlib.Data.Seq.Computation

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

English

For terminating s, getting from think(s) yields the same as getting from s.

Русский

Для завершающегося s получение из think(s) даёт то же самое, что и из s.

LaTeX

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

Lean4

@[simp]
theorem get_think : get (think s) = get s :=
  get_eq_of_mem _ <|
    let ⟨n, h⟩ := get_mem s
    ⟨n + 1, h⟩

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

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

Разделы

Аффилиация

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