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

%\item Predecessor $p$:   $\forall^{\safe} x, \exists^{\safe} y. (x=\succ{0} y \cor x=\succ{1} y \cor (x=\epsilon \cand y= \epsilon)) .$

\item Conditional $C$: 

$$\begin{array}{ll}

                                                                                                   & \cor( \exists^{\safe}z.(x=\succ{0}z) \cand (y=y_0))\\

                                                                                                   & \cor( \exists^{\safe}z.(x=\succ{1}z) \cand (y=y_1)))\

\end{array}