Index: CSL17/tech-report/arithmetic.tex
===================================================================
--- CSL17/tech-report/arithmetic.tex	(revision 262)
+++ CSL17/tech-report/arithmetic.tex	(revision 263)
@@ -33,7 +33,7 @@
 	\item $\forall x^\safe, y^\safe . \safe(x+y)$
 	\item $\forall u^\normal, x^\safe . \safe(u\times x) $
 	\item $\forall u^\normal , v^\normal . \safe (u \smsh v)$
-	\item $\forall u^\normal .\safe(|x|)$
+	\item $\forall u^\normal .\safe(|u|)$
 \end{enumerate}
 %\[
 %\begin{array}{l}
@@ -50,18 +50,20 @@
 %\forall u^\normal .\safe(|x|)
 %\end{array}
 %\]
+\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. }
+
 Notice in particular that we have $\normal \subseteq \safe$.
 %
 Apart from these, the remaining $\basic$ axioms mimic those of Buss in \cite{Buss86book}:
 \begin{enumerate}[(1)]
-	\item $\forall x^{\safe}, y^{\safe}.  (y\leq x\cimp  y \leq \succ{} x) $
-	\item $\forall x^{\safe}. x \neq \succ{} x$
-	\item $\forall x^{\safe}.0 \leq x$
-	\item $\forall x^{\safe}, y^{\safe}. ((x\leq y \cand x \neq y) \ciff \succ{} x \leq y) $
+	\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}. (x\neq 0 \cimp \succ{0}x \neq 0)$
-	\item $\forall x^{\safe}, y^{\safe}. (y\leq x \cor x \leq y)$
+	\item $\forall x^{\safe}, y^{\safe}. (y\leq x \cor x \leq y)$  \label{axiom6}
 	\item $\forall x^{\safe}, y^{\safe}. ((x\leq y \cand y\leq x )\cimp x=y)$
-	\item $\forall x^{\safe}, y^{\safe}, z^{\safe}. ((x\leq y \cand y\leq z) \cimp x\leq z)$
+	\item $\forall x^{\safe}, y^{\safe}, z^{\safe}. ((x\leq y \cand y\leq z) \cimp x\leq z)$ \label{axiom<=transitivity}
 	\item $|0|=0$
 	\item $\forall x^{\safe}, y^{\safe}.( x\neq 0 \cimp  (|\succ{0}x|=\succ{}( |x|) \cand |\succ{1}x|= \succ{}(|x|))) $
 	\item $|\succ{}0|=\succ{} 0$
@@ -74,15 +76,15 @@
 	\item $\forall x^{\normal}, u^{\normal}, v^{\normal}, y^{\normal}.      (|x|= |u|+  |v| \cimp x\smsh y=(u\smsh y)\cdot (v\smsh y))$
 	\item $\forall x^{\safe}, y^{\safe}.      x\leq x+y$
 	\item $\forall x^{\safe}, y^{\safe}.    (  ( x\leq y \cand x\neq y) \cimp( \succ{}(\succ{0}x) \leq \succ{0}y \cand  \succ{}(\succ{0}x) \neq \succ{0}y))$
-	\item $\forall x^{\safe}, y^{\safe}.     x+y=y+x$
+	\item $\forall x^{\safe}, y^{\safe}.     x+y=y+x$ \label{axiom21}
 	\item $\forall x^{\safe}.       x+0=x$
 	\item $\forall x^{\safe}, y^{\safe}.       x+\succ{}y=\succ{}(x+y)$
 	\item $\forall x^{\safe}, y^{\safe}, z^{\safe}.      (x+y)+z=x+(y+z)$
 	\item $\forall x^{\safe}, y^{\safe}, z^{\safe}. (    x+y \leq x+z \ciff y\leq z)$
 	\item $\forall x^{\safe}       0\cdot x =0$
-	\item $\forall x^{\safe}, y^{\normal}.  x\cdot(\succ{}y)=(x\cdot y)+x$
+	\item $\forall x^{\normal}, y^{\safe}.  x\cdot(\succ{}y)=(x\cdot y)+x$  \label{axiom27}
 	\item $\forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x$
-	\item $\forall x^{\normal}, y^{\safe}, z^{\safe}.  x\cdot(y+z)=(x\cdot y)+(x\cdot z)$
+	\item $\forall x^{\normal}, y^{\safe}, z^{\safe}.  x\cdot(y+z)=(x\cdot y)+(x\cdot z)$ \label{axiom29}
 	\item $\forall x^{\normal}, y^{\safe}, z^{\safe}.      (x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \ciff y\leq z))$
 	\item $\forall x^{\normal}  .     (x\neq 0 \cimp  |x|=\succ{}(\hlf{x}))$
 	\item $\forall x^{\safe}, y^{\safe}.   (  x= \hlf{y} \ciff (\succ{0}x=y \cor \succ{}(\succ{0}x)=y))$
@@ -221,13 +223,27 @@
 	\begin{array}{l}
 	\forall x^\safe . 0 \neq \succ{} (x) \\
 	\forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) \\
-	\forall x^\safe . (x = 0 \cor \exists y^\safe.\  x = \succ{} y   )  \\
-	\forall u^\normal ,x^\safe . u \succ{} x = u + ux
+	%\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
 	\end{array}
 	\]
 	\todo{Proof: Patrick? The final two should require PIND.}
-\end{example}
-
+	
+	\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}
 It is often useful for us to work with \emph{length-induction}, which is equivalent to polynomial induction and well known from bounded arithmetic:
 \begin{proposition}
 	[Length induction]
