evalFrom_append_singleton — Mathlib

English

Reading x followed by a single symbol a equals stepping from the value after x by a.

Русский

Чтение x затем символ a эквивалентно переходу на a от состояния после x.

LaTeX

$$M.evalFrom(S, x ++ [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
  simp only [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]

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