English
For a start state s, a target t, and input x, t belongs to the set of states reachable from s by reading x if and only if there exists a path from s to t reading x.
Русский
Для начального состояния s, конечного состояния t и входа x принадлежит t множеству состояний, достижимых из s после чтения x тогда и только тогда существует путь от s к t, читающий x.
LaTeX
$$$t \in M.evalFrom {s} x \iff \text{Nonempty} (M.Path s t x)$$$
Lean4
theorem mem_evalFrom_iff_nonempty_path {s t : σ} {x : List α} : t ∈ M.evalFrom { s } x ↔ Nonempty (M.Path s t x)
where
mp
h :=
match x with
| [] =>
have h : s = t := by simp at h; tauto
⟨h ▸ Path.nil s⟩
| a :: x =>
have h : ∃ s' ∈ M.step s a, t ∈ M.evalFrom { s' } x := by
rw [evalFrom_cons, mem_evalFrom_iff_exists, stepSet_singleton] at h; exact h
let ⟨s', h₁, h₂⟩ := h
let ⟨p'⟩ := mem_evalFrom_iff_nonempty_path.1 h₂
⟨Path.cons s' _ _ _ _ h₁ p'⟩
mpr
p :=
match p with
| ⟨Path.nil s⟩ => by simp
| ⟨Path.cons s' s t a x h₁ h₂⟩ =>
by
rw [evalFrom_cons, stepSet_singleton, mem_evalFrom_iff_exists]
exact ⟨s', h₁, mem_evalFrom_iff_nonempty_path.2 ⟨h₂⟩⟩
