Index: soundness.tex
===================================================================
--- soundness.tex	(revision 266)
+++ 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
