trans

Mathlib.Computability.TMComputable

URI: https://scilib.ai/kg/mathlib#Turing.EvalsTo.trans

Lean4

/-- Transitivity of `EvalsTo` in the sum of the numbers of steps. -/
@[trans]
def trans {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) (c : Option σ) (h₁ : EvalsTo f a b) (h₂ : EvalsTo f b c) :
    EvalsTo f a c :=
  ⟨h₂.steps + h₁.steps, by rw [Function.iterate_add_apply, h₁.evals_in_steps, h₂.evals_in_steps]⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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