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

	\item $\forall u^\normal .\safe(|u|)$

\patrick{Actually I guess that we could replace the last one by $\forall x^\normal .\safe(|x|)$, as $|x|$ has smaller size as $x$? But I am not sure this would be needed anywhere. }

	\item $\forall x^{\safe}, y^{\safe}.  (y\leq x\cimp  y \leq \succ{} x) $ \label{axiom1}

	\item $\forall x^{\safe}. x \neq \succ{} x$       \label{axiom2}

	\item $\forall x^{\safe}.0 \leq x$       \label{axiom3}

	\item $\forall x^{\safe}, y^{\safe}. ((x\leq y \cand x \neq y) \ciff \succ{} x \leq y) $ \label{axiom4}

	\item $\forall x^{\safe}, y^{\safe}. (y\leq x \cor x \leq y)$  \label{axiom6}

	\item $\forall x^{\safe}, y^{\safe}, z^{\safe}. ((x\leq y \cand y\leq z) \cimp x\leq z)$ \label{axiom<=transitivity}

	\item $\forall x^{\safe}, y^{\safe}.     x+y=y+x$ \label{axiom21}

	\item $\forall x^{\normal}, y^{\safe}.  x\cdot(\succ{}y)=(x\cdot y)+x$  \label{axiom27}

	\item $\forall x^{\normal}, y^{\safe}, z^{\safe}.  x\cdot(y+z)=(x\cdot y)+(x\cdot z)$ \label{axiom29}

	%\forall x^\safe . (x = 0 \cor \exists y^\safe.\  x = \succ{} y   )  \\

	\forall u^\normal . (u = 0 \cor \exists v^\normal.\  u = \succ{} v  )  \\

	\forall u^\normal ,x^\safe . u \cdot \succ{} x = u + ux

	\patrick{Actually statement 4 is nearly trivial from axiom 27 (for which I corrected the sorts). Maybe you meant something else?

	For statement 3 I replaced the quantifications $\safe$ by $\normal$, otherwise I don't know how to prove it. But I think we need the stronger statement with $\safe$, so probably we should add it as an additional axiom.}

	\end{example}

\begin{proof}

\begin{itemize}

 \item For the first statement, assume  $\succ{} (x)=0$ in order to derive a contradiction. From axiom \ref{axiom1} we deduce $x \leq x$, and so by transitivity (axiom \ref{axiom<=transitivity}) we have $x\leq 0$. So axiom \ref{axiom3} gives us $x=0$, and so $x=\succ{} (x)$. Finally with axiom  \ref{axiom2} we conclude with a contradiction.

 \item For statement 2 assume $\succ{} x= \succ{} y$ and, in view of a contradiction, $x\neq y$. Let us apply axiom \ref{axiom6} and assume we are in the case where $x\leq y$ (the case $y\leq x$ is symmetric). By axiom \ref{axiom4}, using the assumption $x\neq y$ we deduce $\succ{} x \leq y$. So as $\succ{} x = \succ{} y$ we can derive that $\succ{} y \leq y$. So by using axiom \ref{axiom1} we obtain that $\succ{} y = y$, hence axiom \ref{axiom2} gives us a contradiction, so we are done.

 \item For statement 3 we proceed by induction on $u$ on the formula $A(u)= (u=0) \cup \exists^{\normal} v. u=\succ{} v$. The formula $A(0)$ obviously holds. Let us assume $A(u)$ and prove $A(\succ{0} u)$ (the case for $A(\succ{1} u)$ will be similar).  By $A(u)$ we deduce that either $u=0$, in which case we also have $\succ{0} u=0$, hence  $A(\succ{0} u)$ also holds, or there is a $v$ such that $u=\succ{} v$. In this latter case we have $\succ{0} u=2\cdot(\succ{} v)=2 v +2$ (by axiom \ref{axiom29}), hence have $\succ{0} u=\succ{} (\succ{} (2\cdot v))$, and so $A(\succ{0} u)$ holds.

 By induction we conclude that $\forall^{\normal} u. A(u)$ holds.

\item For statement 4 we just use axiom  \ref{axiom27} followed by the $+$ commutativity axiom \ref{axiom21}.

\end{itemize}

\end{proof}