evalFrom — Mathlib

English

EvalFrom defines, for a starting set S, the set of states reachable by reading a word x from any element of S, by folding stepSet along the list x.

Русский

EvalFrom задаёт множество состояний, достижимых чтением слова x из любого элемента S, получая результат последовательного применения stepSet по списку x.

LaTeX

$$evalFrom(S) : List α → Set σ := List.foldl M.stepSet S$$

Lean4

/-- `M.evalFrom S x` computes all possible paths through `M` with input `x` starting at an element
  of `S`. -/
def evalFrom (S : Set σ) : List α → Set σ :=
  List.foldl M.stepSet S

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