English
Let M be an εNFA and x a list of symbols. Then x is in the language accepted by M if and only if there exist a start state s1, an accept state s2, and a path from s1 to s2 labeled by some x′ whose reduction reduces to x.
Русский
Пусть M — ε-НКА и x — список символов. Тогда x принадлежит языку, принятому M, тогда и только тогда существуют начальное состояние s1, принимающее состояние s2 и путь от s1 до s2, помеченный некоторым x′, такой что x′ приводит к x.
LaTeX
$$$x \\in M.accepts \\iff \\exists s_1 \\in M.start, \\exists s_2 \\in M.accept, \\exists x' : List (Option \\alpha), x'.reduceOption = x \\land M.IsPath s_1 s_2 x'$$$
Lean4
theorem mem_accepts_iff_exists_path {x : List α} :
x ∈ M.accepts ↔ ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
where
mp := by
intro ⟨s₂, _, h⟩
rw [eval, mem_evalFrom_iff_exists] at h
obtain ⟨s₁, _, h⟩ := h
rw [mem_evalFrom_iff_exists_path] at h
tauto
mpr := by
intro ⟨s₁, s₂, x', hs₁, hs₂, h⟩
have := M.mem_evalFrom_iff_exists.mpr ⟨_, hs₁, M.mem_evalFrom_iff_exists_path.mpr ⟨_, h⟩⟩
exact ⟨s₂, hs₂, this⟩
