head

Mathlib.Computability.PostTuringMachine

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

English

If b ∈ f a and Reaches₀ f b c hold, then Reaches₀ f a c.

Русский

Если b ∈ f a и Reaches₀ f b c, то Reaches₀ f a c.

LaTeX

$$$\\mathrm{Option.instMembership.mem}(f\\ a,b) \\rightarrow \\mathrm{Reaches_0}\\ f\\ b\\ c \\rightarrow \\mathrm{Reaches_0}\\ f\\ a\\ c$$$

Lean4

theorem head {σ} {f : σ → Option σ} {a b c : σ} (h : b ∈ f a) (h₂ : Reaches₀ f b c) : Reaches₀ f a c :=
  (Reaches₀.single h).trans h₂

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

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

Разделы

Аффилиация

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