Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

\section{Appendix for Sect.~\ref{sect:preliminaries}}

\label{sect:app-preliminaries}

Equality axioms:

\[

 \begin{array}{rl}

\refl & \forall x . x = x \\

\symm & \forall x, y. (x = y \limp y = x )\\

\trans & \forall x , y , z . ( x = y \limp y = z \limp x = z ) \\

\subst_f & \forall \vec x , \vec y . (\vec x = \vec y \limp f(\vec x) = f(\vec y) ) \\

\subst_P & \forall \vec x , \vec y. (\vec x = \vec y \limp P(\vec x) \limp P(\vec y)  )

 \end{array}

 \]