to₀

Mathlib.Computability.PostTuringMachine

URI: https://scilib.ai/kg/mathlib#Turing.Reaches.to₀

English

Every reachability path implies zero-level reachability.

Русский

Каждый путь достижимости влечет за собой нулевую достижимость.

LaTeX

$$$\\forall \\sigma\\ (f:\\\\sigma \\\\to \\\\mathrm{Option}\\\\, a,b:\\sigma),\\ Reaches\\ f\\ a\\ b \\Rightarrow Reaches_0\\ f\\ a\\ b$$$

Lean4

theorem to₀ {σ} {f : σ → Option σ} {a b : σ} (h : Reaches f a b) : Reaches₀ f a b
  | _, h₂ => h₂.trans_right h

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

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

Разделы

Аффилиация

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