Index: appendix-soundness.tex
===================================================================
--- appendix-soundness.tex	(revision 253)
+++ appendix-soundness.tex	(revision 254)
@@ -1,164 +1,2 @@
-\section{Proof of soundness}
+%\section{Proof of soundness}
 
-\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.
-	%	If $A$ is a $\Pi_{i}$ formula then:
-	\[
-	\begin{array}{rcl}
-	\charfn{\vec u ; \vec x}{s\leq t} (l, \vec u ; \vec x) & \dfn & \leqfn(l;s,t) \\
-	\smallskip
-	%	\charfn{}{s=t} (l, \vec u ; \vec x) & \dfn & \eq(l;s,t) \\
-	%	\smallskip
-	\charfn{\vec u ; \vec x}{\neg A} (l, \vec u ; \vec x) & \dfn & \notfn (;\charfn{\vec u ; \vec x}{A}(l , \vec u ; \vec x)) \\
-	\smallskip
-	\charfn{\vec u ; \vec x}{A\cor B} (l, \vec u ; \vec x ) & \dfn & \orfn(; \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w), \charfn{\vec u ; \vec x}{B} (\vec u ;\vec x) ) \\
-	\smallskip
-	\charfn{\vec u ; \vec x}{A\cand B} (l, \vec u ; \vec x ) & \dfn & \andfn(; \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w), \charfn{\vec u ; \vec x}{B} (\vec u ;\vec x) )
-	%	\end{array}
-	%	\quad
-	%	\begin{array}{rcl}
-	\\	\smallskip
-	\charfn{\vec u ; \vec x}{\exists x^\safe . A(x)} (l, \vec u ;\vec x) & \dfn & \begin{cases}
-	1 & \exists x^\safe . \charfn{}{A(x)} (l, \vec u ;\vec x , x) = 1 \\
-	0 & \text{otherwise} 
-	\end{cases} \\
-	\smallskip
-	\charfn{\vec u ; \vec x}{\forall x^\safe . A(x)} (l, \vec u ;\vec x ) & \dfn & 
-	\begin{cases}
-	0 & \exists x^\sigma. \charfn{\vec u ; \vec x}{ A(x)} (l, \vec u; \vec x , x) = 0 \\
-	1 & \text{otherwise}
-	\end{cases}
-	\end{array}
-	\]
-\end{definition}
-
-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}
-	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 (wlog):
-	\[
-	\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}{\Gamma, A(0)} (l , u , \vec u ; \vec x ,  \vec 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) )
-	\]
-	First let us define $ f$ 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 ))
-	\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.}
-	
-	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}
-	
