coefficients of primed variables are 0).

For all $j$ such that $j \neq i$ such that $x_j$ is not an induction variable of strata $< N$ and $n \leq j \leq 2n$, $c_{j} = 0$ (except for $x_i$ and induction variables of strata $< N$, all coefficients for unprimed variables are 0).

Thus, after computing the affine hull of ${{\varphi}_{\textsf{body}}}$, determining whether a given variable satisfies a stratified recurrence is simply a matter of solving a system of linear equations (e.g., using Gaussian elimination).

### Closed forms for stratified recurrences.

We first state a lemma:

The closed form for a stratified induction variable of strata $N$ is of the form $$x^{(k)} = p_0(k) + p_1(k)y_1^{(0)} + \dotsi + p_n(k)y_n^{(0)}$$ where each $y_i$ is a stratified induction variable of strata $<N$ and each $p_i(k) \in \mathbb{Q}[k]$ is a polynomial of one variable with rational coefficients.

Our algorithm for solving stratified recurrences is based on a constructive proof for this lemma. We proceed by induction on strata. The base case is trivial. Suppose that we have a recurrence at strata $N$ (and all $y_1,...,y_n$ are of strata $<N$): $x' = x + c_1y_1 + \dotsi + c_ny_n + b$. Then we may 