with equality guard has the form $$\label{equ:mpp}
\textsc{ while} \quad (G({\pmb{x}})=0)\quad
  \left\{
   \begin{aligned}
   &{\pmb{x}}\coloneqq {\pmb{A}}_{1}({\pmb{x}});\\
   \parallel\quad &{\pmb{x}}\coloneqq {\pmb{A}}_{2}({\pmb{x}}); \\
   &\vdots\\
   \parallel\quad &{\pmb{x}}\coloneqq {\pmb{A}}_{l-1}({\pmb{x}}); \\
   \parallel\quad &{\pmb{x}}\coloneqq {\pmb{A}}_{l}({\pmb{x}});
   \end{aligned}\right\},$$ where

1.  ${\pmb{x}}\in {\mathbb{K}}^d$ denotes the vector of program variables;

2.  $ G\in {\mathbb{K}}[{\pmb{x}}]$ is a polynomial and $G({{\pmb{x}}})=0$ is the equality typed loop guard;

3.  $ {\pmb{A}}_{i}\in {\mathbb{K}}^d[{\pmb{x}}]$ ($ 1\leq i\leq l$) are vectors of polynomials, describing the transformations on program variables in the loop body;

4.  $``\parallel"$ interprets as a nondeterministic choice between the $l$ transformations.

<!-- -->

1.  The loop guard of MPP (\[equ:mpp\]) can be extended to a more general form $\bigvee_{i=1}^M\bigwedge_{j=1}^{N_i} G_{ij}({\pmb{x}})=0$. However, it is essential to assume that inequalities will never occur in guards, otherwise the termination problem will become undecidable, even not semi-decidable [@bradley:polynomial].

2.  The initial value of ${\pmb{x}}$ is not specified here, and assume it is taken from $\Bbb{K}^{d}$. If the input ${\pmb{x}}$ is subject to semi-algebraic constraints, our decidability result still holds according to [@Tarski51].

\[exm1\] Consider the following MPP (named as `liu1`): $$\textsc{while} \quad (x^2+1-y=0)\quad
  \left\{
   \begin{aligned}
   (x,y) &\coloneqq (x,x^2y);  \\
   \parallel\quad (x,y) &\coloneqq (-x,y);  \\
    \end{aligned}
   \right\}.$$ We have $d=2$, $G(x,y)=x^2-y+1$, ${\pmb{A}}_1(x,y)=(x,x^2y)$ and ${\pmb{A}}_2(x,y)=(-x,y)$.

\[exa:quantum\] A nondeterministic quantum program [@LY14] 