accepts_toDFA — Mathlib

English

The language accepted by the DFA built from L is exactly L.

Русский

Язык, принимаемый ДКА, построенным из L, совпадает с L.

LaTeX

$$$L.toDFA.accepts = L$$$

Lean4

@[simp]
theorem accepts_toDFA : L.toDFA.accepts = L := by
  ext x
  rw [DFA.mem_accepts]
  suffices L.toDFA.eval x = L.leftQuotient x by simp [this]
  induction x using List.reverseRecOn with
  | nil => simp
  | append_singleton x a ih => simp [ih, leftQuotient_append]

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