evalFrom_of_append — Mathlib

English

For any start state start and words x,y, the evaluation from start on the concatenation equals the evaluation from start on x followed by y: M.evalFrom start (x ++ y) = M.evalFrom (M.evalFrom start x) y.

Русский

Для любой стартовой конфигурации и слов x,y вычисление из начала на конкатенацию равно вычислению из начала на x с последующим y.

LaTeX

$$$ M.\mathrm{evalFrom}(start, x \!\++\!y) = M.\mathrm{evalFrom}(M.\mathrm{evalFrom}(start, x), y) $$$

Lean4

theorem evalFrom_of_append (start : σ) (x y : List α) : M.evalFrom start (x ++ y) = M.evalFrom (M.evalFrom start x) y :=
  List.foldl_append

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