Index: CSL17/tech-report/arithmetic.tex
===================================================================
--- CSL17/tech-report/arithmetic.tex	(revision 255)
+++ CSL17/tech-report/arithmetic.tex	(revision 256)
@@ -45,8 +45,68 @@
 
 Apart from these, the remaining $\basic$ axioms mimic those of Buss in \cite{Buss86book}:
 
-\input{appendix-arithmetic}
+$$
+%\begin{equation}
+\begin{array}{l}
+\forall x^{\safe}, y^{\safe}.  (y\leq x\cimp  y \leq \succ{} x) \\
+\forall x^{\safe}. x \neq \succ{} x\\
+\forall x^{\safe}.0 \leq x\\
+\forall x^{\safe}, y^{\safe}. ((x\leq y \cand x \neq y) \ciff \succ{} x \leq y) \\
+\forall x^{\safe}. (x\neq 0 \cimp \succ{0}x \neq 0)\\
+\forall x^{\safe}, y^{\safe}. (y\leq x \cor x \leq y)\\
+\forall x^{\safe}, y^{\safe}. ((x\leq y \cand y\leq x )\cimp x=y)\\
+\forall x^{\safe}, y^{\safe}, z^{\safe}. ((x\leq y \cand y\leq z) \cimp x\leq z)\\
+|0|=0\\
+\forall x^{\safe}, y^{\safe}.( x\neq 0 \cimp  (|\succ{0}x|=\succ{}( |x|) \cand |\succ{1}x|= \succ{}(|x|))) \\
+|\succ{}0|=\succ{} 0\\
+\forall x^{\safe}, y^{\safe}.   (x\leq y \cimp   |x|\leq  |y|)\\
+\forall x^{\normal}, y^{\normal}.    |x\smsh y|=\succ{}( |x|\cdot  |y|)\\
+\forall y^{\normal}.    0 \smsh y=\succ{} 0\\
+\forall x^{\normal}.    (x\neq 0 \cimp (1 \smsh(\succ{0}x)=\succ{0}(1\smsh x) \cand 1 \smsh(\succ{1}x)=\succ{0}(1\smsh x)))\\
+\forall x^{\normal}, y^{\normal}.    x \smsh y = y \smsh x\\
+\forall x^{\normal}, y^{\normal}, z^{\normal}. (   |x|= |y| \cimp x\smsh z = y\smsh z)\\
+\forall x^{\normal}, u^{\normal}, v^{\normal}, y^{\normal}.      (|x|= |u|+  |v| \cimp x\smsh y=(u\smsh y)\cdot (v\smsh y))\\
+\forall x^{\safe}, y^{\safe}.      x\leq x+y\\
+\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))\\
+\forall x^{\safe}, y^{\safe}.     x+y=y+x\\
+\forall x^{\safe}.       x+0=x\\
+\forall x^{\safe}, y^{\safe}.       x+\succ{}y=\succ{}(x+y)\\
+\forall x^{\safe}, y^{\safe}, z^{\safe}.      (x+y)+z=x+(y+z)\\
+\forall x^{\safe}, y^{\safe}, z^{\safe}. (    x+y \leq x+z \ciff y\leq z)\\
+\forall x^{\safe}       0\cdot x =0\\
+\forall x^{\normal}, y^{\safe}.  x\cdot(\succ{}y)=(x\cdot y)+x\\
+\forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x\\
+\forall x^{\normal}, y^{\safe}, z^{\safe}.  x\cdot(y+z)=(x\cdot y)+(x\cdot z)\\
+\forall x^{\normal}, y^{\safe}, z^{\safe}.      (x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \ciff y\leq z))\\
+\forall x^{\normal}  .     (x\neq 0 \cimp  |x|=\succ{}(\hlf{x}))\\
+\forall x^{\safe}, y^{\safe}.   (  x= \hlf{y} \ciff (\succ{0}x=y \cor \succ{}(\succ{0}x)=y))
+\end{array}
+%\end{equation}
+$$
 
+
+
+
+
+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]
+	The axiom schema of formulae,
+	\begin{equation}
+	\label{eqn:lind}
+	( A(0) \cand \forall x^\normal . (A(x) \cimp A(\succ{} x)) ) \cimp \forall x^\safe. A(|x|)
+	\end{equation}
+	for formulae $A \in \Sigma^\safe_i$
+	is equivalent to $\cpind{\Sigma^\safe_i}$.
+\end{proposition}
+\begin{proof}
+	Suppose we have $A(0)$ and $A(a) \cimp A(\succ{} a)$ for each $a \in \normal$.
+	Then, by $\basic$, we have that $A(|a|) \cimp A(|2a|)$ and $A(|a|) \cimp A(|2a+1|)$ for each $a \in \normal$, whence we may conclude $\forall x. A(|x|)$ by polynomial induction on $A(|x|)$.
+\end{proof}
+
+Let us refer to the axiom schema in \eqref{eqn:lind} as $\clind{\Xi}$, when $A \in \mathcal \Xi$.
+We will freely use this in place of polynomial induction whenever it is convenient.
+
 %\begin{definition}
 %	[Basic theory]
 %	The theory $\basic$ consists of the axioms from Appendix \ref{appendix:arithmetic}.
