Index: soundness.tex
===================================================================
--- soundness.tex	(revision 218)
+++ soundness.tex	(revision 219)
@@ -70,7 +70,9 @@
 	\]
 \end{definition}
 
+\anupam{Above and below definitions need to be with respect to a typing of variables which terms respect.}
 
+
 \begin{proposition}
 	$\charfn{}{A} (l, \vec u ; \vec x)$ is the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.
 \end{proposition}
@@ -78,21 +80,58 @@
 \begin{definition}
 	[Length bounded witness function]
 	We now define $\Wit{\vec u ; \vec x}{A} (l , \vec u ; \vec x)$ for a $\Sigma_{i+1}$-formula $A$ with free variables amongst $\vec u; \vec x$.
-	\[
-	\begin{array}{rcl}
-	\Wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w) & \dfn & \charfn{}{A} (l, \vec u ; \vec x)  \text{ if $A$ is $\Pi_i$} \\
-	\smallskip
-	\Wit{\vec u ; \vec x}{A \cor B} (l,\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cor ( ; \Wit{\vec u ; \vec x}{A} (l,\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (l,\vec u ; \vec x , \vec w^B)  )  \\
-	\smallskip
-	\Wit{\vec u ; \vec x}{A \cand B} (l,\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cand ( ; \Wit{\vec u ; \vec x}{A} (l,\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (l,\vec u ; \vec x , \vec w^B)  )  \\
-	\smallskip
-	\Wit{\vec u ; \vec x}{\exists x^\safe . A(x)} (l,\vec u ; \vec x , \vec w , w) & \dfn & \Wit{\vec u ; \vec x , x}{A(x)} ( l,\vec u ; \vec x , w , \vec w )
-	\\
-	\smallskip
-	\Wit{\vec u ; \vec x}{\forall u \leq |t(\vec u;)| . A(x)} (l , \vec u ; \vec x, w) & \dfn & 
-	\forall u \leq |t(\vec u;)| . \Wit{u , \vec u ; \vec x}{A(u)} (l, u , \vec u ; \vec x, \beta(u;w) )
-	\end{array}
-	\]
+	For a $\Sigma^\safe_i$ formula $A$ with free variables amongst $(\vec u ; \vec x)$, with $\vec x$ occurring only hereditarily safe in terms, we define the \emph{length-bounded witness function} $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w)$ 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 )$.
+		\item If $A$ is $B \cor C$ then 
+		\[
+		\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) 
+		\quad \dfn \quad
+		\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 ) )  )
+		\]
+		and we may set $b_A = O(b_B + b_C)$.
+		\item Similarly if $A $ is $B \cand C$, but with $\andfn$ in place of $\orfn$.
+%		\item If $A$ is $B \cand C$ then
+%			\[
+%			\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) 
+%			\quad \dfn \quad
+%			\andfn ( ; \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 ) )  )
+%			\]
+%			and we may set $b_A = O(b_B + b_C)$.
+		\item If $A$ is $\forall u \leq |t(\vec u;)| . B(u)$ then 
+		\[
+		\wit{\vec u ; \vec x}{A}
+		\quad \dfn\quad
+		\forall u\normal \leq |t|.
+		\wit{u, \vec u ; \vec x}{B(u)} (l, u, \vec u ; \vec x , \beta( b_{B(t)} (l) , u ; w ) )
+		\]
+		appealing to Lemma~\ref{lem:sharply-bounded-recursion}, where we may set $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
+		\[
+		\wit{\vec u ; \vec x}{A}
+		\quad \dfn \quad
+		\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 lemmata for $\wit{\vec u ; \vec x , x}{B(x)}$.
+		We may set $b_A = O(b_B + q )$.
+	\end{itemize}
+%	\[
+%	\begin{array}{rcl}
+%	\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w) & \dfn & \charfn{}{A} (l, \vec u ; \vec x)  \text{ if $A$ is $\Pi_i$} \\
+%	\smallskip
+%	\wit{\vec u ; \vec x}{A \cor B} (l,\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cor ( ; \wit{\vec u ; \vec x}{A} (l,\vec u ; \vec x , \vec w^A) ,\wit{\vec u ; \vec x}{B} (l,\vec u ; \vec x , \vec w^B)  )  \\
+%	\smallskip
+%	\wit{\vec u ; \vec x}{A \cand B} (l,\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cand ( ; \wit{\vec u ; \vec x}{A} (l,\vec u ; \vec x , \vec w^A) ,\wit{\vec u ; \vec x}{B} (l,\vec u ; \vec x , \vec w^B)  )  \\
+%	\smallskip
+%	\wit{\vec u ; \vec x}{\exists x^\safe . A(x)} (l,\vec u ; \vec x , \vec w , w) & \dfn & \wit{\vec u ; \vec x , x}{A(x)} ( l,\vec u ; \vec x , w , \vec w )
+%	\\
+%	\smallskip
+%	\wit{\vec u ; \vec x}{\forall u \leq |t(\vec u;)| . A(x)} (l , \vec u ; \vec x, w) & \dfn & 
+%	\forall u \leq |t(\vec u;)| . \wit{u , \vec u ; \vec x}{A(u)} (l, u , \vec u ; \vec x, \beta(u;w) )
+%	\end{array}
+%	\]
+%	\anupam{need length bounding for sharply bounded quantifiers}
 \end{definition}
 
 \anupam{may as well use a single witness variable since need it for sharply bounded quantifiers anyway.}
@@ -105,58 +144,156 @@
 	\anupam{check statement, need proof-theoretic version?}
 \end{proposition}
 
+By the polychecking lemma, we can assume that such a $w$ is bounded by some polynomial in $l$.
+
 In order to prove Thm.~\ref{thm:soundness} we need the following lemma:
 
 
+\paragraph*{Two properties needed}
+For below, need witnesses and functions bounded by a polynomial in $l$.
+
 \begin{lemma}
-	[Proof interpretation]
-	\label{lem:proof-interp}
-	For any $\arith^i$ proof of a $\Sigma^\safe_i$ sequent $\Gamma \seqar \Delta$, there is a $\mubci{i-1}$ function $f$ such that, for any $l, \vec u , \vec x  , w$, we have:
+		[Proof interpretation]
+		\label{lem:proof-interp}
+	From a normal form \todo{define, prove exists} $\arith^i$ proof $\pi$ of a $\Sigma^\safe_i$ sequent $\normal(\vec u), \safe(\vec x) , \Gamma  \seqar \Delta$
+	there are $\mubci{i-1}$ functions $\vec f^\pi (\vec u ; \vec x , w)$ (where $\vec f^\pi = (f^\pi_B)_{B\in\Delta}$) such that, for any $l, \vec u ; \vec x  , w$, we have:
 	\[
-	\wit{\vec u ; \vec x}{ \wedge \Gamma } (l, \vec u ; \vec x , w) 
-	\quad \leq \quad
-	\wit{\vec u ; \vec x}{\vee \Delta} (l, \vec u ; \vec x , f(l, \vec u ; \vec x , w))
+%	\vec a^\nu = \vec u ,
+%	\vec b^\sigma = \vec u, 
+	\bigwedge\limits_{A \in \Gamma} \wit{\vec u ; \vec x}{ A} (l, \vec u ; \vec x , w_A) =1
+	\quad \implies \quad
+	\bigvee\limits_{B\in \Delta} \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , f^\pi_B(\vec u \mode l ; \vec x \mode l, \vec w)) = 1
 	\]
-	\anupam{maybe want $f(\vec u \mode l ; \vec x \mode l , w)$}
-	\anupam{Also, perhaps split for formulae of $\Gamma$, to avoid lots of (de)coding}
+	\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.
+
 \begin{proof}
-	We assume the proof, say $\pi$, is in integer positive free-cut free form, by the results from the previous section.
-	This means that the predicate $\charfn{\vec u ; \vec x}{A}$ is defined for each formula $A(\vec u ; \vec x)$ occurring in a proof, so the theorem is well-stated.
+	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$.
 	
+	
 	\paragraph*{Negation}
 	Can assume only on atomic formulae, so no effect.	
+	
+	\paragraph*{Logical rules}
+	Pairing, depairing. Need length-boundedness.
+	
+	If we have 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}
+	\]
+		By inductive hypothesis we have functions $\vec f (\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) ))
+		\]
+	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)$.
+	
+	
+	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))}$.
 	\paragraph*{Quantifiers}
 	\anupam{Do $\exists$-right and $\forall$-right, left rules are symmetric.}
 	
