is based on the following lemma. Combined with property (2) of ${\textit{aff}}({{\varphi}_{\textsf{body}}})$ above, this lemma implies that any equation implied by ${{\varphi}_{\textsf{body}}}$ can be expressed as a linear combination of the equations in ${\textit{aff}}({{\varphi}_{\textsf{body}}})$.

Let $A$ be a matrix, $\vec{b}$ be a column vector, $\vec{c}$ be a row vector, and $d$ be a constant. Assume that the system $A\vec{x} = b$ has a solution. Then $A\vec{x} = \vec{b}$ implies $\vec{c}\vec{x} = d$ iff there is a row vector $\vec{\lambda}$ such that $\vec{\lambda}A = \vec{c}$ and $\vec{\lambda}\vec{b} = d$.

Let us write ${\textit{aff}}({{\varphi}_{\textsf{body}}})$ as $A\vec{x} = \vec{b}$. Suppose that we have detected all recurrences of strata $< N$, and that we want to determine whether a variable $x_i$ ($0 \leq i \leq n$) is an induction variable at stratum $N$. Then we ask whether there exists $\vec{\lambda}$, $\vec{c}$, and $d$ such that:

$\vec{\lambda} A = \vec{c}$ and $\vec{\lambda}\vec{b} = d$ (i.e, $\vec{c}\vec{x} = d$ is implied by ${\textit{aff}}({{\varphi}_{\textsf{body}}})$ and thus by ${{\varphi}_{\textsf{body}}}$)

$c_i = 1$ and $c_{i+n} = -1$ (the coefficients of $x_i$ and $x_i'$ are 1 and -1, respectively)

For all $j$ such that $j \neq i+n$ and $n \leq j \leq 2n$, $c_{j} = 0$ (except for $x_i'$, all 