Index: CSL17/tech-report/appendix-arithmetic.tex
===================================================================
--- CSL17/tech-report/appendix-arithmetic.tex	(revision 255)
+++ CSL17/tech-report/appendix-arithmetic.tex	(revision 256)
@@ -4,64 +4,3 @@
 %%$\succ{0}(x)$ stand for $2\cdot x$ and $\succ{1}(x)$ stand for $\succ{}(2\cdot x)$,
 % 
 % 
-$$
-%\begin{equation}
-\begin{array}{l}
- \forall x^{\safe}, y^{\safe}.  (y\leq x\cimp  y \leq \succ{} x) \\
-\forall x^{\safe}. x \neq \succ{} x\\
- \forall x^{\safe}.0 \leq x\\
- \forall x^{\safe}, y^{\safe}. ((x\leq y \cand x \neq y) \ciff \succ{} x \leq y) \\
-\forall x^{\safe}. (x\neq 0 \cimp \succ{0}x \neq 0)\\
-\forall x^{\safe}, y^{\safe}. (y\leq x \cor x \leq y)\\
-\forall x^{\safe}, y^{\safe}. ((x\leq y \cand y\leq x )\cimp x=y)\\
-\forall x^{\safe}, y^{\safe}, z^{\safe}. ((x\leq y \cand y\leq z) \cimp x\leq z)\\
-  |0|=0\\
-  \forall x^{\safe}, y^{\safe}.( x\neq 0 \cimp  (|\succ{0}x|=\succ{}( |x|) \cand |\succ{1}x|= \succ{}(|x|))) \\
-   |\succ{}0|=\succ{} 0\\
-\forall x^{\safe}, y^{\safe}.   (x\leq y \cimp   |x|\leq  |y|)\\
-\forall x^{\normal}, y^{\normal}.    |x\smsh y|=\succ{}( |x|\cdot  |y|)\\
-\forall y^{\normal}.    0 \smsh y=\succ{} 0\\
-\forall x^{\normal}.    (x\neq 0 \cimp (1 \smsh(\succ{0}x)=\succ{0}(1\smsh x) \cand 1 \smsh(\succ{1}x)=\succ{0}(1\smsh x)))\\
-\forall x^{\normal}, y^{\normal}.    x \smsh y = y \smsh x\\
-  \forall x^{\normal}, y^{\normal}, z^{\normal}. (   |x|= |y| \cimp x\smsh z = y\smsh z)\\
-  \forall x^{\normal}, u^{\normal}, v^{\normal}, y^{\normal}.      (|x|= |u|+  |v| \cimp x\smsh y=(u\smsh y)\cdot (v\smsh y))\\
-  \forall x^{\safe}, y^{\safe}.      x\leq x+y\\
- \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))\\
-   \forall x^{\safe}, y^{\safe}.     x+y=y+x\\
- \forall x^{\safe}.       x+0=x\\
- \forall x^{\safe}, y^{\safe}.       x+\succ{}y=\succ{}(x+y)\\
-  \forall x^{\safe}, y^{\safe}, z^{\safe}.      (x+y)+z=x+(y+z)\\
-   \forall x^{\safe}, y^{\safe}, z^{\safe}. (    x+y \leq x+z \ciff y\leq z)\\
- \forall x^{\safe}       0\cdot x =0\\
-      \forall x^{\normal}, y^{\safe}.  x\cdot(\succ{}y)=(x\cdot y)+x\\
-       \forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x\\
-      \forall x^{\normal}, y^{\safe}, z^{\safe}.  x\cdot(y+z)=(x\cdot y)+(x\cdot z)\\
-  \forall x^{\normal}, y^{\safe}, z^{\safe}.      (x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \ciff y\leq z))\\
- \forall x^{\normal}  .     (x\neq 0 \cimp  |x|=\succ{}(\hlf{x}))\\
-   \forall x^{\safe}, y^{\safe}.   (  x= \hlf{y} \ciff (\succ{0}x=y \cor \succ{}(\succ{0}x)=y))
- \end{array}
-%\end{equation}
-$$
-
-
-
-
-%
-%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]
-%	The axiom schema of formulae,
-%	\begin{equation}
-%	\label{eqn:lind}
-%	( A(0) \cand \forall x^\normal . (A(x) \cimp A(\succ{} x)) ) \cimp \forall x^\safe. A(|x|)
-%	\end{equation}
-%	for formulae $A \in \Sigma^\safe_i$
-%	is equivalent to $\cpind{\Sigma^\safe_i}$.
-%\end{proposition}
-%\begin{proof}
-%	Suppose we have $A(0)$ and $A(a) \cimp A(\succ{} a)$ for each $a \in \normal$.
-%	Then, by $\basic$, we have that $A(|a|) \cimp A(|2a|)$ and $A(|a|) \cimp A(|2a+1|)$ for each $a \in \normal$, whence we may conclude $\forall x. A(|x|)$ by polynomial induction on $A(|x|)$.
-%\end{proof}
-%
-%Let us refer to the axiom schema in \eqref{eqn:lind} as $\clind{\mathcal C}$, when $A \in \mathcal C$.
-%We will freely use this in place of polynomial induction whenever it is convenient.
\ No newline at end of file
