Index: CSL17/tech-report/completeness.tex
===================================================================
--- CSL17/tech-report/completeness.tex	(revision 266)
+++ CSL17/tech-report/completeness.tex	(revision 267)
@@ -6,69 +6,38 @@
 	\label{thm:completeness}
 	For every $\mubci{i-1}$ program $f(\vec u ; \vec x)$ (which is in $\fphi i$), there is a $\Sigma^{\safe}_i$ formula $A_f(\vec u, \vec x)$ such that $\arith^i$ proves $\forall^{\normal} \vec u, \forall^{\safe} \vec x, \exists^{\safe} ! y. A_f(\vec u , \vec x , y )$ and $\Nat \models \forall \vec u , \vec x. A_f(\vec u , \vec x , f(\vec u ; \vec x))$.
 \end{theorem}
-%\begin{proof}[Proof sketch]
-% The proof proceeds by induction on the construction of $\mubci{i-1}$ program $f(\vec u ; \vec x)$ to construct a suitable formula $A_f(\vec u, \vec x)$ .  The case of initial functions is easy, by using the formulas we gave in Sect. \ref{sect:graphsbasicfunctions}. The case of safe composition is also simple, and makes use of the $\rais$ rule and simply combines previously defined graphs by \emph{modus ponens} (or, equivalently, $\cut$) and logical steps. 
-% Naturally, the interesting cases are predicative recursion and predicative minimisation. 
-% 
-% For predicative recursion, the basic idea is to follow the classical simulation of primitive recursion in arithmetic, adapted to recursion on notation, by encoding the sequence of recursive calls as an integer $w$. 
-% The main technical difficulty is the representation of (de)coding functions $\beta (k, x)$ (``the $k$th element of the sequence $x$'') and $\langle x,y \rangle$ (``the pair $(x,y)$'').
-% For this we represent instead the length-bounded variants of these functions given towards the end of Sect.~\ref{sect:prelims}, relying on the bounded minimisation and polychecking results, Lemmas~\ref{lem:bounded-minimisation} and \ref{lem:polychecking}, to find appropriate length bounds.
-%%  which is sorted in a suitable way so that the formula $A_f$  is in the same class $\Sigma^{\safe}_i$ as $A_g$,  $A_{h_0}$ and $A_{h_1}$.  This can be obtained by defining  the predicate $\beta (k, w, y)$ with $k$ in $\normal$ and $w$, $y$ in $\safe$.
-%
-% 
-% For predicative minimisation, assume $f$ is defined as  $\succ 1 \mu x .( g(\vec u ; \vec x , x) =_2 0)$ (or $0$ if no such $x$ exists).
-%  By induction hypothesis we have a $\Sigma^{\safe}_{i-1}$ formula $A_g (\vec u , \vec x , x , y)$  satisfying the property. We then define $A_f(\vec u ; \vec x , z)$ as the following $\Sigma^{\safe}_{i}$ formula:
-%\[
-%\begin{array}{rl}
-%&\left(
-%z=0 \  \cand \ \forall x^\safe , y^\safe . (A_g (\vec u , \vec x , x, y) \cimp y=_2 1)
-%\right) \\
-%\cor & \left(
-%\begin{array}{ll}
-%z\neq 0 
-%& \cand\   \forall y^\safe . (A_g (\vec u , \vec x , p z , y) \cimp y=_2 0 ) \\
-%& \cand\ \forall x^\safe < p z . \forall y^\safe . (A_g (\vec u , \vec x , x , y) \cimp y=_2 1) 
-%\end{array}
-%\right)
-%\end{array}
-%\]
-%As for the analogous bounded arithmetic theory $S^i_2$ (\cite{Buss86book}, Thm 20, p. 58),  $\arith^i$ can prove a \emph{minimisation} principle for $\Sigma^\safe_{i-1}$ formulas, allowing us to extract the \emph{least} witness of a safe existential, which we apply to $\exists x^\safe , y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$. From here we are able to readily prove the totality of $A_f(\vec u ; \vec x , z)$, notably relying crucially on classical reasoning.
-%\end{proof}
+\begin{proof}[Proof sketch]
+ The proof proceeds by induction on the construction of $\mubci{i-1}$ program $f(\vec u ; \vec x)$ to construct a suitable formula $A_f(\vec u, \vec x)$ .  The case of initial functions is easy, by using the formulas we gave in Sect. \ref{sect:graphsbasicfunctions}. The case of safe composition is also simple, and makes use of the $\rais$ rule and simply combines previously defined graphs by \emph{modus ponens} (or, equivalently, $\cut$) and logical steps. 
+ Naturally, the interesting cases are predicative recursion and predicative minimisation. 
+ 
+ For predicative recursion, the basic idea is to follow the classical simulation of primitive recursion in arithmetic, adapted to recursion on notation, by encoding the sequence of recursive calls as an integer $w$. 
+ The main technical difficulty is the representation of (de)coding functions $\beta (k, x)$ (``the $k$th element of the sequence $x$'') and $\langle x,y \rangle$ (``the pair $(x,y)$'').
+ For this we represent instead the length-bounded variants of these functions given towards the end of Sect.~\ref{sect:prelims}, relying on the bounded minimisation and polychecking results, Lemmas~\ref{lem:bounded-minimisation} and \ref{lem:polychecking}, to find appropriate length bounds.
+%  which is sorted in a suitable way so that the formula $A_f$  is in the same class $\Sigma^{\safe}_i$ as $A_g$,  $A_{h_0}$ and $A_{h_1}$.  This can be obtained by defining  the predicate $\beta (k, w, y)$ with $k$ in $\normal$ and $w$, $y$ in $\safe$.
 
