English
For a deterministic finite automaton M, the left quotient of the language recognized by M is obtained by first evaluating an input word to a state of M, and then taking the set of continuations from that state that lead to acceptance. Equivalently, for every word w, the left quotient by w equals the set of continuations from the state M.eval(w): leftQuotient(M.accepts)(w) = M.acceptsFrom(M.eval(w)). In particular, leftQuotient(M.accepts) = M.acceptsFrom ∘ M.eval.
Русский
Для детерминированного конечного автомата M левый делитель языка, распознаваемого M, определяется следующим образом: сначала по слову w переходим в состояние M.eval(w), затем берём множество продолжений, приводящих к принятию. Тождество: для каждого w выполняется leftQuotient(M.accepts)(w) = M.acceptsFrom(M.eval(w)). Следовательно, leftQuotient(M.accepts) = M.acceptsFrom ∘ M.eval.
LaTeX
$$$\operatorname{leftQuotient}(\operatorname{accepts}_M) = \operatorname{acceptsFrom} \circ \operatorname{eval}_M.$$$
Lean4
theorem leftQuotient_accepts (M : DFA α σ) : leftQuotient M.accepts = M.acceptsFrom ∘ M.eval :=
funext <| leftQuotient_accepts_apply M
