remove further abstract elements otherwise we do not retain the same b.c.a. as $\operatorname{Sign}$. For example, this means that $\operatorname{Sign}$-based analyses of programs like $$x := k;
\textbf{while}~\text{condition}~ \textbf{do}
~x := x*x;$$ can be carried out by using the simpler domain $\operatorname{Sign}\smallsetminus
\{\mathbb{Z}_{< 0}, \mathbb{Z}_{\leq 0}\}$, yet providing the same input/output abstract behavior.

It is worth remarking that in Theorem \[kernel\] the hypothesis of continuity is crucial for the existence of correctness kernels and this is shown by the following example.

\[esempio1\] Let us consider as concrete domain $C$ the $\omega + 2$ ordinal, i.e., $C \triangleq \{ x\in \mathit{Ord}~|~ x
  < \omega\} \cup$, and let $f:C{\rightarrow}C$ be defined as follows: $$f(x) {\triangleq}\left\{
    \begin{array}{ll}
    \omega & \mbox{ if $x<\omega$;} \\
    \omega+1 &\mbox{ otherwise.}
    \end{array}
    \right.$$ Let $\mu\in \operatorname{uco}(C)$ be the identity $\lambda x.x$ uco, so that $\mu {\circ}f {\circ}\mu = f$. For any $k\geq 0$, consider $\rho_k\in \operatorname{uco}(C)$ defined as $\ok{\rho_k {\triangleq}C\smallsetminus [0,k[}$ and observe that for any $k$, we have that $\rho_k {\circ}f {\circ}\rho_k = f = \mu {\circ}f {\circ}\mu$. However, it turns out that $\sqcup_{k\geq 0} \rho_k = \cap_{k\geq 0} 
\operatorname{img}(\rho_k) =
\{\omega, \omega +1\}$. Hence, $(\sqcup_{k\geq 0} \rho_k) {\circ}f {\circ}(\sqcup_{k\geq 0} \rho_k) = \lambda x.\omega +1\neq \mu 