evalFrom_append_singleton — Mathlib

English

For a DFA M, and any list x and symbol a, the value after appending a at the end equals stepping from the value after x: M.evalFrom s (x ++ [a]) = M.step (M.evalFrom s x) a.

Русский

Для детерминированного конечного автомата M и любой последовательности x и символа a, значение после добавления a в конец равно переходу от значения x: M.evalFrom s (x ++ [a]) = M.step (M.evalFrom s x) a.

LaTeX

$$$ M.\mathrm{evalFrom}(s, x \cup \{a\}) = M.\mathrm{step}(M.\mathrm{evalFrom}(s, x), a) $$$

Lean4

@[simp]
theorem evalFrom_append_singleton (s : σ) (x : List α) (a : α) : M.evalFrom s (x ++ [a]) = M.step (M.evalFrom s x) a :=
  by simp only [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]

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