-\begin{proof}
-	We proceed by structural induction on a $\mubc^{i-1} $ program, dealing with each case in the proceeding paragraphs.
-	
-	The property is easily verified for the class of initial functions of  $\mubci{i-1}$: constant, projections, (binary) successors, predecessor, conditional, as already shown in Sect. \ref{sect:graphsbasicfunctions}. Now let us examine the three constructions: predicative minimisation, predicative (safe) recursion and composition. 
-	\paragraph*{Predicative minimisation}
-	Suppose $f(\vec u ; \vec x)$ is defined by predicative minimisation from $g$ (we then denote $f$ as as $\mu x^{+1} . g(\vec u ; \vec x , x) =_2 0$). 
-	By definition $g$ is in $\mubci{i-2}$, and so by the inductive hypothesis there is a $\Sigma^{\safe}_{i-1}$ formula $A_g (\vec u , \vec x , x , y)$ computing the graph of $g$ such that,
-	\[
-	\arith^i \proves \forall \vec u^\normal . \forall \vec x^\safe , x^\safe . \exists ! y^\safe . A_g(\vec u , \vec x , x , y)
-	\]
-	Let us define $A_f(\vec u ; \vec x , z)$ as:
-	\[
-	\begin{array}{rl}
-	&\left(
-	z=0 \  \cand \ \forall x^\safe , y^\safe . (A_g (\vec u , \vec x , x, y) \cimp y=_2 1)
-	\right) \\
-	\cor & \left(
-	\begin{array}{ll}
-	%z\neq 0
-	z=\succ{1} p z 
-	& \cand\   \forall y^\safe . (A_g (\vec u , \vec x , p z , y) \cimp y=_2 0 ) \\
-	& \cand\ \forall x^\safe < p z . \forall y^\safe . (A_g (\vec u , \vec x , x , y) \cimp y=_2 1) 
-	\end{array}
-	\right)
-	\end{array}
-	\]
-	Notice that $A_f$ is $\Pi^{\safe}_{i-1}$, since $A_g$ is $\Sigma^{\safe}_{i-1}$ and occurs only in negative context above, with additional safe universal quantifiers occurring in positive context.
-	In particular this means $A_f$ is $\Sigma^{\safe}_i$.
-	
-	Now, to prove totality of $A_f$, we rely on $\Sigma^\safe_{i-1}$-minimisation, which is a consequence of $\cpind{\Sigma^\safe_i}$:
-	
+ 
+ For predicative minimisation, assume $f$ is defined as  $\succ 1 \mu x .( g(\vec u ; \vec x , x) =_2 0)$ (or $0$ if no such $x$ exists).
+  By induction hypothesis we have a $\Sigma^{\safe}_{i-1}$ formula $A_g (\vec u , \vec x , x , y)$  satisfying the property. We then define $A_f(\vec u ; \vec x , z)$ as the following $\Sigma^{\safe}_{i}$ formula:
+\[
+\begin{array}{rl}
+&\left(
+z=0 \  \cand \ \forall x^\safe , y^\safe . (A_g (\vec u , \vec x , x, y) \cimp y=_2 1)
+\right) \\
+\cor & \left(
+\begin{array}{ll}
+z\neq 0 
+& \cand\   \forall y^\safe . (A_g (\vec u , \vec x , p z , y) \cimp y=_2 0 ) \\
+& \cand\ \forall x^\safe < p z . \forall y^\safe . (A_g (\vec u , \vec x , x , y) \cimp y=_2 1) 
+\end{array}
+\right)
+\end{array}
+\]
+As for the analogous bounded arithmetic theory $S^i_2$ (\cite{Buss86book}, Thm 20, p. 58),  $\arith^i$ can prove a \emph{minimisation} principle for $\Sigma^\safe_{i-1}$ formulas, allowing us to extract the \emph{least} witness of a safe existential; we prove this in the lemma below. We apply minimisation to $\exists x^\safe , y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$. From here we are able to readily prove the totality of $A_f(\vec u ; \vec x , z)$ arguing by cases, notably relying crucially on classical reasoning.
+\end{proof}
+
 	\begin{lemma}
 		[Minimisation]
-		$\arith^i \proves \cmin{\Sigma^\safe_{i-1}}$.	
+		For any $\Sigma^\safe_{i-1}$ formula $A$, $\arith^i \proves \exists x^\safe . A(x) \cimp \exists x^\safe . ( A(x) \cand \forall y^\safe \leq x . (A(y) \cimp y=x) ) $.	
 	\end{lemma}
 	% see Thm 20 p. 58 in Buss' book.
 	%\begin{proof}
@@ -76,7 +45,8 @@
 	\begin{proof}
 		This Lemma is proved by using the same method as for the proof of the analogous result in the bounded arithmetic $S_2^{i}$ (see \cite{Buss86book}, Thm 20, p. 58).
 		
-		Let $A(x)$ be a  $\Sigma^\safe_{i-1}$ formula, with $x$ in $\safe$. We define the formula $B(a,b,c)$ as:
+		%Let $A(x)$ be a  $\Sigma^\safe_{i-1}$ formula, with $x$ in $\safe$. 
+		We define the formula $B(a,b,c)$ as:
 		$$ \forall x^{\safe}. (x < |a| \moins b \cimp \zerobit(x,c)) \cand \forall y^{\safe}<c. \neg A(y) \cand \exists y^{\safe} < 2^{|a|\moins b}.A(c+y)$$
 		where $a$ is in $\normal$, $b$ in $\normal$ and $c$ in $\safe$.  $B(a,b,c)$ is in $\Sigma^\safe_{i}$.
 		
@@ -102,143 +72,215 @@
 		$$(A(a) \cand a \neq 0 ) \cimp \exists x^{\safe } \leq a.B(a,|a|,x).$$
 		But $B(a,|a|,x)$ implies $(\forall y^{\safe}<x. \neg A(y))\cand A(x)$, so we have proven:
 		$$(A(a) \cand a \neq 0 ) \cimp (\exists x^{\safe } \leq a. (\forall y^{\safe}<x. \neg A(y))\cand A(x))$$
-		which is the $\Sigma_{i-1}^{\safe}$ axiom for $A$.
+	%	which is the $\Sigma_{i-1}^{\safe}$ axiom for $A$.
+	as required.
 	\end{proof}
