leftQuotient_accepts_apply — Mathlib

English

For a DFA M and a word x, the left quotient of the language of accepts by x equals acceptsFrom (M.eval x): leftQuotient M.accepts x = M.acceptsFrom (M.eval x).

Русский

Для детерминированного конечного автомата M и слова x левая частная Accepts по x равна acceptsFrom (M.eval x): leftQuotient M.accepts x = M.acceptsFrom (M.eval x).

LaTeX

$$$\\text{leftQuotient}\\ M.accepts\\ x = M.acceptsFrom\\ (M.eval\\ x)$$$

Lean4

theorem leftQuotient_accepts_apply (M : DFA α σ) (x : List α) : leftQuotient M.accepts x = M.acceptsFrom (M.eval x) :=
  by
  ext y
  simp [DFA.mem_accepts, DFA.mem_acceptsFrom, DFA.eval, DFA.evalFrom_of_append]

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