$f\in F$, $\ok{f^A = f^B}$. Hence, given $A\in \operatorname{Abs}(C)$ and by defining $$A_{s} \triangleq \sqcup \{B \in \operatorname{Abs}(C)~|~ F^B = F^A\}$$ the question is whether $F^{A_{s}} = F^A$ holds or not. This leads us to the following notion of correctness kernel.

Given $F\subseteq C{\mbox{\raisebox{0ex}[1ex][1ex]{$
  \mathrel{\mathop{
\hspace*{1pt}\longrightarrow\hspace*{1pt}}\limits^{\,_{\mbox{\tiny
\hspace*{-2.2pt}}}}}$}}} C$ define: $\mathscr{K}_F: \operatorname{Abs}(C) \rightarrow \operatorname{Abs}(C)$ as $$\mathscr{K}_F(A) \triangleq \sqcup \{ B \in \operatorname{Abs}(C) ~|~ F^B = F^A\}.$$ If $F^{\mathscr{K}_F(A)} = F^A$ then $\mathscr{K}_F(A)$ is called the *correctness kernel* of $A$ for $F$.

It is worth remarking that the dual question on the existence of the *most concrete domain* that induces the same best correct approximation of $f$ as $A$ has a negative answer, as shown by the following simple example.

\[esempio2\] Consider the lattice $C$ depicted below.

(0,0) node\[name=1\] [$1$]{}; (0,1) node\[name=2\] [$2$]{}; (-1,2) node\[name=3\] [$3$]{}; (1,2) node\[name=4\] [$4$]{}; (0,3) node\[name=5\] [$5$]{};

\(1) – (2); (2) – (3); (2) – (4); (3) – (5); (4) – (5);

Let us also consider the monotonic function $f:C\rightarrow C$ defined as $f\triangleq \{1\mapsto 1,\, 2\mapsto 1,\, 3\mapsto 5,\, 4\mapsto 5,\, 5\mapsto 5\}$ and the abstraction $\mu \in \operatorname{uco}(C)$ whose image is $\mu \triangleq \{1,5\}$. Let us observe that $\mu{\circ}f {\circ}\mu = \{1\mapsto 1,\, 2\mapsto 5,\, 