set of *difference variables* $\delta_x$, one for each variable $x \notin {\textsf{siv}}({{\varphi}_{\textsf{body}}})$ (variables which do belong to ${\textsf{siv}}({{\varphi}_{\textsf{body}}})$ are already precisely described by recurrence equations, so we need not approximate them). We then compute (via Algorithm \[alg:convex\_hull\]) the convex hull of the formula $\psi$ defined as:

$$\psi {\triangleq}\exists X. {{\varphi}_{\textsf{body}}}\land \bigwedge \{ \delta_x = x' - x : x \in {\textsf{Var}}\setminus {\textsf{siv}}({{\varphi}_{\textsf{body}}}) \}$$ where $X$ is ${\textsf{Var}}' \cup ({\textsf{Var}}\setminus {\textsf{siv}}({{\varphi}_{\textsf{body}}}))$.

$P \gets \bot$

Geometrically, the convex hull ${\textit{hull}}({{\varphi}_{\textsf{body}}})$ is the smallest convex polyhedron which contains ${{\varphi}_{\textsf{body}}}$. Logically, it is a set of (in)equations such that (1) every (in)equation in ${\textit{hull}}({{\varphi}_{\textsf{body}}})$ is implied by ${{\varphi}_{\textsf{body}}}$, and (2) any linear (in)equation (over ${\textsf{Var}}\cup {\textsf{Var}}'$) which is implied by ${{\varphi}_{\textsf{body}}}$ is also implied by ${\textit{hull}}({{\varphi}_{\textsf{body}}})$. For example, ${\textit{hull}}({{\varphi}_{\textsf{body}}})$ for the loop above is: $$0 \leq \delta_x \land \delta_x \leq 1 \land 0 \leq \delta_y \land \delta_y \leq 1 \land \delta_x + \delta_y = 1$$

We note that the only variables which appear in the (in)equations in ${\textit{hull}}({{\varphi}_{\textsf{body}}})$ are (stratified) induction variables and difference variables. Thus, we may write any (in)equation in ${\textit{hull}}({{\varphi}_{\textsf{body}}})$ as $\vec{c}\vec{\delta}
\bowtie \vec{b}\vec{y} + d$ (where $\vec{\delta}$ is the vector of difference variables, $\vec{y}$ is the vector of stratified induction 