Example 4.3 
We are interested to synthesize a loop implementing Euclidean division over
\(x,y\in \mathbb {K}\) . Following the problem specification of [1]}for
\(x,y\in \mathbb {K}\)  we want to compute \(q,r\in \mathbb {K}\)  such that \(x = yq + r\)  holds, a
synthesized loop performing Euclidean division satisfies the polynomial
invariant \({p = \bar{x} - \bar{y}q - r = 0}\) , where \(\bar{x}\)  and \(\bar{y}\) 
denote the initial values of \(x\)  and \(y\)  before the loop. It is clear, that
the synthesized loop should be parameterized with respect to \(\bar{x}\)  and
\(\bar{y}\) .
With this setting, input to our synthesis approach is the invariant \({p =\bar{x} - \bar{y}q - r = 0}\) . A recurrence system performing Euclidean
division and therefore satisfying the algebraic relation \(\bar{x} - \bar{y}q -r\)  is then given by \(X_{n+1} = BX_n\)  and \(X_0 = A\)  with a corresponding closed
form system \(X_n = A + Cn\)  where:
\(X_n = \begin{pmatrix}x(n) \\ r(n) \\ q(n) \\ y(n) \\ t(n)\end{pmatrix}\quad A = \begin{pmatrix}\bar{x} \\ \bar{x} \\ 0 \\ \bar{y} \\ 1\end{pmatrix}\quad B =\begin{pmatrix}1 & 0 & 0 & 0 & 0 \\0 & 1 & 0 & -1 & 0 \\0 & 0 & 1 & 0 & 1 \\0 & 0 & 0 & 1 & 0 \\0 & 0 & 0 & 0 & 1\end{pmatrix}\quad C = \begin{pmatrix} 0 \\ -\bar{y} \\ 1 \\ 0 \\ 0 \end{pmatrix}\) 
