variable) at stratum 0.

Let $\vec{y}$ denote a vector of the stratified induction variables of strata $\leq N$. A recurrence of the form $x' = x + \vec{c}\vec{y}$ (where $\vec{c}$ is a vector of constants) is a stratified recurrence at stratum $N+1$ (and if $x$ satisfies such a recurrence, it is a stratified induction variable at stratum $N+1$).

We use ${\textsf{siv}}({\varphi})$ to denote the set of all stratified induction variables of ${\varphi}$.

$H \gets \bot$; $\psi \gets {{\varphi}_{\textsf{body}}}$

Let us now discuss how stratified recurrences are detected from a loop body formula ${{\varphi}_{\textsf{body}}}$. We begin by computing the affine hull ${\textit{aff}}({{\varphi}_{\textsf{body}}})$ of ${{\varphi}_{\textsf{body}}}$ (Algorithm \[alg:affine\_hull\]).[^1]

The *affine hull* ${\textit{aff}}({\varphi})$ of a formula ${\varphi}$ is the smallest affine set which contains ${\varphi}$, represented as (the set of solutions to) a system of equations $A\vec{x} = \vec{b}$, where $\vec{x} = \begin{bmatrix*}x_1 & \dotsi & x_n & x_1' & \dotsi & x_n' \end{bmatrix*}$. Logically, ${\textit{aff}}({\varphi})$ is a system of equations which satisfies the following three properties: (1) ${\varphi}\models {\textit{aff}}({\varphi})$, (2) every linear equation over ${\textsf{Var}}\cup {\textsf{Var}}'$ which is implied by ${\varphi}$ is also implied by ${\textit{aff}}({\varphi})$, and (3) no equation in ${\textit{aff}}({\varphi})$ is implied by the others.

Our strategy for detecting stratified recurrences 