Finite-state path expression ($R_{ij}^{(k)}$)

For numbered states of a finite-state automaton, $R_{ij}^{(k)}$ is a regular expression describing paths from $i$ to $j$ whose internal states have numbers at most $k$. Splitting a path at its visits to state $k$ gives $R_{ij}^{(k)}=R_{ij}^{(k-1)}+R_{ik}^{(k-1)}(R_{kk}^{(k-1)}{)}^{\ast }{R}_{kj}^{(k-1)}$. At stage zero use individual edge labels and an empty-word option when the endpoints coincide. This proves the automaton-to-expression direction of Kleene theorem.