\newcommand{\lgf}{\Lambda;\Phi;\Gamma\vd}
\newcommand{\fg}{\Phi;\Gamma\vd}
\newcommand{\mapd}{\stackrel{D}{\mapsto}}
\newcommand{\mapg}{\stackrel{G}{\mapsto}}
We present in Figure \ref{fig:inputerm} the rules for normalization
\wrt input variables; this is realized by the judgments:
\begin{itemize}
\item $\D\mapd D'$: clause normalization.
\item $\ga\vd_{\Phi} G\mapg G'$: goal normalization.
\item $\fg D\mapsto D'$: assumption normalization.
\item $\lgf M\mapsto M',E$: term normalization.
\end{itemize}
The first three simply recur, keeping track of bound ($\GG$), global
$\Phi$ and existential variables in assumptions $\Lambda$, until we
normalize an assumption $\Pi (Q\If G)$: here we rewrite every term by
introducing new local existential variable and binding them to the
global one by an equation $E$. For the sake of conciseness, we do
this for the simply-typed fragment; the generalization to the strict
one is immediate.


\begin{figure}
\newcommand{\vdfg}{\vd_{\Phi}}
\renewcommand{\glob}{[\rho]}
  \[
  \begin{array}{c}
    \ibnc{D_1\mapd D_1'}{D_2\mapd D_2'}
    {D_{1}\And D_{2}\mapd D_{1}'\And D_{2}'}{\mapd\And}\qquad
    \ibnc{D_1\mapd D_1'}{D_2\mapd D_2 '}
    {D_{1}\tensor D_{2}\mapd D_{1}'\tensor
    D_{2}'}{\mapd\tensor}\vsk
    \ianc{X\in\{ \top,\perp\}}{X\mapd  X}{\mapd X}\qquad
 \ianc{\cdot;\top\vd_{\dom(\rho)}\glob G\mapg \glob G'}{\Pi(Q\If G) 
 \mapd\Pi(Q \If G')}{\mapd\If^{\rho}}
\vsk\vsk
  \ianc{X\in\{ \top,\perp, Q\} \mbox{ or  (dis)eq}}{\ga\vdfg X\mapg
    X}{\mapg X}\qquad
  \ianc{\GG,y\oftp A);\cD\vdfg [y/x]G\mapg [y/x]G'}{\ga\vdfg \PIXA
  G\mapg  \PIXA G'}{\mapg\Pi^y}\vsk
  \ibnc{\fg D\mapsto D'}
{\GG;\cD\And D\vdfg G\mapg G'}{\ga\vdfg (D\Imp  G)\mapg (D'\Imp
  G')}{\mapg\Imp}\vsk
 \ibnc{\ga\vdfg G_1\mapg  G_1'}{\ga\vdfg G_2\mapg  G_2 '}
    {\ga\vdfg G_{1}\And G_{2}\mapg  G_{1}'\And G_{2}'}{\mapg\And}\qquad
    \ibnc{\ga\vdfg G_1\mapg  G_1'}{\ga\vdfg G_2\mapg   G_2 '}
    {\ga\vdfg G_{1}\Or G_{2}\mapg  G_{1}'\Or
    G_{2}'}{\mapg\Or}\vsk\vsk
    \ianc{}{\Lambda;\Phi;(\GG,\xoa)\vd x\mapsto x}{bv}\qquad
    \ianc{Z \mbox{ new}}{\Lambda;(\Phi,u\oftp A);\GG\vd u\mapsto u,
    Z\eqd u}{iv}\qquad
    \ianc{}{(\Lambda,\xoa);\Phi;\GG\vd x\mapsto x}{lv}\vsk
  \ibnc{\lgf M_1\mapsto M'_1,E_1}{\lgf M_2\mapsto M'_2,E_2}{\lgf M_1\
    M_2\mapsto M_1'\ M_2', E_1\And E_2}{App}\qquad
  \ianc{\Lambda;\Phi;(\Gamma,\xoa)\vd M\mapsto M', E}{\lgf\lamb{x}{A}
    M\mapsto M', E}{\l}
  \vsk\vsk
  \ianc{\Lambda=FV(\Mn)\setminus(\GG\cup\Phi)\qquad \lgf M_1\mapsto
    M_1',E_1\dots \lgf M_n\mapsto M_n',E_n}{\fg\Pi(q\ \Mn\If G)\mapsto
    \Pi(q\ \ol{M'_n}\If E_1\And\dots\And E_n\And G)}{\mapsto\Imp}\vsk 
 \ianc{X\in\{ \top,\perp\}}{\fg X\mapsto X}{\mapsto X}\vsk
    \ibnc{\fg D_1\mapsto D_1'}{\fg D_2\mapsto D_2'}
    {\fg D_{1}\And D_{2}  \mapsto D_{1}'\And D_{2}'}{\mapsto\And}\qquad
    \ibnc{\fg D_1\mapsto D_1'}{\fg D_2\mapsto D_2 '}
    {\fg D_{1}\tensor D_{2}  \mapsto D_{1}'\tensor
    D_{2}'}{\mapsto\tensor}\vsk
  \end{array}
  \]
  \caption{Clause, goal and assumption normalization}
  \label{fig:inputterm}
\end{figure}


It is clear, although very tedious, to verify that this transformation
preserves provability and denial\ednote{Add the statement of the theorem}.





