\sum_{i=0}^{k-1} (\texttt{x}^{(i)} + 1)$. Since `x` satisfies a simple recurrence ($x' = x + 1$), we have a closed form for $\texttt{x}^{(i)}$, so we may simplify this recurrence and remove the summation:

$$\texttt{y}^{(k)} =
\texttt{y}^{(0)} + \sum_{i=0}^{k-1} (\texttt{x}^{(0)} + i + 1) = \texttt{y}^{(0)} + k\texttt{x}^{(0)} + k + \sum_{i=0}^{k-1} i = \texttt{y}^{(0)} +
k\texttt{x}^{(0)} + \frac{k(k+1)}{2}.$$

*Stratified recurrence equations* generalize this idea: starting from simple recurrence equations, we solve more and more complicated recurrences using the closed forms for simpler ones. As with the example above, stratified recurrences have non-linear closed forms. Non-linear invariant generation is not the main focus of our work, but it is sometimes a necessary intermediate step for proving *linear* invariants in a compositional setting: since our analysis cannot take advantage of contextual information when analyzing a loop, we generate a non-linear invariant and then, after the analysis has examined more context, simplify it (using the linearization algorithm from Section \[sec:discussion\]).

Let ${\varphi}$ be a formula. The stratified recurrence equations (and stratified induction variables) of ${\varphi}$ are defined inductively as:

A simple recurrence equation which is satisfied by ${\varphi}$ is a stratified recurrence equation of ${\varphi}$ (and a simple induction variable is a stratified induction 