+ kc$ (writing $x^{(k)}$ for the value that $x$ obtains on the $k$th iteration of the loop). To provide some early intuition on the iteration operator to be developed in the remainder of this section, let us suppose that we are only interested in simple recurrences. Then a possible definition for the iteration operator is $${{\varphi}_{\textsf{body}}}^{\ostar}{\triangleq}{\fbox{$\exists k \geq 0. \bigwedge \{ x' = x + kc : x' = x + c \in \textit{SR}({{\varphi}_{\textsf{body}}}) \}$}}$$ where $\textit{SR}({{\varphi}_{\textsf{body}}})$ is the set of simple recurrences satisfied by ${{\varphi}_{\textsf{body}}}$.

The iteration operator defined above is sound (it over-approximates the behaviour of any number of iterations of the loop, since each variable is either described exactly by a recurrence or is not constrained at all), but it is imprecise. The remainder of this section discusses more general recurrence equations which can be used to compute more precise transition invariants for loops.

Stratified recurrences equations {#sec:stratified}
--------------------------------

Consider the loop shown to the right. We can see that `x` satisfies a simple recurrence equation $\texttt{x}' = \texttt{x} + 1$, and that `y` satisfies a (non-simple) recurrence equation $\texttt{y}' = \texttt{y} +
\texttt{x} + 1$. A closed form for `y`’s recurrence is $y^{(k)} =
\texttt{y}^{(0)} + 