+	
+	
+	Sharply bounded quantifiers are generalised versions of logical rules.
+	\[
+	\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)  }
+	\]
+	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  )$.
+	
+	
+	Right existential:
+	\[
+	\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)}
+	\]
+	Here we assume the variables of $t$ are amongst $(\vec u ; \vec x)$, since we are in typed variable normal form.
+
+	
 	\paragraph*{Contraction}
 	Left contraction simply duplicates an argument, whereas right contraction requires a conditional on a $\Sigma^\safe_i$ formula.
 
+	\[
+	\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:
+	 \[
+	 f^\pi_A ( \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)  )
+	 \]
+
+
+	\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:
+	Suppose final step is (wlog):
 	\[
-	\vlinf{\pind}{}{\Gamma , \normal (t) , A(0) \seqar A(t) , \Delta}{ \left\{\Gamma , \normal (u) , A(u) \seqar A(\succ i u ) , \Delta \right\}_{i=0,1} }
+	\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!}
 	
 		Now, by the inductive hypothesis, we have functions $h_i$ such that:
 		\[
-		\wit{u , \vec u ; \vec x}{LHS} (l , u , \vec u ; \vec x ,  w) =1
+		\Wit{u , \vec u ; \vec x}{\Gamma, A(0)} (l , u , \vec u ; \vec x ,  \vec w)
 		\quad \implies \quad
-		\wit{u , \vec u ; \vec x}{RHS} (l , u , \vec u ; \vec x ,  h_i (u \mode l , \vec u \mode l ; \vec x \mode l) ) =1
+		\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) )
 		\]
-	We define $ f$ as follows:
+	First let us define $ f$ as follows:
 	\[
 	\begin{array}{rcl}
-	 f (0 , \vec u ; \vec x, \vec w^\Gamma , w^{\normal (t)} , w^{A(0)}) & \dfn &  w^{A(0)} \\
-	 f( \succ i u , \vec u ; \vec x , \vec w^\Gamma , w^{\normal (t)} , w^{A(0)}) & \dfn & 
-	 h_i (u , \vec u ; \vec x , \vec w^\Gamma w^{\normal (?)}, f(u , \vec u ; \vec x , \vec w ))
+	 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 ))
 	\end{array}
 	\]
-	\anupam{Must check above, could be problems in recursive case.}
+	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)$.
+	
+	\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':
+	\[
+	\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:
+	\[
+	\vec f^\pi ( \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 )
+	\]
 \end{proof}
 
 We are now ready to prove the soundness theorem.
