and $\texttt{y}' \leq
\texttt{y}$. These inequations can be closed to yield $\texttt{x}^{(0)} - k
\leq \texttt{x}^{(k)}$ and $\texttt{x}^{(k)} \leq \texttt{x}^{(0)}$, $y^{(0)}
- k\leq y^{(k)}$, and $y^{(k)} \leq y^{(0)}$. In this section, we discuss linear recurrence (in)equations, which allow us to compute good approximations for loops that cannot be completely described by recurrence equations.

\[def:lri\] A *linear recurrence (in)equation* of a formula ${\varphi}$ is an (in)equation which is implied by ${\varphi}$ and which is of the form $$\vec{c}\vec{x}' \bowtie \vec{c}\vec{x} + \vec{b}\vec{y} + d$$ where $\mathop{\bowtie} \in \{ <, \leq, =\}$, $\vec{x}$ is any vector of variables, $\vec{y}$ is a vector of stratified induction variables in ${{\varphi}_{\textsf{body}}}$, $\vec{c}$, $\vec{b}$ are constant vectors, and $d$ is a constant.

Linear recurrence (in)equations generalize recurrence equations in two ways: first, they allow for *inequalities* rather than equations. Second, they allow recurrences for *linear terms*, rather than just variables. For example, the linear recurrence equation $(\texttt{x}' +
\texttt{y}') = (\texttt{x} + \texttt{y}) + 1$ is satisfied by the body of the loop above, which can be closed to yield $(\texttt{x}^{(k)} +
\texttt{y}^{(k)}) = (\texttt{x}^{(0)} + \texttt{y}^{(0)}) + k$.

We now describe our method for detecting and solving linear recurrence (in)equations. We begin by introducing a 