Index: soundness.tex
===================================================================
--- soundness.tex	(revision 267)
+++ soundness.tex	(revision 268)
@@ -5,7 +5,7 @@
 
 \begin{theorem}
 	\label{thm:soundness}
-	If $\arith^i$ proves $\forall \vec u^\normal . \forall \vec x^\safe . \exists y^\safe . A(\vec u ; \vec x , y)$ then there is a $\mubci{i-1}$ program $f(\vec u ; \vec x)$ such that $\Nat \models A(\vec u ; \vec x , f(\vec u ; \vec x))$.
+	If $\arith^i$ proves $\forall \vec u^\normal  . \exists y^\safe . A(\vec u ;  y)$ then there is a $\mubci{i-1}$ program $f(\vec u ; )$ such that $\Nat \models A(\vec u ;  f(\vec u ; ))$.
 \end{theorem}
 
 
@@ -178,9 +178,15 @@
 %	\ \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
 	\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 \\
+&	\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^\pi(l))) = 1
+\implies & 	\bigvee\limits_{B\in \Delta} \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , f^\pi_B(l,
+(
+\vec u ; \vec x 
+)	\mode l
+, \vec w \mode p^\pi(l))) = 1
 	\end{array}
 	\]
 	for some polynomial $p^\pi$.
@@ -190,12 +196,16 @@
 
 
 
-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.
+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 (
+l,(
+\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}
+\begin{proof}[Proof sketch]
 	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$.
-	We define the function $f$ inductively, by considering the various final rules of $\pi$.
+	We define the function $f^\pi$ inductively, by considering the various final rules of $\pi$.
 	
 	
 	\paragraph*{Negation}
@@ -205,7 +215,7 @@
 \]
 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$. 
+Namely, if $\vec f (l,\vec u ; \vec x , \vec w , w )$ is obtained by the inductive hypothesis, then we may set $f^\pi_B (l, \vec u ; \vec x , \vec w) \dfn f_B (l,\vec u ;\vec x , \vec w , 0)$ for $B\in \Delta$, and $f^\pi_A (\vec u ; \vec x , \vec w) \dfn 0$. 
 The modulus $p^\pi$ remains the same as that of the inductive hypothesis. 
 
 Left negation is similar, relying on a dummy argument.
@@ -217,118 +227,137 @@
 	\[
 	\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}
 	\]
-	By inductive hypothesis we have functions $\vec f (\vec u ; \vec x , w_A , w_B , \vec w)$ such that,
+	By inductive hypothesis we have functions $\vec f (l,\vec u ; \vec x , w_A , w_B , \vec w)$ such that,
 	\[
 	\Wit{\vec u ; \vec x}{\Gamma} (l, \vec u ; \vec x , w_A , w_B , \vec w)
 	\quad \implies \quad
-	\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , \vec f ( (\vec u ; \vec x) \mode l , (w_A , w_B , \vec w) \mode p(l) ))
+	\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , \vec f (
+	l, (
+	\vec u ; \vec x
+	) \mode l 
+	, (w_A , w_B , \vec w) \mode p(l) ))
 	\]
 	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 (l,\vec u ; \vec x , w , \vec w) \dfn \vec f (l,\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:
+	Suppose $\pi$ ends with a 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:
+		Let $\vec f , f_A, f_B$ be obtained by the inductive hypothesis 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) ))		
+		\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , (\vec f , f_A , f_B) ( 
+		l,(
+		\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))}$.
+		$\vec f^\pi_\Delta$ is defined the same as $\vec f$. 
+		Let $q(l)$ be an upper bound for $f_A , f_B$  and 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))}$.
+		$p^\pi$ is obtained from $p$, $q$ and the bounding polynomial for pairing.
 	
 	The other logical cases use a similar argument.
 	
 
 	\paragraph*{Quantifiers}
