toNFA_correct — Mathlib

English

A DFA M and its transduction to an NFA have identical acceptance behavior; the NFA accepts a word iff the DFA does.

Русский

ДКА и соответствующая ей NFA имеют одинаковую принимаемость; слово принимается NFA тогда же, когда оно принимается ДКА.

LaTeX

$$$M.toNFA.accepts = M.accepts$$$

Lean4

@[simp]
theorem toNFA_correct (M : DFA α σ) : M.toNFA.accepts = M.accepts :=
  by
  ext x
  rw [NFA.mem_accepts, toNFA_start, toNFA_evalFrom_match]
  constructor
  · rintro ⟨S, hS₁, hS₂⟩
    rwa [Set.mem_singleton_iff.mp hS₂] at hS₁
  · exact fun h => ⟨M.eval x, h, rfl⟩

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