English
Let M be an NFA with a designated start state and a set of accepting states. A word x is accepted by M if and only if there exists a state S in the accepting set that is reachable from the start state by reading x.
Русский
Пусть M — НКА с начальным состоянием и множеством принимающих состояний. Слово x принимается M тогда и только тогда, когда существует состояние S из множества принимающих состояний, достижимое из начального состояния по чтению x.
LaTeX
$$$x \in M.accepts \iff \exists S \in M.accept, S \in M.evalFrom M.start x$$$
Lean4
theorem mem_accepts {x : List α} : x ∈ M.accepts ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x := by rfl
