toεNFA_evalFrom_match — Mathlib

English

Equality of evalFrom results when translating an NFA to an εNFA and using evalFrom from a start set.

Русский

Сопоставление результатов evalFrom при переводе НКА в εНКА и использовании evalFrom на множестве начала.

LaTeX

$$$M.toεNFA.evalFrom start = M.evalFrom start$$$

Lean4

@[simp]
theorem toεNFA_evalFrom_match (M : NFA α σ) (start : Set σ) : M.toεNFA.evalFrom start = M.evalFrom start :=
  by
  rw [evalFrom, εNFA.evalFrom, toεNFA_εClosure]
  suffices εNFA.stepSet (toεNFA M) = stepSet M by rw [this]
  ext S s
  simp only [stepSet, εNFA.stepSet, exists_prop, Set.mem_iUnion]
  apply exists_congr
  simp only [and_congr_right_iff]
  intro _ _
  rw [M.toεNFA_εClosure]
  rfl

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