mem_acceptsFrom — Mathlib

English

For any start state s and input x, membership x ∈ M.acceptsFrom s is equivalent to M.evalFrom s x ∈ M.accept.

Русский

Для любого состояния начала s и входа x принадлежность x ∈ M.acceptsFrom s эквивалентна тому, что M.evalFrom s x ∈ M.accept.

LaTeX

$$$ x \in M.\mathrm{acceptsFrom}(s) \iff M.\mathrm{evalFrom}(s, x) \in M.\mathrm{accept} $$$

Lean4

theorem mem_acceptsFrom {s : σ} {x : List α} : x ∈ M.acceptsFrom s ↔ M.evalFrom s x ∈ M.accept := by rfl

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