-	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)  }
-	\]
-	By the inductive hypothesis we have functions $\vec f(u , \vec u ; \vec x , w , \vec w)$ such that:
-	\[
-	\Wit{u ,\vec u ; \vec x}{\lhs} ( u , \vec u ;\vec x , w , \vec w )
-	\quad \implies \quad
-	\Wit{u , \vec u ; \vec x}{\rhs} (u, \vec u ; \vec x , \vec f ((\vec u ; \vec x) \mode l , \vec w \mode p(l) ) )
-	\]
-	with $|f|\leq q(|l|)$.
+	Sharply bounded quantifier steps use a similar argument to the logical rules above, only requiring a larger modulus.
 	
-	By Lemma~\ref{lem:sequence-creation}, we have a function $F (l , u , \vec u ; \vec x , w , \vec w) $ such that....
 	
-	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  )$.
+%	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)  }
+%	\]
+%	By the inductive hypothesis we have functions $\vec f(u , \vec u ; \vec x , w , \vec w)$ such that:
+%	\[
+%	\Wit{u ,\vec u ; \vec x}{\lhs} ( u , \vec u ;\vec x , w , \vec w )
+%	\quad \implies \quad
+%	\Wit{u , \vec u ; \vec x}{\rhs} (u, \vec u ; \vec x , \vec f ((\vec u ; \vec x) \mode l , \vec w \mode p(l) ) )
+%	\]
+%	with $|f|\leq q(|l|)$.
+%	
+%	By Lemma~\ref{lem:sequence-creation}, we have a function $F (l , u , \vec u ; \vec x , w , \vec w) $ such that....
+%	
+%	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.}
 	
-		\anupam{Do $\exists$-right and $\forall$-right, left rules are symmetric.}
-	
-	Right existential:
+Suppose $\pi$ ends with a right existential step:\footnote{	Here we assume the variables of $t$ are amongst $(\vec u ; \vec x)$, since we are in typed variable normal form.}
 	\[
-	\vlinf{\rigrul{\exists}}{}{\normal(\vec u ) , \safe (\vec x) , \Gamma \seqar \Delta , \exists x . A(x)}{\normal(\vec u ) , \safe (\vec x) , \Gamma \seqar \Delta , A(t)}
+	\vlinf{\rigrul{\exists}}{}{\normal(\vec u ) , \safe (\vec x) , \Gamma \seqar \Delta , \exists x . A(x)}{\normal(\vec u ) , \safe (\vec x) , \Gamma \seqar \Delta , A(t (\vec u ; \vec x))}
 	\]
-	Here we assume the variables of $t$ are amongst $(\vec u ; \vec x)$, since we are in typed variable normal form.
+By the inductive hypothesis we have functions $\vec f , f$ such that:
+\[
+\Wit{\vec u ;\vec x}{\Gamma} ( l , \vec u ; \vec x , \vec w )
+\quad \implies \quad
+\Wit{\vec u ; \vec x}{\Delta, A(t)} ( l, \vec u ; \vec x , (\vec f , f) (l, (\vec u ; \vec x) \mode l , \vec w \mode p(l) ) )
+\]
+We let $\vec f^\pi_\Delta \dfn \vec f$ and define $f^\pi_{\exists x . A } ( l, \vec u ; \vec x , \vec w ) \dfn \pair{p(l) + t(\vec l ; \vec l)}{f(l, \vec u ; \vec x , \vec w)}{t(\vec u ; \vec x)}$.
+$p^\pi$ is hence obtained from $t$, $p$ and the bounding polynomial for pairing.
 	
+	Other quantifier steps are routine.
 	
 	\paragraph*{Contraction}
 	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:
+	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}
 	\]
 	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  )
+	f^\pi_A (l, \vec u ; \vec x , \vec w  )
 	\quad \dfn \quad
-	\cond (; \wit{\vec u ; \vec x}{A} ( l , \vec u ; \vec x , f_0(\vec u ; \vec x , \vec w) ) , f_1(\vec u ; \vec x , \vec w) , f_0(\vec u ; \vec x , \vec w)  )
+	\cond (; \wit{\vec u ; \vec x}{A} ( l , \vec u ; \vec x , f_0(l,\vec u ; \vec x , \vec w) ) , f_1(l,\vec u ; \vec x , \vec w) , f_0(\vec u ; \vec x , \vec w)  )
 	\]
 	
 	
