evalFrom_append_singleton — Mathlib

English

Appending a single element a to the input corresponds to applying stepSet to the previous result.

Русский

Добавление элемента a к списку приводит к применению stepSet к предыдущему результату.

LaTeX

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

Lean4

@[simp]
theorem evalFrom_append_singleton (S : Set σ) (x : List α) (a : α) :
    M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a := by
  rw [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]

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