-	
-	Now, working in $\arith^i$, let $\vec u \in \normal , \vec x \in \safe$ and let us prove:
-	\[
-	\exists !z^\safe  . A_f(\vec u ; \vec x , z)
-	\]
-	Suppose that $\exists x^\safe , y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$.
-	We can apply minimisation due to the lemma above to find the least $x\in \safe$ such that $\exists y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$, and we set $z = \succ 1 x$. So $x= p z$. 
-	%\todo{verify $z\neq 0$ disjunct.} 
-	%Then $z \neq 0$ holds. 
-	Then $z=\succ{1} p z$ holds.
-	Moreover we had  $\exists ! y^\safe . A_g(\vec u , \vec x , x , y)$. So we deduce that
-	$\forall y^\safe . (A_g (\vec u , \vec x , p z , y) \cimp y=_2 0 ) $. Finally, as $p z$ is the least element such that
-	$\exists y^\safe .  (A_g (\vec u ,\vec x , p z , y) \cand y=_2 0)$, we deduce 
-	$\ \forall x^\safe < p z . \forall y^\safe . (A_g (\vec u , \vec x , x , y) \cimp y=_2 1) $. We conclude that the second member of the disjunction
-	$A_f(\vec u ; \vec x , z)$ is proven.  
-	
-	Otherwise, we have that $\forall x^\safe , y^\safe . (A_g (\vec u , \vec x , x, y) \cimp y=_2 1)$, so we can set $z=0$ and the first member of the disjunction $A_f(\vec u ; \vec x , z)$ is proven.  
-	
-	So we have proven $\exists z^\safe  . A_f(\vec u ; \vec x , z)$, and unicity can be easily verified.
-	
-	\paragraph*{Predicative recursion on notation}
-	
-	\anupam{Assume access to the following predicates (makes completeness easier, soundness will be okay):
-		\begin{itemize}
-			%	\item $\pair x y z $ . ``$z$ is the sequence that appends $y$ to the sequence $x$''
-			\item $\pair x y z$. ``$z$ is the sequence that prepends $x$ to the sequence $y$''
-			\item $\beta (i; x ,y)$. ``The $i$th element of the sequence $x$ is $y$.''
-		\end{itemize}
-	}
-	\patrick{I also assume access to the following predicates:
-		\begin{itemize}
-			%   \item $\zerobit (u,k)$ (resp. $\onebit(u,k)$). " The $k$th bit of $u$ is 0 (resp. 1)"
-			%   \item $\pref(k,x,y)$. "The prefix of $x$ (as a binary string) of length $k$ is $y$" 
-			\item $\addtosequence(w,y,w')$. "$w'$ represents the sequence obtained by adding $y$ at the end of the sequence represented by $w$". Here we are referring to sequences which can be decoded with predicate $\beta$.
-		\end{itemize}}
-		In the following we will use the predicates $\zerobit (u,k)$, $\onebit(u,k)$, $\pref(k,x,y)$ which have been defined in Sect. \ref{sect:graphsbasicfunctions}.
-		
-		Suppose that $f$ is defined by predicative recursion on notation:
-		\[
-		\begin{array}{rcl}
-		f(0 , \vec u ; \vec x) & \dfn & g(\vec u ; \vec x) \\
-		f(\succ i u, \vec u ; \vec x) & \dfn & h_i( u , \vec u ; \vec x , f(u , \vec u ; \vec x))
-		\end{array}
-		\]
-		
-		\anupam{using $\beta(i,x,y)$ predicate for sequences: ``$i$th element of $x$ is $y$''. Provably total in $\arith^1$.}
-		
-		Suppose we have $\Sigma^\safe_i$ formulae $A_g (\vec u ; \vec x,y)$ and $A_{h_i} (u , \vec u ; \vec x , y , z)$ computing the graphs of $g$ and $h_i$ respectively, provably total in $\arith^i$.
-		We define $A_f (u ,\vec u ; \vec x , y)$ as,
-		\[
-		\exists w^\safe . \left(
-		\begin{array}{ll}
-		& 
-		%Seq(z) \cand 
-		\exists^{\safe} y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w , y_0) ) \cand \beta(|u|, w,y ) \\
-		%\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1})  \cand A_{h_i} (u , \vec u ; \vec x , y_k , y_{k+1}) )\\
-		\cand & \forall^{\normal}  k < |u| . \exists^{\safe} y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1})  \cand B (u , \vec u ; \vec x , y_k , y_{k+1}) )
-		\end{array}
-		\right)
-		\]
-		where 
-		\[
-		B (u , \vec u ; \vec x , y_k , y_{k+1}) = \left(
-		\begin{array}{ll}
-		& \zerobit(u,k+1) \cimp  \exists v .(\pref(k,u,v)  \cand A_{h_0}(v,\vec u ; \vec x, y_k, y_{k+1}) )\\
-		\cand &  \onebit(u,k+1) \cimp  \exists v .(\pref(k,u,v)  \cand A_{h_1}(v,\vec u ; \vec x, y_k, y_{k+1}) )
-		\end{array}
-		\right)
-		\]
-		
-		%which is $\Sigma^\safe_i$ by inspection, and indeed defines the graph of $f$.
-		
-		To show totality, let $\vec u \in \normal, \vec x \in \safe$ and proceed by induction on $u \in \normal$.
-		The base case, when $u=0$, is immediate from the totality of $A_g$, so for the inductive case we need to show:
-		\[
-		\exists y^\safe . A_f (u , \vec u ; \vec x , y) 
-		\quad \seqar \quad
-		\exists z^\safe . A_f (s_i u, \vec u ; \vec x , z)
-		\]
-		
-		So let us assume $\exists y^\safe . A_f (u , \vec u ; \vec x , y) $. Then there exists $w$ such that $\safe(w)$ and 
-		$A_f (u , \vec u ; \vec x , w) $.
-		
-		We know that there exists a $z$ such that $A_{h_i}(u,\vec u ; \vec x, y, z)$. Let then $w'$ be such that
-		$\addtosequence(w,z,w')$. Observe also that we have $\pref(|u|,s_i u,u)$
-		
-		So we have, for $k=|u|$:
-		
-		$$  \beta (k, w', y) \cand \beta (k+1 ,w', z)  \cand B (u , \vec u ; \vec x , y , z).$$
-		
-		and we can conclude that
-		\[
-		\exists w'^\safe . \left(
-		\begin{array}{ll}
-		& 
-		%Seq(z) \cand 
-		\exists y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w' , y_0) ) \cand \beta(|u|+1, w',z ) \\
-		\cand & \forall k < |u|+1 . \exists y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1})  \cand B (u , \vec u ; \vec x , y_k , y_{k+1}) )
-		\end{array}
-		\right)
-		\]
-		So $\exists z^{\safe} . A_f (s_i u, \vec u ; \vec x , z)$ has been proven. So by induction we have proven $\forall^{\normal} u,  
-		\forall^{\normal} \vec u, \exists^{\safe} y. A_f (u ,\vec u ; \vec x , y)$. Moreover one can also check the unicity of $y$, and so we have proved the required formula. 
-		
-		\anupam{here need to `add' element to the computation sequence. Need to do this earlier in the paper.}
-		
-		\anupam{for inductive cases, need $u\neq 0$ for $\succ 0$ case.}
-		
-		\paragraph*{Safe composition}
-		Now suppose that $f$ is defined by safe composition:
-		\[
-		f(\vec u ; \vec x) \quad \dfn \quad g( \vec h(\vec u;) ; \vec h' (\vec u ; \vec x) )
-		\]
-		
-		By the inductive hypothesis, let us suppose that we have $\Sigma^\safe_i $ definitions $A_g , A_{h_i} , A_{h_j'} $ of the graphs of $g , h_i , h_j'$ respectively, which are provably total etc.
-		In particular, by Raising, we have that $\forall \vec u^\normal . \exists v^\normal . A_{h_i} (\vec u , v)$.
-		
-		We define $A_f (\vec u , \vec x , z)$ defining the graph of $f$ as follows:
-		\[
-		\exists \vec v^\normal . \exists \vec y^\safe .  
-		\left(  
-		\bigwedge\limits_i A_{h_i} (\vec u , v_i)
-		\wedge
-		\bigwedge\limits_j A_{h_j'} (\vec u ; \vec x , y_j)
-		\wedge
-		A_g ( \vec v , \vec y , z ) 
-		\right)
-		\]
-		The provable totality of $A_f$ follows from simple first-order reasoning, mostly cuts and basic quantifier manipulations.
-		
-		\todo{elaborate}
-		
-		The proof of Thm \ref{thm:completeness} is thus completed.
-\end{proof}
 
+%\begin{proof}
+%	We proceed by structural induction on a $\mubc^{i-1} $ program, dealing with each case in the proceeding paragraphs.
+%	
+%	The property is easily verified for the class of initial functions of  $\mubci{i-1}$: constant, projections, (binary) successors, predecessor, conditional, as already shown in Sect. \ref{sect:graphsbasicfunctions}. Now let us examine the three constructions: predicative minimisation, predicative (safe) recursion and composition. 
+%	\paragraph*{Predicative minimisation}
+%	Suppose $f(\vec u ; \vec x)$ is defined by predicative minimisation from $g$ (we then denote $f$ as as $\mu x^{+1} . g(\vec u ; \vec x , x) =_2 0$). 
+%	By definition $g$ is in $\mubci{i-2}$, and so by the inductive hypothesis there is a $\Sigma^{\safe}_{i-1}$ formula $A_g (\vec u , \vec x , x , y)$ computing the graph of $g$ such that,
+%	\[
+%	\arith^i \proves \forall \vec u^\normal . \forall \vec x^\safe , x^\safe . \exists ! y^\safe . A_g(\vec u , \vec x , x , y)
+%	\]
+%	Let us define $A_f(\vec u ; \vec x , z)$ as:
+%	\[
+%	\begin{array}{rl}
+%	&\left(
+%	z=0 \  \cand \ \forall x^\safe , y^\safe . (A_g (\vec u , \vec x , x, y) \cimp y=_2 1)
+%	\right) \\
+%	\cor & \left(
+%	\begin{array}{ll}
+%	%z\neq 0
+%	z=\succ{1} p z 
+%	& \cand\   \forall y^\safe . (A_g (\vec u , \vec x , p z , y) \cimp y=_2 0 ) \\
+%	& \cand\ \forall x^\safe < p z . \forall y^\safe . (A_g (\vec u , \vec x , x , y) \cimp y=_2 1) 
+%	\end{array}
+%	\right)
+%	\end{array}
+%	\]
+%	Notice that $A_f$ is $\Pi^{\safe}_{i-1}$, since $A_g$ is $\Sigma^{\safe}_{i-1}$ and occurs only in negative context above, with additional safe universal quantifiers occurring in positive context.
+%	In particular this means $A_f$ is $\Sigma^{\safe}_i$.
+%	
+%	Now, to prove totality of $A_f$, we rely on $\Sigma^\safe_{i-1}$-minimisation, which is a consequence of $\cpind{\Sigma^\safe_i}$:
+%	
+%	\begin{lemma}
+%		[Minimisation]
+%		$\arith^i \proves \cmin{\Sigma^\safe_{i-1}}$.	
+%	\end{lemma}
+%	% see Thm 20 p. 58 in Buss' book.
+%	%\begin{proof}
+%	%\end{proof}
+%	\begin{proof}
+%		This Lemma is proved by using the same method as for the proof of the analogous result in the bounded arithmetic $S_2^{i}$ (see \cite{Buss86book}, Thm 20, p. 58).
+%		
+%		Let $A(x)$ be a  $\Sigma^\safe_{i-1}$ formula, with $x$ in $\safe$. We define the formula $B(a,b,c)$ as:
+%		$$ \forall x^{\safe}. (x < |a| \moins b \cimp \zerobit(x,c)) \cand \forall y^{\safe}<c. \neg A(y) \cand \exists y^{\safe} < 2^{|a|\moins b}.A(c+y)$$
+%		where $a$ is in $\normal$, $b$ in $\normal$ and $c$ in $\safe$.  $B(a,b,c)$ is in $\Sigma^\safe_{i}$.
+%		
+%		The intuitive idea of the proof is to observe that, if $A(a)$ is true for $a\neq 0$, then  $\exists x^{\safe}\leq a. B(a,b,x)$ holds for $b=0$, and to try to prove it for $b=|a|$, by using a length induction on $b$.
+%		
+%		First, one can prove:
+%		$$ (A(a) \cand a \neq 0) \cimp B(a,0,0).$$ 
+%		And thus:
+%		$$ (A(a) \cand a \neq 0) \cimp \exists x^{\safe}\leq a .B(a,0,x).$$ 
+%		We then can check that the two following statements are provable:
+%		$$
+%		\begin{array}{rcl}
+%		(b<|a| \cand B(a,b,c)\cand \exists y^{\safe}<2^{|a| \moins (b+1)}.A(c+y)) &\cimp& B(a,\succ{} b,c)\\
+%		(b<|a| \cand B(a,b,c)\cand \forall y^{\safe}<2^{|a| \moins(b+1)}.  A(c+y)) &\cimp & B(a,\succ{} b, c+2^{|a| \moins (b+1)})
+%		\end{array}
+%		$$
+%		Moreover we have: $A(a) \cand B(a,b,c) \cimp c\leq a$.
+%		From these three statements we deduce:
+%		$$(A(a) \cand a \neq 0 \cand b<|a| \cand \exists x^{\safe} \leq a. B(a,b,x)) \cimp \exists x^{\safe } \leq a.B(a,\succ{} b,x).$$
+%		Note that here we have used the fact that we are in classical logic.
+%		
+%		The formula $\exists x\leq a. B(a,b,c)$ is in $\Sigma^{\safe}_{i}$, so by $\Sigma^{\safe}_{i}$-LIND on the formula $\exists x\leq a. B(a,b,c)$, with the variable $b$ which is in $\normal$,  we obtain:
+%		$$(A(a) \cand a \neq 0 ) \cimp \exists x^{\safe } \leq a.B(a,|a|,x).$$
+%		But $B(a,|a|,x)$ implies $(\forall y^{\safe}<x. \neg A(y))\cand A(x)$, so we have proven:
+%		$$(A(a) \cand a \neq 0 ) \cimp (\exists x^{\safe } \leq a. (\forall y^{\safe}<x. \neg A(y))\cand A(x))$$
+%		which is the $\Sigma_{i-1}^{\safe}$ axiom for $A$.
+%	\end{proof}
+%	
+%	Now, working in $\arith^i$, let $\vec u \in \normal , \vec x \in \safe$ and let us prove:
+%	\[
+%	\exists !z^\safe  . A_f(\vec u ; \vec x , z)
+%	\]
+%	Suppose that $\exists x^\safe , y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$.
+%	We can apply minimisation due to the lemma above to find the least $x\in \safe$ such that $\exists y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$, and we set $z = \succ 1 x$. So $x= p z$. 
+%	%\todo{verify $z\neq 0$ disjunct.} 
+%	%Then $z \neq 0$ holds. 
+%	Then $z=\succ{1} p z$ holds.
+%	Moreover we had  $\exists ! y^\safe . A_g(\vec u , \vec x , x , y)$. So we deduce that
+%	$\forall y^\safe . (A_g (\vec u , \vec x , p z , y) \cimp y=_2 0 ) $. Finally, as $p z$ is the least element such that
+%	$\exists y^\safe .  (A_g (\vec u ,\vec x , p z , y) \cand y=_2 0)$, we deduce 
+%	$\ \forall x^\safe < p z . \forall y^\safe . (A_g (\vec u , \vec x , x , y) \cimp y=_2 1) $. We conclude that the second member of the disjunction
+%	$A_f(\vec u ; \vec x , z)$ is proven.  
+%	
+%	Otherwise, we have that $\forall x^\safe , y^\safe . (A_g (\vec u , \vec x , x, y) \cimp y=_2 1)$, so we can set $z=0$ and the first member of the disjunction $A_f(\vec u ; \vec x , z)$ is proven.  
+%	
+%	So we have proven $\exists z^\safe  . A_f(\vec u ; \vec x , z)$, and unicity can be easily verified.
+%	
+%	\paragraph*{Predicative recursion on notation}
+%	
+%	\anupam{Assume access to the following predicates (makes completeness easier, soundness will be okay):
+%		\begin{itemize}
+%			%	\item $\pair x y z $ . ``$z$ is the sequence that appends $y$ to the sequence $x$''
+%			\item $\pair x y z$. ``$z$ is the sequence that prepends $x$ to the sequence $y$''
+%			\item $\beta (i; x ,y)$. ``The $i$th element of the sequence $x$ is $y$.''
+%		\end{itemize}
+%	}
+%	\patrick{I also assume access to the following predicates:
+%		\begin{itemize}
+%			%   \item $\zerobit (u,k)$ (resp. $\onebit(u,k)$). " The $k$th bit of $u$ is 0 (resp. 1)"
+%			%   \item $\pref(k,x,y)$. "The prefix of $x$ (as a binary string) of length $k$ is $y$" 
+%			\item $\addtosequence(w,y,w')$. "$w'$ represents the sequence obtained by adding $y$ at the end of the sequence represented by $w$". Here we are referring to sequences which can be decoded with predicate $\beta$.
+%		\end{itemize}}
+%		In the following we will use the predicates $\zerobit (u,k)$, $\onebit(u,k)$, $\pref(k,x,y)$ which have been defined in Sect. \ref{sect:graphsbasicfunctions}.
+%		
+%		Suppose that $f$ is defined by predicative recursion on notation:
+%		\[
+%		\begin{array}{rcl}
+%		f(0 , \vec u ; \vec x) & \dfn & g(\vec u ; \vec x) \\
+%		f(\succ i u, \vec u ; \vec x) & \dfn & h_i( u , \vec u ; \vec x , f(u , \vec u ; \vec x))
+%		\end{array}
+%		\]
+%		
+%		\anupam{using $\beta(i,x,y)$ predicate for sequences: ``$i$th element of $x$ is $y$''. Provably total in $\arith^1$.}
+%		
+%		Suppose we have $\Sigma^\safe_i$ formulae $A_g (\vec u ; \vec x,y)$ and $A_{h_i} (u , \vec u ; \vec x , y , z)$ computing the graphs of $g$ and $h_i$ respectively, provably total in $\arith^i$.
+%		We define $A_f (u ,\vec u ; \vec x , y)$ as,
+%		\[
+%		\exists w^\safe . \left(
+%		\begin{array}{ll}
+%		& 
+%		%Seq(z) \cand 
+%		\exists^{\safe} y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w , y_0) ) \cand \beta(|u|, w,y ) \\
+%		%\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1})  \cand A_{h_i} (u , \vec u ; \vec x , y_k , y_{k+1}) )\\
+%		\cand & \forall^{\normal}  k < |u| . \exists^{\safe} y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1})  \cand B (u , \vec u ; \vec x , y_k , y_{k+1}) )
+%		\end{array}
+%		\right)
+%		\]
+%		where 
+%		\[
+%		B (u , \vec u ; \vec x , y_k , y_{k+1}) = \left(
+%		\begin{array}{ll}
+%		& \zerobit(u,k+1) \cimp  \exists v .(\pref(k,u,v)  \cand A_{h_0}(v,\vec u ; \vec x, y_k, y_{k+1}) )\\
+%		\cand &  \onebit(u,k+1) \cimp  \exists v .(\pref(k,u,v)  \cand A_{h_1}(v,\vec u ; \vec x, y_k, y_{k+1}) )
+%		\end{array}
+%		\right)
+%		\]
+%		
+%		%which is $\Sigma^\safe_i$ by inspection, and indeed defines the graph of $f$.
+%		
+%		To show totality, let $\vec u \in \normal, \vec x \in \safe$ and proceed by induction on $u \in \normal$.
+%		The base case, when $u=0$, is immediate from the totality of $A_g$, so for the inductive case we need to show:
+%		\[
+%		\exists y^\safe . A_f (u , \vec u ; \vec x , y) 
+%		\quad \seqar \quad
+%		\exists z^\safe . A_f (s_i u, \vec u ; \vec x , z)
+%		\]
+%		
+%		So let us assume $\exists y^\safe . A_f (u , \vec u ; \vec x , y) $. Then there exists $w$ such that $\safe(w)$ and 
+%		$A_f (u , \vec u ; \vec x , w) $.
+%		
+%		We know that there exists a $z$ such that $A_{h_i}(u,\vec u ; \vec x, y, z)$. Let then $w'$ be such that
+%		$\addtosequence(w,z,w')$. Observe also that we have $\pref(|u|,s_i u,u)$
+%		
+%		So we have, for $k=|u|$:
+%		
+%		$$  \beta (k, w', y) \cand \beta (k+1 ,w', z)  \cand B (u , \vec u ; \vec x , y , z).$$
+%		
+%		and we can conclude that
+%		\[
+%		\exists w'^\safe . \left(
+%		\begin{array}{ll}
+%		& 
+%		%Seq(z) \cand 
+%		\exists y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w' , y_0) ) \cand \beta(|u|+1, w',z ) \\
+%		\cand & \forall k < |u|+1 . \exists y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1})  \cand B (u , \vec u ; \vec x , y_k , y_{k+1}) )
+%		\end{array}
+%		\right)
+%		\]
+%		So $\exists z^{\safe} . A_f (s_i u, \vec u ; \vec x , z)$ has been proven. So by induction we have proven $\forall^{\normal} u,  
+%		\forall^{\normal} \vec u, \exists^{\safe} y. A_f (u ,\vec u ; \vec x , y)$. Moreover one can also check the unicity of $y$, and so we have proved the required formula. 
+%		
+%		\anupam{here need to `add' element to the computation sequence. Need to do this earlier in the paper.}
+%		
+%		\anupam{for inductive cases, need $u\neq 0$ for $\succ 0$ case.}
+%		
+%		\paragraph*{Safe composition}
+%		Now suppose that $f$ is defined by safe composition:
+%		\[
+%		f(\vec u ; \vec x) \quad \dfn \quad g( \vec h(\vec u;) ; \vec h' (\vec u ; \vec x) )
+%		\]
+%		
+%		By the inductive hypothesis, let us suppose that we have $\Sigma^\safe_i $ definitions $A_g , A_{h_i} , A_{h_j'} $ of the graphs of $g , h_i , h_j'$ respectively, which are provably total etc.
+%		In particular, by Raising, we have that $\forall \vec u^\normal . \exists v^\normal . A_{h_i} (\vec u , v)$.
+%		
+%		We define $A_f (\vec u , \vec x , z)$ defining the graph of $f$ as follows:
+%		\[
+%		\exists \vec v^\normal . \exists \vec y^\safe .  
+%		\left(  
+%		\bigwedge\limits_i A_{h_i} (\vec u , v_i)
+%		\wedge
+%		\bigwedge\limits_j A_{h_j'} (\vec u ; \vec x , y_j)
+%		\wedge
+%		A_g ( \vec v , \vec y , z ) 
+%		\right)
+%		\]
+%		The provable totality of $A_f$ follows from simple first-order reasoning, mostly cuts and basic quantifier manipulations.
+%		
+%		\todo{elaborate}
+%		
+%		The proof of Thm \ref{thm:completeness} is thus completed.
+%\end{proof}
+%
+%
 
 
 
@@ -258,4 +300,3 @@
 
 
 
-
Index: CSL17/tech-report/soundness.tex
===================================================================
--- CSL17/tech-report/soundness.tex	(revision 266)
+++ CSL17/tech-report/soundness.tex	(revision 267)
@@ -47,10 +47,6 @@
 In the presence of a compatible sorting, we may easily define functions that \emph{evaluate} safe formulae in $\mubc$:
 
 
-\begin{proposition}
-Given a $\Sigma^\safe_i$ formula $A$ and compatible sorting $(\vec u; \vec x)$ of its variables, there is a $\mubci{i}$ program $\charfn{\vec u ;\vec x}{A} (l, \vec u ; \vec x)$ computing the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.
-\end{proposition}
-
 \begin{definition}
 	[Length bounded characteristic functions]
 	We define $\mubci{}$ programs $\charfn{}{A} (l , \vec u; \vec x)$, parametrised by a formula $A$ and a compatible typing $(\vec u ; \vec x)$ of its varables, as follows.
@@ -85,6 +81,13 @@
 \end{definition}
 
 
+\begin{proposition}
+Given a $\Sigma^\safe_i$ formula $A$ and compatible sorting $(\vec u; \vec x)$ of its variables, 
+$\charfn{\vec u ;\vec x}{A} (l, \vec u ; \vec x)$ is in $\mubci{i}$ and computes the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.
+\end{proposition}
+
+
+
 We will use the programs $\charfn{}{}$ in the witness functions we define below.
 Let us write $\charfn{}{i}$ to denote the class of functions $\charfn{}{A}$ for $A \in \Sigma^\safe_{i}$.
 For the notion of bounding polynomial below we are a little informal with bounds, using `big-oh' notation, since it will suffice just to be `sufficiently large'.
@@ -96,7 +99,7 @@
 	For a $\Sigma^\safe_{i}$ formula $A$ with a compatible sorting $(\vec u ; \vec x)$, we define the \emph{length-bounded witness function} $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w)$ in $\bc (\charfn{}{i-1})$ and its \emph{bounding polynomial} $b_A (l)$ as follows:
 	\begin{itemize}
 		\item If $A$ is $\Pi^\safe_{i-1}$ then $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w) \dfn \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x )$ and we set $b_A (l) = 1$.
-		\item If $A$ is $B \cor C$ then we may set $b_A = O(b_B + b_C)$ and define $		\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) \dfn		\orfn ( ; \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , \beta (b_B (l) , 0 ; w ) ) , \wit{\vec u ; \vec x}{C} (l, \vec u ; \vec x , \beta (b_C (l) , 0 ; w ) )  )$.
+		\item If $A$ is $B \cor C$ then we may set $|b_A| = O(|b_B| + |b_C|)$ and define $		\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) \dfn		\orfn ( ; \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , \beta (b_B (l) , 0 ; w ) ) , \wit{\vec u ; \vec x}{C} (l, \vec u ; \vec x , \beta (b_C (l) , 0 ; w ) )  )$.
 %		\[
 %		\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) 
 %		\quad \dfn \quad
@@ -121,7 +124,7 @@
 		%appealing to Lemma~\ref{lem:sharply-bounded-recursion}, 
 		and 
 		we set 
-		$b_A = O(b_{B(t)}^2 )$.
+		$|b_A| = O(|b_{B(t)}|^2 )$.
 		\item Similarly if $A$ is $\exists u^\normal \leq |t(\vec u;)|. A'(u)$, but with $\exists u \leq |t|$ in place of $\forall u \leq |t|$.
 		\item If $A$ is $\exists x^\safe . B(x) $ then
 		\(
@@ -129,8 +132,8 @@
 		\dfn 
 		\wit{\vec u ; \vec x , x}{B(x)} ( l, \vec u ; \vec x , \beta( b_{B} (l) , 0;w ) , \beta (q(l) , 1 ;w ))
 		\)
-		where $q$ is obtained by the polychecking and bounded minimisation properties, Lemmas~\ref{lem:polychecking} and \ref{lem:bounded-minimisation}, for $\wit{\vec u ; \vec x , x}{B(x)}$.
-		We may set $b_A = O(b_B + q )$.
+		where $q$ is obtained by the polychecking and bounded minimisation properties,\footnote{Here let us assume that $q$ is formulated as a corresponding quasipolynomial in $l$ as opposed to a polynomial in $|l|$, as in Lemma~\ref{lem:bounded-minimisation}.} Lemmas~\ref{lem:polychecking} and \ref{lem:bounded-minimisation}, for $\wit{\vec u ; \vec x , x}{B(x)}$.
+		We may set $|b_A| = O(|b_B | + |q|)$.
 	\end{itemize}
 %	\[
 %	\begin{array}{rcl}
@@ -151,7 +154,7 @@
 \end{definition}
 
 
-
+From Lemmas~\ref{lem:polychecking} and \ref{lem:bounded-minimisation} we have:
 \begin{proposition}
 	\label{prop:wit-rfn}
 	If, for some $w$, $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x,w) =1$, then $A (\vec u \mode l ; \vec x \mode l)$ is true.
@@ -177,17 +180,18 @@
 	\begin{array}{rl}
 &	\bigwedge\limits_{A \in \Gamma} \wit{\vec u ; \vec x}{ A} (l, \vec u ; \vec x , w_A \mode b_A(l)) =1 \\
 \noalign{\medskip}
-\implies & 	\bigvee\limits_{B\in \Delta} \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , f^\pi_B((\vec u ; \vec x )\mode l, \vec w \mode p(l))) = 1
+\implies & 	\bigvee\limits_{B\in \Delta} \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , f^\pi_B((\vec u ; \vec x )\mode l, \vec w \mode p^\pi(l))) = 1
 	\end{array}
 	\]
-	for some polynomial $p$.
+	for some polynomial $p^\pi$.
 %	\anupam{Need $\vec w \mode p(l)$ for some $p$.}
 %	\anupam{$l$ may occur freely in the programs $f^\pi_B$}
 \end{lemma}
 
 
 
-For the implication above, let us simply refer to the LHS as $\Wit{\vec u ; \vec x}{\Gamma} (l , \vec u ; \vec x , \vec w)$ and the RHS as $\Wit{\vec u ; \vec x}{ \Delta} (l, \vec u ; \vec x , \vec w')$, with $\vec w'$ in place of $\vec f( \cdots )$, which is a slight abuse of notation: we assume that LHS and RHS are clear from context.
+For the implication above, let us simply refer to the LHS as $\Wit{\vec u ; \vec x}{\Gamma} (l , \vec u ; \vec x , \vec w)$ and the RHS as $\Wit{\vec u ; \vec x}{ \Delta} (l, \vec u ; \vec x , \vec f^\pi ((\vec u ; \vec x )\mode l, \vec w \mode p^\pi(l))  )$, which is a slight abuse of notation: we assume that LHS and RHS are clear from context.
+Also let us call $p^\pi$ the \emph{modulus} of $f^\pi$ with respect to $l$.
 
 \begin{proof}
 	Since the proof is in typed variable normal form we have that each line of the proof is of the same form, i.e.\ $\normal (\vec u), \safe (\vec x) , \Gamma \seqar \Delta$ over free variables $\vec u ; \vec x$.
@@ -202,12 +206,14 @@
 Notice that, since $\pi$ is in De Morgan form, we have that $A$ is atomic ($s\leq t$) and so, in particular, $\Pi^\safe_{i-1}$.
 So we can simply set the witness for both $A$ and $\cnot A$ to $0$.
 Namely, if $\vec f (\vec u ; \vec x , \vec w , w )$ is obtained by the inductive hypothesis, then we may set $f^\pi_B ( \vec u ; \vec x , \vec w) \dfn f_B (\vec u ;\vec x , \vec w , 0)$ for $B\in \Delta$, and $f^\pi_A (\vec u ; \vec x , \vec w) \dfn 0$. 
-The bounding polynomial remains the same. 
+The modulus $p^\pi$ remains the same as that of the inductive hypothesis. 
+
+Left negation is similar, relying on a dummy argument.
 	
 	\paragraph*{Logical rules}
-	Pairing, depairing. Need length-boundedness.
-	
-	If we have a left conjunction step:
+%	Pairing, depairing. Need length-boundedness.
+	Suppose $\pi$ ends with a 
+	left conjunction step:
 	\[
 	\vlinf{\lefrul{\cand}}{}{ \normal (\vec u ), \safe (\vec x) , A\cand B , \Gamma \seqar \Delta }{ \normal (\vec u ), \safe (\vec x) , A, B , \Gamma \seqar \Delta}
 	\]
@@ -219,30 +225,30 @@
 	\]
 	for some polynomial $p$.
 	%