-	\anupam{For $\normal (\vec u), \safe (\vec x)$ in antecedent, we always consider as a set, so do not display explicitly contraction rules. }
+%	\anupam{For $\normal (\vec u), \safe (\vec x)$ in antecedent, we always consider as a set, so do not display explicitly contraction rules. }
 	\paragraph*{Induction}
-	Corresponds to safe recursion on notation.
-	Suppose final step is (wlog):
+Suppose $\pi$ ends with a polynomial induction step:
 	\[
 	\vlinf{\pind}{}{ \normal (\vec u), \safe (\vec x) , \Gamma, A(0) \seqar A(t(\vec u ;)) , \Delta}{ \left\{\normal (u) , \normal (\vec u) , \safe (\vec x) , \Gamma,  A(u) \seqar A(\succ i u ) , \Delta \right\}_{i=0,1} }
 	\]
-	\anupam{need to say in normal form part that can assume induction of this form}
-	For simplicity we will assume $\Delta $ is empty, which we can always do by Prop.~\todo{DO THIS!}
-	
+%	\anupam{need to say in normal form part that can assume induction of this form}
+	For simplicity we will assume $\Delta $ is empty.\footnote{Note that a proof can always be put into this form by the right disjunction rules. The criterion on logical complexity for typed variable normal form proofs is preserved due to free-cut freeness.}
+	%
 	Now, by the inductive hypothesis, we have functions $h_i$ such that:
 	\[
-	\Wit{u , \vec u ; \vec x}{\Gamma, A(0)} (l , u , \vec u ; \vec x ,  \vec w)
+	\Wit{u , \vec u ; \vec x}{\Gamma, A(0)} (l , u , \vec u ; \vec x ,  \vec w , w)
 	\quad \implies \quad
-	\Wit{u , \vec u ; \vec x}{A(\succ i u)} (l , u , \vec u ; \vec x ,  h_i ((u , \vec u) \mode l ; \vec x \mode l , \vec w) )
+	\Wit{u , \vec u ; \vec x}{A(\succ i u)} (l , u , \vec u ; \vec x ,  h_i (l,(u , \vec u ; \vec x ) \mode l , (\vec w , w) \mode p(l) ) )
 	\]
-	First let us define $ f$ as follows:
+	First let us define $ f$ by safe recursion as follows:
 	\[
 	\begin{array}{rcl}
-	f (0 , \vec u ; \vec x, \vec w,  w ) & \dfn &  w\\
-	f( \succ i u , \vec u ; \vec x , \vec w, w) & \dfn & 
-	h_i (u , \vec u ; \vec x , \vec w , f(u , \vec u ; \vec x , \vec w , w ))
+	f (l,0 , \vec u ; \vec x, \vec w,  w ) & \dfn &  w\\
+	f(l, \succ i u , \vec u ; \vec x , \vec w, w) & \dfn & 
+	h_i (l,u , \vec u ; \vec x , \vec w , f(l,u , \vec u ; \vec x , \vec w , w ))
 	\end{array}
 	\]
-	where $\vec w$ corresponds to $\Gamma $ and $w$ corresponds to $A(0)$.
-	\anupam{Wait, should $\normal (t)$ have a witness? Also there is a problem like Patrick said for formulae like: $\forall x^\safe . \exists y^\safe. (\normal (z) \cor \cnot \normal (z))$, where $z$ is $y$ or otherwise.}
-	
+%	where $\vec w$ corresponds to $\Gamma $ and $w$ corresponds to $A(0)$.
+%	\anupam{Wait, should $\normal (t)$ have a witness? Also there is a problem like Patrick said for formulae like: $\forall x^\safe . \exists y^\safe. (\normal (z) \cor \cnot \normal (z))$, where $z$ is $y$ or otherwise.}
 	Now we let $f^\pi (\vec u ; \vec x , \vec w) \dfn f(t(\vec u ; ) , \vec u ; \vec x , \vec w)$.
+	It suffices to let $|p^\pi| = O(|p|^2)$.
 	
 	\paragraph*{Cut}
