mem_accepts — Mathlib

English

An input x is accepted by the DFA iff its evaluation equals an accepting state: x ∈ M.accepts iff M.eval x ∈ M.accept.

Русский

Вход x принимается ДФА тогда и только тогда, когда его вычисление достигает принимающего состояния.

LaTeX

$$$ x \in M.\mathrm{accepts} \iff M.\mathrm{eval}(x) \in M.\mathrm{accept} $$$

Lean4

theorem mem_accepts {x : List α} : x ∈ M.accepts ↔ M.eval x ∈ M.accept := by rfl

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