-	We define $\vec f^\pi (\vec u ; \vec x , w , \vec w) \dfn \vec f (\vec u ; \vec x , \beta (p(l),0; w) , \beta(p(l),1;w),\vec w )$ and, by the bounding polynomial for pairing, it suffices to set $p^\pi = O(p)$.
+	We define $\vec f^\pi (\vec u ; \vec x , w , \vec w) \dfn \vec f (\vec u ; \vec x , \beta (p(l),0; w) , \beta(p(l),1;w),\vec w )$ and, by the bounding polynomial for pairing, it suffices to set $|p^\pi| = O(|p|)$.
 	
+		Right disjunction step:
+		\[
+		\vlinf{\rigrul{\cor}}{}{ \normal (\vec u ), \safe (\vec x) , \Gamma \seqar \Delta , A \cor B}{ \normal (\vec u ), \safe (\vec x) , \Gamma \seqar \Delta, A, B }
+		\]
+		$\vec f^\pi_\Delta$ remains the same as that of premiss.
+		Let $f_A, f_B$ be the functions corresponding to $A$ and $B$ in the premiss, so that:
+		\[
+		\Wit{\vec u ; \vec x}{\Gamma} (l, \vec u ; \vec x , \vec w)
+		\quad \implies \quad
+		\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , f_C ( (\vec u ; \vec x) \mode l , \vec w \mode p(l) ))		
+		\]
+		for $C = A,B$ and for some $p$, such that $f_A , f_B$ are bounded by $q(l)$ (again by IH).
+		We define $f^\pi_{A\cor B} (\vec u ; \vec x, \vec w) \dfn \pair{q(l)}{f_A ((\vec u ; \vec x, \vec w))}{f_B ((\vec u ; \vec x, \vec w))}$.
 	
