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

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