-	If it is a cut on an induction formula, which is safe, then it just corresponds to a safe composition since everything is substituted into a safe position.
-	Otherwise it is a `raisecut':
+	If $\pi$ ends with a cut on an induction formula, which is $\Sigma^\safe_i$, then $f^\pi$ is obtained from the inductive hypothesis by simply substituting already defined functions into a safe position.
+	The other possibility is that $\pi$ ends with a `raisecut':
 	\[
 	\vliinf{\rais\cut}{}{\normal (\vec u ) , \normal (\vec v) , \safe (\vec x) ,\Gamma \seqar \Delta }{ \normal (\vec u) \seqar \exists x^\safe  . A(x) }{ \normal (u)  , \normal (\vec v) , \safe (\vec x) , A(u), \Gamma \seqar \Delta }
 	\]
-	In this case we have functions $f(\vec u ; )$ and $\vec g (u, \vec v ; \vec x , w , \vec w )$, in which case we construct $\vec f^\pi$ as:
+	In this case, by the inductive hypothesis, we have functions $f(l,\vec u ; )$ from the left premiss and $\vec g (l,u, \vec v ; \vec x , w , \vec w )$ from the right premiss, so we may define:
 	\[
-	\vec f^\pi ( \vec u , \vec v ; \vec x , \vec w )
+	\vec f^\pi ( l ,  \vec u , \vec v ; \vec x , \vec w )
 	\quad \dfn \quad
-	\vec g ( \beta (1 ; f(\vec u ;) ) , \vec v ; \vec x , \beta(0;f(\vec u ;)) , \vec w )
+	\vec g ( l, \beta (1 ; f(l,\vec u ;) ) , \vec v ; \vec x , \beta(0;f(l,\vec u ;)) , \vec w )
 	\]
+	Again, $p^\pi$ is obtained from $p$ and the bounding polynomial for pairing.
 \end{proof}
 
 
@@ -341,7 +370,7 @@
 	\begin{proof}
 		[Proof sketch of Thm.~\ref{thm:soundness} from Lemma~\ref{lem:proof-interp}]
 		Suppose $\arith^i \proves \forall \vec u^\normal . \exists x^\safe . A(\vec u ; x)$. By inversion and Thm.~\ref{thm:normal-form} there is a $\arith^i$ proof $\pi$ of $\normal (\vec u ) \seqar \exists x^\safe. A(\vec u ; x )$ in typed variable normal form.
-By Lemma~\ref{lem:proof-interp}, we have a $\mubci{i-1}$ function $f^\pi$ with $\wit{\vec u ;}{\exists x^\safe . A} (l, \vec u ; f(\vec u \mode l;)) =1$.
-By the definition of $\wit{}{}$ and Prop.~\ref{prop:wit-rfn} we have that $\exists x . A(\vec u \mode l; x)$ is true just if $A(\vec u \mode l ; \beta (q(l), 1 ; f(\vec u \mode l;) ))$ is true.
-Now, since all $\vec u$ are normal, we may simply set $l$ to have a longer length than all of these arguments, so the function $f(\vec u;) \dfn \beta (q(\sum \vec u), 1 ; f(\vec u \mode \sum \vec u;) ))$ suffices to finish the proof.
+By Lemma~\ref{lem:proof-interp}, we have a $\mubci{i-1}$ function $f^\pi$ with $\wit{\vec u ;}{\exists x^\safe . A} (l, \vec u ; f^\pi(l,\vec u \mode l;)) =1$.
+By the definition of $\wit{}{}$ and Prop.~\ref{prop:wit-rfn} we have that $\exists x . A(\vec u \mode l; x)$ is true just if $A(\vec u \mode l ; \beta (q(l), 1 ; f(l, \vec u \mode l;) ))$ is true, where $q(l)$ is an upper bound for $f^\pi (l, \vec u \mode l ; )$.
+Now, since all $\vec u$ are normal, we may simply set $l$ to have a longer length than all of these arguments, so the function $f(\vec u;) \dfn \beta (q(\sum \vec u), 1 ; f(\vec u \mode \sum \vec u;) ))$ indeed witnesses the required existential.
 	\end{proof}
