step_one

Mathlib.Computability.EpsilonNFA

URI: https://scilib.ai/kg/mathlib#εNFA.step_one

English

The one-state εNFA has empty-step transitions.

Русский

У εНКА с одним состоянием переходы по шагу равны пустому множеству.

LaTeX

$$$(1 : \\varepsilonNFA \\alpha \\sigma).step s a = \\emptyset$$$

Lean4

@[simp]
theorem step_one (s a) : (1 : εNFA α σ).step s a = ∅ :=
  rfl

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

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

Разделы

Аффилиация

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