-	Right disjunction step:
-	\[
-	\vlinf{\rigrul{\cor}}{}{ \normal (\vec u ), \safe (\vec x) , \Gamma \seqar \Delta , A \cor B}{ \normal (\vec u ), \safe (\vec x) , \Gamma \seqar \Delta, A, B }
-	\]
-	$\vec f^\pi_\Delta$ remains the same as that of premiss.
-	Let $f_A, f_B$ be the functions corresponding to $A$ and $B$ in the premiss, so that:
-	\[
-	\Wit{\vec u ; \vec x}{\Gamma} (l, \vec u ; \vec x , \vec w)
-	\quad \implies \quad
-	\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , f_C ( (\vec u ; \vec x) \mode l , \vec w \mode p(l) ))		
-	\]
-	for $C = A,B$ and for some $p$, such that $f_A , f_B$ are bounded by $q(l)$ (again by IH).
-	We define $f^\pi_{A\cor B} (\vec u ; \vec x, \vec w) \dfn \pair{q(l)}{f_A ((\vec u ; \vec x, \vec w))}{f_B ((\vec u ; \vec x, \vec w))}$.
+	The other logical cases use a similar argument.
+	
+
 	\paragraph*{Quantifiers}
-	\anupam{Do $\exists$-right and $\forall$-right, left rules are symmetric.}
-	
-	
-	
-	Sharply bounded quantifiers are generalised versions of logical rules.
+	If $\pi$ ends with a sharply bounded quantifier step, then we use a similar argument to that for logical rules. 
+	For instance, suppose $\pi$ ends with a $\rigrul{|\forall|}$:
 	\[
-	\vlinf{|\forall|}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar  \Delta , \forall u^\normal \leq |t(\vec u;)| . A(u) }{ \normal(u) , \normal (\vec u) , \safe (\vec x) , u \leq |t(\vec u;)| , \Gamma \seqar  \Delta, A(u)  }
+	\vlinf{\rigrul{|\forall|}}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar  \Delta , \forall u^\normal \leq |t(\vec u;)| . A(u) }{ \normal(u) , \normal (\vec u) , \safe (\vec x) , u \leq |t(\vec u;)| , \Gamma \seqar  \Delta, A(u)  }
 	\]
 	By the inductive hypothesis we have functions $\vec f(u , \vec u ; \vec x , w , \vec w)$ such that:
 	\[
@@ -256,6 +262,7 @@
 	
 	We set $f^\pi_{\forall u^\normal \leq t . A} (\vec u ; \vec x , \vec w) \dfn F(q(|l|), t(\vec u;), \vec u ; \vec x , 0, \vec w  )$.
 	
+		\anupam{Do $\exists$-right and $\forall$-right, left rules are symmetric.}
 	
 	Right existential:
 	\[
@@ -265,14 +272,15 @@
 	
 	
 	\paragraph*{Contraction}
-	Left contraction simply duplicates an argument, whereas right contraction requires a conditional on a $\Sigma^\safe_i$ formula.
+	Left contraction simply duplicates an argument,\footnote{We ignore here the cases when contraction is on a $\normal (u) $ or $\safe (x)$ formula, treating these formulae form as forming a set rather than a multiset.} whereas right contraction requires a conditional on a $\Sigma^\safe_i$ formula.
+	This is the reason why we need to the witness function encoded itself into $\mubc$ rather than simply using a predicate.
 	
+	For the sake of example, suppose $\pi$ ends with a right contraction step:
 	\[
 	\vlinf{\cntr}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A }{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A , A}
 	\]
-	
-	$\vec f^\pi_\Delta$ remains the same as that of premiss. Let $f_0 ,f_1$ correspond to the two copies of $A$ in the premiss.
-	We define:
+	By the inductive hypothesis we have functions $\vec f_\Delta , f_0, f_1$ corresponding to the RHS $\Delta , A ,A$.
+	We may define $\vec f^\pi_\Delta = \vec f_\Delta$ and:
 	\[
 	f^\pi_A ( \vec u ; \vec x , \vec w  )
 	\quad \dfn \quad
Index: CSL17/tech-report/main.tex
===================================================================
--- CSL17/tech-report/main.tex	(revision 266)
+++ CSL17/tech-report/main.tex	(revision 267)
@@ -68,7 +68,7 @@
 \appendix
 
 %%\input{pv-theories}	
-\input{appendix-sequent-calculus}
+%\input{appendix-sequent-calculus}
 
 
 \end{document}
Index: CSL17/tech-report/arithmetic.tex
===================================================================
--- CSL17/tech-report/arithmetic.tex	(revision 266)
+++ CSL17/tech-report/arithmetic.tex	(revision 267)
@@ -26,14 +26,14 @@
 
 Namely, in addition to usual axioms, our $\basic$ includes the following:\footnote{Later some of these will be redundant, for instance $\safe (u \times x) $ and $\safe (u \smsh v)$ are consequences of $\Sigma^\safe_i$-$\pind$, but $\safe (x + y)$ is not since both inputs are safe and so we cannot induct.}
 \begin{enumerate}[(a)]
-	\item $\forall u^\normal. \safe(u) $
+	\item\label{ax:a} $\forall u^\normal. \safe(u) $
 	\item $\safe (0) $
 	\item $\forall x^\safe . \safe (\succ{} x) $
 	\item $\forall u^\safe .\safe(\hlf{u})$
 	\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(|u|)$
+	\item\label{ax:h} $\forall u^\normal .\safe(|u|)$
 \end{enumerate}
 %\[
 %\begin{array}{l}
@@ -50,7 +50,7 @@
 %\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. }
+%\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$.
 %
@@ -211,7 +211,7 @@
 %
 %\anupam{In induction,for inductive cases, need $u\neq 0$ for $\succ 0$ case.}
 
-\anupam{Need vector $\vec y^\safe$?}
+%\anupam{Need vector $\vec y^\safe$?}
 
 \begin{remark}
 Notice that $\rais$ looks similar to the $K$ rule from the calculus for the modal logic $S4$ (which subsumes necessitation), and indeed we believe there is a way to present these results in such a framework.
@@ -219,40 +219,45 @@
 	\end{remark}
 
 
+Let us consider some basic examples of theorems of our
 \begin{example}
 	[Some basic theorems]
 	We give proofs of the following, that are sometimes included as basic axioms, in $\arith^1$:
-	\[
-	\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   )  \\        %% 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}
-	\]
-	\todo{Proof: Patrick? The final two should require PIND.}
+	\begin{enumerate}[(i)]
+		\item\label{item:i} $\forall x^\safe . 0 \neq \succ{} (x)$
+		\item\label{item:ii} $\forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) $
+		\item\label{item:iii} $\forall u^\normal . (u = 0 \cor \exists y^\safe.  u = \succ{} v  ) $
+		\item\label{item:iv} $\forall u^\normal ,x^\safe . u \cdot \succ{} x = u + ux$
+	\end{enumerate}
+%	\[
+%	\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   )  \\        %% 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}
+%	\]
+%	\todo{Proof: Patrick? The final two should require PIND.}
 	
