the corresponding abstract functions $\operatorname{pre}^{\exists\exists} = \alpha_P \circ \operatorname{pre}\circ \gamma_P$ and $\operatorname{post}^{\exists\exists} = \alpha_P \circ \operatorname{post}\circ \gamma_P$. Then, the correctness kernel of the abstraction $\wp(P)$ for the concrete predecessor/successor $\{\operatorname{pre},\operatorname{post}\}$, that we denote simply by $\mathscr{K}_{{\shortrightarrow}}(P)$ (by Theorem \[kernel\], this clearly exists since $\operatorname{pre}$ and $\operatorname{post}$ are additive functions), provides a simplification of the abstract domain $\wp(P)$ that preserves the best correct approximations of predecessor and successor functions. This simplification $\mathscr{K}_{{\shortrightarrow}}(P)$ of the abstract state space $P$ works as follows:

\[kernel-part\] $\mathscr{K}_{{\shortrightarrow}}(P)$ merges two blocks $B_1,B_2\in P$ if and only if for any $A\in P$, $A {\shortrightarrow}^{\exists\exists} B_1 \:{\Leftrightarrow}\: A {\shortrightarrow}^{\exists\exists} B_2$ and $B_1 {\shortrightarrow}^{\exists\exists} A \:{\Leftrightarrow}\: B_2 {\shortrightarrow}^{\exists\exists} A$.

By Theorem \[kernel\], we have that the kernel $\mathscr{K}_{{\shortrightarrow}}(P)$ of the abstraction $\wp(P)\in \operatorname{Abs}(\wp(\Sigma))$ for $\operatorname{pre}$ and $\operatorname{post}$ is as follows: $$\begin{gathered}
\mathscr{K}_{{\shortrightarrow}}(P) = \operatorname{Cl}_{\cap} 
\Big(\operatorname{img}(\operatorname{pre}^{\exists\exists}) \cup \textstyle \bigcup_{\mathcal{C}\in \operatorname{img}(\operatorname{pre}^{\exists\exists})}
\cup \{\mathcal{B}\in \wp(P)~|~ \operatorname{pre}^{\exists\exists}(\mathcal{C}) = \mathcal{B}\}\\
\bigcup 
\operatorname{img}(\operatorname{post}^{\exists\exists}) \cup \textstyle \bigcup_{\mathcal{B}\in \operatorname{img}(\operatorname{post}^{\exists\exists})}
\cup \{\mathcal{C}\in \wp(P)~|~ \operatorname{post}^{\exists\exists}(\mathcal{B}) = \mathcal{C}\}
\Big).\end{gathered}$$ Let us observe that both b.c.a.’s $\operatorname{pre}_{\exists\exists}, \operatorname{post}_{\exists\exists}: \wp(P) {\rightarrow}\wp(P)$ are additive functions, so that for any $\mathcal{C}\in \operatorname{img}(\operatorname{pre}_{\exists\exists})$, $\cup \{\mathcal{B}\in \wp(P)~|~ \operatorname{pre}^{\exists\exists}(\mathcal{C}) = \mathcal{B}\} 
\in \operatorname{img}(\operatorname{pre}_{\exists\exists})$ and for any $\mathcal{B}\in \operatorname{img}(\operatorname{post}_{\exists\exists})$, $\cup \{\mathcal{C}\in \wp(P)~|~ \operatorname{post}^{\exists\exists}(\mathcal{B}) = \mathcal{C}\} 
\in \operatorname{img}(\operatorname{post}_{\exists\exists})$. Moreover, 