variables, $\vec{c}$ and $\vec{b}$ are constant vectors, and $d$ is a constant). Recalling the definition of the difference variables, we may rewrite such an inequation as $\vec{c}\vec{(\vec{x}'-\vec{x})} \bowtie \vec{b}\vec{y} + d$ and then rewrite again as $\vec{c}\vec{x}' \bowtie \vec{c}\vec{x} + \vec{b}\vec{y}
+ d$, which matches the definition of linear recurrence (in)equations given in Definition \[def:lri\].

We may close such a linear recurrence (in)equation as follows: $$\vec{c}\vec{x}^{(k)} \bowtie \vec{c}\vec{x}^{(0)} + \sum_{i=0}^{k-1} \vec{b}\vec{y}^{(i)} + d$$ We can compute a closed form for the summation $\sum_{i=0}^{k-1}
\vec{b}\vec{y}^{(i)} + d$ as in the preceding section.

Loop guards
-----------

A loop body typically contains crucial information about the execution of the loop that cannot be captured by recurrence relations. For example, consider the loop in Section \[sec:stratified\]. Supposing that the loop executes $n$ times, we must have that $\texttt{x}^{(k)} \leq 10$ for each $k < n$. Further, consider that the variable `z` is a function of the simple induction variable `x`, and so $\texttt{z}^{(k)}$ can be described precisely in terms of the pre-state variables (even though it does not itself satisfy any recurrence): $$\texttt{z}^{(k)} = 
\begin{cases}
  \texttt{z}^{(0)} & \text{if } k = 0\\
  2(\texttt{x}^{(0)} + k + 1) & \text{otherwise.}
\end{cases}$$ The question is: how 