toNFA_evalFrom_match — Mathlib

English

The evaluation function from a start set for an εNFA M and its corresponding NFA M.toNFA agree after taking the ε-closure: evalFrom(start) computed via M equals evalFrom(start) computed via M.toNFA with the ε-closure of start.

Русский

Функции вычисления из множества начала для ε-НКА M и соответствующего НКА M.toNFA совпадают после применения ε-замыкания: evalFrom(start) для M совпадает с evalFrom(start) для M.toNFA.

LaTeX

$$$M.toNFA.evalFrom (M.\\varepsilonClosure\\, start) = M.evalFrom start$$$

Lean4

@[simp]
theorem toNFA_evalFrom_match (start : Set σ) : M.toNFA.evalFrom (M.εClosure start) = M.evalFrom start :=
  rfl

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