eval_append_singleton

Mathlib.Computability.EpsilonNFA

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

English

Evaluating with an appending singleton equals applying evalFrom append singleton.

Русский

Оценка через добавление одиночного элемента равна применению evalFrom к добавлению.

LaTeX

$$M.\\eval( x \\cup [a] ) = M.\\stepSet (M.\\eval x) a$$

Lean4

@[simp]
theorem eval_append_singleton (x : List α) (a : α) : M.eval (x ++ [a]) = M.stepSet (M.eval x) a :=
  evalFrom_append_singleton _ _ _ _

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

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

Разделы

Аффилиация

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