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

%\input{appendix-sequent-calculus}

	\item\label{ax:a} $\forall u^\normal. \safe(u) $

	\item\label{ax:h} $\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. }

%\anupam{Need vector $\vec y^\safe$?}

Let us consider some basic examples of theorems of our

	\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 )$. }

	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$.	

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$:

\[

\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}

\]

\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; 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}

		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) ) $.	

		%Let $A(x)$ be a  $\Sigma^\safe_{i-1}$ formula, with $x$ in $\safe$. 

		We define the formula $B(a,b,c)$ as:

	%	which is the $\Sigma_{i-1}^{\safe}$ axiom for $A$.

	as required.

%\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}

%

%

\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}

		\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 ) )  )$.

		$|b_A| = O(|b_{B(t)}|^2 )$.

		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|)$.

From Lemmas~\ref{lem:polychecking} and \ref{lem:bounded-minimisation} we have:

\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

	for some polynomial $p^\pi$.

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$.

The modulus $p^\pi$ remains the same as that of the inductive hypothesis. 

Left negation is similar, relying on a dummy argument.

%	Pairing, depairing. Need length-boundedness.

	Suppose $\pi$ ends with a 

	left conjunction step:

	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))}$.

	The other logical cases use a similar argument.

	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{\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)  }

		\anupam{Do $\exists$-right and $\forall$-right, left rules are symmetric.}

	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:

	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: