$\mathscr{K}_{{\shortrightarrow}}(P)$ is closed under arbitrary unions. Hence, the kernel can be simplified as follows: $$\mathscr{K}_{{\shortrightarrow}}(P) = \operatorname{Cl}_{\cap,\cup} (\{\operatorname{pre}^{\exists\exists} (\{C\})~|~
C\in P\} \cup \{\operatorname{post}^{\exists\exists} (\{B\})~|~
B\in P\}).$$ We therefore have that a block $B\in P$ is merged together with all the blocks $B'\in P$ such that for any block $A\in P$, $B \in \operatorname{pre}^{\exists\exists} (\{A\}) {\Leftrightarrow}B'  \in \operatorname{pre}^{\exists\exists} (\{A\})$ and $B \in \operatorname{post}^{\exists\exists} (\{A\}) {\Leftrightarrow}B'  \in \operatorname{post}^{\exists\exists} (\{A\})$. Thus, the thesis follows.

Reconsider the abstract transition system ${\mathcal{A}}$ in Section \[intro\] and let $P=\{[1],[2,3],[4,5],[6],[7],[8,9]\}$ be the underlying state partition. In this case, we have that $$\begin{array}{l}
\operatorname{img}(\operatorname{pre}^{\exists\exists}) = \operatorname{Cl}_{\cup} \big( \big\{ \{[1]\}, \{[2,3],[4,5]\}, \{[6],[7]\}\big\}\big),\\
\operatorname{img}(\operatorname{post}^{\exists\exists}) = \operatorname{Cl}_{\cup} \big(\big\{\{[2,3],[4,5]\}, \{[6],[7]\},\{[8,9]\}\big\}\big).
\end{array}$$ Hence, by Corollary \[kernel-part\], in the correctness kernel $\mathscr{K}_{{\shortrightarrow}}(P)$ the block $[2,3]$ is merged with $[4,5]$ while $[6]$ is merged with $[7]$. This therefore simplifies the partition $P$ to $P'' = \{[1], [2,3,4,5], [6,7], [8,9]\}$, that is, we obtain the abstract transition system ${\mathcal{A}}''$ in Section \[intro\].

Example Guided Abstraction Simplification {#egas}
=========================================

Let us discuss how correctness kernels give rise to an Example-Guided Abstraction Simplification (EGAS) paradigm in abstract transition systems.

Let us first recall some basic notions of CEGAR [@cgjlv00; @cgjlv03]. Consider an abstract transition system ${\mathcal{A}}=
\langle P, 