Program equivalence

$latex P$ is valid precisely when $latex \neg P$ is not satisfiable. In other words, if it is not possible to make $latex \neg P$ false, then $latex P$ is valid.

To make program equivalence checking with $latex P$ and $latex Q$ ($latex P \leftrightarrow Q$), you need to check $latex \neg (P \to Q)$ and $latex \neg (Q \to P)$ both not satisfiable.

$latex \neg (P \to Q)$ is $latex P \wedge \neg Q$, and let's say $latex P$ and $latex Q$ are decomposed into two symbolic summary elements such as $latex P_1 \lor P_2 $ and $latex Q_1 \lor Q_2 $. $latex P \wedge \neg Q$ becomes unsatisfiable only when $latex (P_1 = Q_1) \wedge (P_2 = Q_2)$.