Lean4
/-- `M.Path` represents a concrete path through the NFA from a start state to an end state
for a particular word.
Note that due to the non-deterministic nature of the automata, there can be more than one `Path`
for a given word.
Also note that this is `Type` and not a `Prop`, so that we can speak about the properties
of a particular `Path`, such as the set of states visited along the way (defined as `Path.supp`). -/
inductive Path : σ → σ → List α → Type (max u v)
| nil (s : σ) : Path s s []
| cons (t s u : σ) (a : α) (x : List α) : t ∈ M.step s a → Path t u x → Path s u (a :: x)
