Index: CSL17/tech-report/arithmetic.tex
===================================================================
--- CSL17/tech-report/arithmetic.tex	(revision 265)
+++ CSL17/tech-report/arithmetic.tex	(revision 266)
@@ -77,13 +77,14 @@
 	\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$ \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}.       x+0=x$                    \label{axiom22}
+	\item $\forall x^{\safe}, y^{\safe}.       x+\succ{}y=\succ{}(x+y)$ \label{axiom23}
 	\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^{\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}.  x\cdot(\succ{}y)=(x\cdot y)+x$  \label{axiom27}  %% version with alternative sorting
+	\item $\forall x^{\safe}, y^{\normal}.  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)$ \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}))$
@@ -225,8 +226,9 @@
 	\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 . (u = 0 \cor \exists v^\normal.\  u = \succ{} v  )  \\
+	%\forall x^\safe . (x = 0 \cor \exists y^\safe.\  x = \succ{} y   )  \\        %% version 1: Anupam
+	%\forall u^\normal . (u = 0 \cor \exists v^\normal.\  u = \succ{} v  )  %%  version 2: Patrick
+	\forall u^\normal . (u = 0 \cor \exists y^\safe.  u = \succ{} v  )  \\        %% version 3: after discussion
 	\forall u^\normal ,x^\safe . u \cdot \succ{} x = u + ux
 	\end{array}
 	\]
@@ -242,10 +244,14 @@
 \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.
+ \item For statement 3 we proceed by induction on $u$ on the formula %$A(u)= (u=0) \cup \exists^{\normal} v. u=\succ{} v$.
+ $A(u)= (u=0) \cup \exists^{\safe} v. u=\succ{} v$. Note that this formula is in $\Sigma^{\safe}_1$, so we can do induction on it in  $\arith^1$. 
+   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 $y$ such that $u=\succ{} y$. In this latter case we have $\succ{0} u=2\cdot(\succ{} y)=2 v +2$ (by axiom \ref{axiom29}), hence have $\succ{0} u=\succ{} (\succ{} (2\cdot y))$, 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}.
+\item Statement 4:
+%For statement 4 we just use axiom  \ref{axiom27} followed by the $+$ commutativity axiom \ref{axiom21}.
+ Let $u$ be in $\normal$ and $x$ in $\safe$, and try to prove $u\succ{} x=u+ux$. We have $\succ{} x=x+1$ by axioms \ref{axiom23} and \ref{axiom22} , so $u\succ{} x= u(x+1)$, so from axiom \ref{axiom29} we deduce $ u\succ{} x= u(x+1)=ux+u$, and by axiom \ref{axiom21} we conclude that $ u\succ{} x=u+ux$.
 \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:
