English
For a path p from s to t reading x, the supp(p) is the finite set of states visited along the path, with the base case that a zero-length path from s visits only s, and the recursive step adds the current state to the visited set of the rest of the path.
Русский
Для траектории p из состояния s в состояние t, читающей x, supp(p) есть конечно множество состояний, посещаемых вдоль траектории: при нулевой длине пути посещается только s, а на каждом шаге добавляется текущее состояние к посещенным состояниям остатка траектории.
LaTeX
$$$\mathrm{supp}:\, M.Path\; s\; t\; x \to \mathrm{Finset}\; \sigma,\quad\mathrm{supp}(\mathrm{nil}\; s) = \{s\},\quad\mathrm{supp}(\mathrm{Path.cons}\; t_1\; s\; t\; a\; x\; h\; p) = \{s\} \cup \mathrm{supp}(p).$$$
Lean4
/-- Set of states visited by a path. -/
@[simp]
def supp [DecidableEq σ] {s t : σ} {x : List α} : M.Path s t x → Finset σ
| nil s => { s }
| cons _ _ _ _ _ _ p => { s } ∪ p.supp
