the recurrence equations shown to the right. It then computes closed forms for these recurrences, also shown to the right (where $x^{(k)}$ denotes the value that the variable $x$ takes on the $k$th iteration of the loop). Note that this table omits “uninteresting” recurrences (such as $q' = q + 0$) which indicate that a variable does not change in a loop. These closed forms are used to abstract the loop as follows:

$$\begin{aligned}
  \varphi_{\textsf{inner}}^{\ostar}&=  {\fbox{$\exists k. k \geq 0 \land r' = r - k \land t' = t - k \land {\mathit{stable}}(\{q, x, y\})$}}\\
  &= {\fbox{$r' = r + t' - t \land t' \leq t \land {\mathit{stable}}(\{q, x, y\})$}}\end{aligned}$$

We may use this summary $\varphi_{\textsf{inner}}^{\ostar}$ for the inner loop to compute a transition formula representing the body of the outer loop: $$\begin{aligned}
  \varphi_{\textsf{outer}} &= {\llbracket {\langle v_2,v_3 \rangle} \rrbracket} {\odot}{\llbracket {\langle v_3,v_4 \rangle} \rrbracket} {\odot}\varphi_{\textsf{inner}}^{\ostar}{\odot}{\llbracket {\langle v_4,v_7 \rangle} \rrbracket} {\odot}{\llbracket {\langle v_7,v_2 \rangle} \rrbracket}\\
  &= {\fbox{$q' = q + 1 \land r' = r + t' - y \land t' = 0 \land r \geq y \land {\mathit{stable}}(\{x, y\})$}} \end{aligned}$$

We then apply the iteration operator to compute a transition formula for the outer loop. The recurrences 