node\[name=3\] [[$\mathbb{Z}_{\leq 0}$]{}]{}; (1,1) node\[name=4\] [[$\mathbb{Z}_{\geq 0}$]{}]{}; (0,2) node\[name=5\] [[$\mathbb{Z}$]{}]{};

(-2.5,1) node [[$A_1$]{}]{};

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

(5,1) node [[$A_2$]{}]{};

(4,0) node\[name=2\] [[$\mathbb{Z}_{\geq 0}$]{}]{}; (4,2) node\[name=5\] [[$\mathbb{Z}$]{}]{};

\(2) – (5);

Recall that in abstract interpretation the best correct approximation of a semantic function $f$ on an abstract domain $A$ that is defined through abstraction/concretization maps $\alpha$/$\gamma$ is given by $f^A {\triangleq}\alpha \circ f \circ \gamma$. Consider a simple operation of increment $x$++ on an integer variable $x$. In this case, the best correct approximations on $A_1$ and $A_2$ are as follows: $$\begin{gathered}
\text{++}^{A_1} = \{0 \mapsto \mathbb{Z}_{\geq 0},\: 
\mathbb{Z}_{\leq 0} \mapsto \mathbb{Z},\: 
\mathbb{Z}_{\geq 0} \mapsto \mathbb{Z}_{\geq 0},\: 
\mathbb{Z} \mapsto \mathbb{Z}\},\\[-2.5pt]
\text{++}^{A_2} = \{
\mathbb{Z}_{\geq 0} \mapsto \mathbb{Z}_{\geq 0},\: 
\mathbb{Z} \mapsto \mathbb{Z}\}.\end{gathered}$$ We observe that the best correct approximations of $\text{++}$ in $A_1$ and $A_2$ encode the same function, meaning that the approximations of $\text{++}$ in $A_1$ and $A_2$ are equivalent, the latter being clearly simpler. In fact, we have that $\gamma_{A_1} \circ \text{++}^{A_1} \circ \alpha_{A_1}$ and $\gamma_{A_2} \circ \text{++}^{A_2} \circ \alpha_{A_2}$ are exactly the same function on $\wp(\mathbb{Z})$. In other terms, the abstract domain $A_1$ contains some “irrelevant” abstract values for approximating 