accepts_iff_exists_path — Mathlib

English

Let x be a word. Then x is accepted by M if and only if there exist a start state s and an accept state t such that there is a path from s to t reading x.

Русский

Пусть x — слово. Тогда x принимается НКА M тогда и только тогда найдутся начальное состояние s и принимающее состояние t such that существует траектория от s к t, читающая x.

LaTeX

$$$x \in M.accepts \iff \exists s \in M.start, \exists t \in M.accept, Nonempty (M.Path s t x)$$$

Lean4

theorem accepts_iff_exists_path {x : List α} : x ∈ M.accepts ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, Nonempty (M.Path s t x) :=
  by
  simp only [← mem_evalFrom_iff_nonempty_path, mem_accepts, mem_evalFrom_iff_exists (S := M.start)]
  tauto

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