User:CircuitCraft/Definition:Abstract Machine/Reachable Configuration

Definition

Let $\struct {S, \vdash}$ be an abstract machine.

Let $a, b \in S$ be configurations.

$b$ is reachable from $a$ if and only if there is a finite sequence $\sequence {s_0, s_1, \dotsc, s_n}$ such that:

$a = s_0 \vdash s_1 \vdash \dotso \vdash s_n = b$