-	\patrick{Actually statement 4 is nearly trivial from axiom 27 (for which I corrected the sorts). Maybe you meant something else?
-		\anupam{I actually changed those sorts from the submitted version: I really think axiom 27 should be $\forall x^{\safe}, y^{\normal}.  x\cdot(\succ{}y)=(x\cdot y)+x$, i.e.\ with the recursion on the normal variable. That way we can do induction on it. Statement 4 is meant to state the recursive property for the safe argument, which we can prove by induction on the normal argument, $u$.}
-	
-	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.}
-\anupam{Rather, I do not know how you would prove the current version: we cannot induct on $\exists v^\normal$ from axiom 27 as I state it. For the previous version I would just do induction on $u$ in $(u = 0 \cor \exists x^\safe.\  u = \succ{} x )$. }
+%	\patrick{Actually statement 4 is nearly trivial from axiom 27 (for which I corrected the sorts). Maybe you meant something else?
+%		\anupam{I actually changed those sorts from the submitted version: I really think axiom 27 should be $\forall x^{\safe}, y^{\normal}.  x\cdot(\succ{}y)=(x\cdot y)+x$, i.e.\ with the recursion on the normal variable. That way we can do induction on it. Statement 4 is meant to state the recursive property for the safe argument, which we can prove by induction on the normal argument, $u$.}
+%	
+%	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.}
+%\anupam{Rather, I do not know how you would prove the current version: we cannot induct on $\exists v^\normal$ from axiom 27 as I state it. For the previous version I would just do induction on $u$ in $(u = 0 \cor \exists x^\safe.\  u = \succ{} x )$. }
 	\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$.
- $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 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}
+	For \eqref{item:i}, 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.
+	
+	For \eqref{item:ii} 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.
+	
+	For \eqref{item:iii} 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.
+	
+	 For \eqref{item:iv} 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{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}
@@ -485,10 +490,19 @@
 	where $\Gamma \seqar \Delta$ contains only $\Sigma^\safe_i$ formulae for which the sorting $(\vec u ;\vec x)$ is compatible.
 \end{theorem}
 
-Strictly speaking, we must alter some of the sequent rules a little to arrive at this normal form. For instance the $\pind$ rule would have $\normal(\vec u)$ in its lower sequent rather than $\normal (t(\vec u))$. The latter is a consequence of the former already in $\basic$.
-The proof of this result also relies on a heavy use of the structural rules, contraction and weakening, to ensure that we always have a complete and compatible sorting of variables on the LHS of a sequent. This is similar to what is done in \cite{OstrinWainer05} where they use a $G3$ style calculus to manage such structural manipulations.
+Strictly speaking, we must alter some of the sequent rules a little to arrive at this normal form. For instance the $\pind$ rule would have $\normal(\vec u)$ in its lower sequent rather than $\normal (t(\vec u))$:
+\[
+\small
+\vliinf{}{}{ \normal(\vec u) , \safe (\vec x) , \Gamma , A(0) \seqar A(t(\vec u)), \Delta }{ \normal(u), \normal (\vec u) , \safe (\vec x) , \Gamma, A(u) \seqar A(\succ{0} u) , \Delta }{ \normal(u) ,, \normal(\vec u ) , \safe (\vec x) , \Gamma, A(u) \seqar A(\succ{1} u) , \Delta  }
+\] 
+Notice that $\normal(t(\vec u))$ is a consequence of $\normal (\vec u)$ already in $\basic$, due to the axioms \eqref{ax:a}-\eqref{ax:h}.
+That the variables of $t$ can be assumed to occur already in the premisses is due to weakening.
+Indeed, the proof of this result relies on a heavy use of the structural rules, contraction and weakening, to ensure that we always have a complete and compatible sorting of variables on the LHS of a sequent. This is similar to what is done in \cite{OstrinWainer05} where they use a $G3$ style calculus to manage such structural manipulations.
 
-As we mentioned, the fact that only $\Sigma^\safe_i$ formulae occur is due to the free-cut elimination result for first-order calculi \cite{Takeuti87,Cook:2010:LFP:1734064}, which gives a form of proof where every $\cut$ step has one of its cut formulae `immediately' below a non-logical step. Again, we have to adapt the $\rais$ rule a little to achieve our result, due to the fact that it has a $\exists x^\normal$ in its lower sequent. For this we consider a merge of $\rais$ and $\cut$, which allows us to directly cut the upper sequent of $\rais$ against a sequent of the form $\normal(u), A(u), \Gamma \seqar \Delta$.
+As we mentioned, the fact that only $\Sigma^\safe_i$ formulae occur is due to the free-cut elimination result for first-order calculi \cite{Takeuti87,Cook:2010:LFP:1734064}, which gives a form of proof where every $\cut$ step has one of its cut formulae `immediately' below a non-logical step. Again, we have to adapt the $\rais$ rule a little to achieve our result, due to the fact that it has a $\exists x^\normal$ in its lower sequent. For this we consider a merge of $\rais$ and $\cut$, which allows us to directly cut the upper sequent of $\rais$ against a sequent of the form $\normal(u), A(u), \Gamma \seqar \Delta$:
+\[
+\vliinf{\rais\cut}{}{\normal (\vec u) , \Gamma \seqar \Delta}{\normal (\vec u) \seqar \exists x^\safe . A(x)}{\normal (u) , A(u) , \Gamma \seqar \Delta}
+\]
 
 Finally, as is usual in bounded arithmetic, we use distinguished rules for our relativised quantifiers \cite{Buss86book}, although we use ones that satisfy the aforementioned constraints. For instance, we include the following rules, from which the remaining ones are similar:
 \[
