%\subsection{$\top$ Normalization}

 \newcommand{\tend}[1]{ #1^{\top}}
 \newcommand{\teng}[1]{ #1^{\top} }
% \newcommand{\teng}[1]{\mid #1 \mid_{G} }
% \newcommand{\tenx}[1]{\mid #1 \mid_{\Pi} }


We show in this Section how to put every program in a normalized
format \wrt assumptions so that every goal in the scope of an
universal quantifier depends on some assumption, at worst the trivial
clause $\top$. This has also the effect of ``localizing'' the trivial
assumption to its atom, a property will be very useful while
performing augmentation, see Section \ref{sec:aug}.


% \begin{Definition}[$\top$ Normalization]
% \label{def:standardtop}
% \[\begin{array}{rclr}
% \tenx{X} & = & X & X\in\{\top,\perp,\mbox{(dis)eq}\}\\
% \tenx{\PIXA Q}& = &  \PIXA \top_Q\Imp Q\\
% \tenx{\PIXA \PI{y}{B}G} & = & \PIXA\tenx{\PI{y}{B}G}\\
% \tenx{\PIXA   G_{1}\And G_{2}}&=& \tenx{\PIXA G_1}\And \tenx{\PIXA G_2'}\\
% \tenx{\PIXA   G_{1}\Or G_{2}}&=& \tenx{\PIXA G_1}\Or \tenx{\PIXA G_2'}\\
% \tenx{\PIXA D\Imp G} & = & \PIXA\tend{D}\Imp\teng{G}\\
% \tend{X} & = & X & X\in\{\top,\perp,Q\}\\
% \mid D\If G\mid_{D} & = & \tend{D}\If \teng{G}\\
% \mid D_{1}\And D_{2} \mid_{D} & = & \mid D_{1} 
% \mid_{D}\And \mid D_{2} \mid_{D} \\
% \mid \PIXA D \mid_{D} & = & \PIXA  \mid D \mid_{D} \\
% \mid D_{1}\tensor D_{2} \mid_{D} & = & \mid D \mid_{D} \tensor \tend{D}\\
% \teng{X} & = & X & X\in\{\top,\perp,Q,\mbox{(dis)eq}\}\\
% \teng{G_1\And G_2} & = & \teng{G_1}\And \teng{G_2}\\
% \teng{G_1\Or G_2} & = & \teng{G_1}\Or \teng{G_2}\\
% \teng{D\Imp G} & = & \tend{D}\Imp\teng{G}\\
% \teng{\PIXA G} & = & \tenx{\PIXA G}\\
% \teng{\exa G} & = & \exa\teng{G}
% \end{array}\]
% \end{Definition}

\begin{figure}[htbp]
  \label{fig:topnormal}
\[
\begin{array}{c}
  \ianc{X\in\{\top,\perp\}\mbox{ or (dis)eq}}{\ga\vd
  X\yg X}{\yg X}\qquad 
\ianc{}{\emp\vd Q\yg Q}{\atm\emp}\qquad
\ianc{\cD\not\equiv\top}{\ga\vd Q\yg Q}{\atm\ga}\vsk
\ianc{x \mbox{ relevant to } Q}{(\GG,\xoa);\top\vd Q\yg \top_Q\Imp
  Q}{\atm\top\mbox{ rel}}\qquad
\ianc{x \mbox{ not relevant to } Q}{(\GG,\xoa);\top\vd Q\yg
  Q}{\atm\top\mbox{non-rel}}\vsk
\ibnc{ \GG;(\cD\And D)\vd G\yg \teng{G}}{D\yd \tend{D}}{ \ga \vd
  D\Imp G\yg \tend{D}\Imp \teng{G}}{ \yg\Imp}\vsk
\ianc{(\GG,y\oftp A);\cD\vd[y/x] G\yg  [y/x]\teng{G}}{ \ga\vd\PIXA
  G\yg \PIXA\teng{G}}{ \yg\Pi^y}\vsk 
\ianc{\GG;\cD\vd[u/x] G\yg [u/x]\teng{G}}{ \ga\vd\exa G\yg \exa\teng{G}}{ \yg\exists^y}\vsk 
\ibnc{ \ga \vd G_1 \yg  \teng{G}_1}{\ga\vd G_2\yg \teng{G}_2} { \ga\vd G_{1}\And
  G_{2} \yg \teng{G}_1\And \teng{G}_2}{ \yg\And}\vsk 
\ibnc{ \ga \vd G_1 \yg \teng{G}_1}{\ga\vd G_2\yg \teng{G}_2} { \ga\vd
  G_{1}\Or G_{2} \yg \teng{G}_1\Or \teng{G}_2}{ \yg\Or}\vsk \vsk

% \ianc{}{\top\yd \cdot;\top}{\yd \top} \qquad
 % \ianc{}{\perp\yd \cdot;\top}{\yd \perp} \vsk
\ianc{X\in\{Q,\top,\perp\} }{X\yd X}{\yd X} \vsk
%  \ianc{\cdot;\top\vd G\yg \cS} {(G\Imp Q)\yd \cS}{ \yd\Imp} Q\If G syntax
  \ibnc{\cdot;\top\vd G\yg \teng{G}_1}{D\yd \tend{D}_2} {(G\Imp  D)\yd \teng{G}\Imp \tend{D}}{ \yd\Imp}\vsk
  \ianc{ [u/x]D\yd [u/x]\tend{D}}{ \PIXA D\yd \PIXA\tend{D}}{ \yd\Pi^y}\vsk 
\ibnc{ D_1 \yd \tend{D}_1}{D_2\yd \tend{D}_2} { D_{1} \And D_{2} \yd
  \tend{D}_1\And \tend{D}_2}{ \yd\And}\vsk
\ibnc{ D_1 \yd \tend{D}_1}{D_2\yd \tend{D}_2} { D_{1} \tensor D_{2} \yd
  \tend{D}_1\tensor \tend{D}_2}{ \yd\tensor}
 

 \end{array}
\]
  \caption{$\top$-Normalization}
\end{figure}

The proof obligation consists in showing that this transformation
preserves provability and denial.

\begin{Theorem}
\label{thm:topnormalvdlr}
\mbox{}
\renewcommand{\ga}{\GG;\q\cD}
\ben
\item  If $\ga\vd \q G$ and $\GG';\cD'\vd G\yg G^{\top}$ then $\ga\vd\q\teng{ G}$.
\item  If $\ga\vd\q  D\imm\q Q$ and $D\yd \tend{D}$ then $\ga\vd\q\tend{ D}\imm\q Q$.
\enen
\end{Theorem}


\begin{proof}
\renewcommand{\ga}{\GG;\q\cD}
By mutual induction on the structure of the derivation of
$\gamma::\ga\vd\q G$  and inversion on $\gamma'::\GG';\cD' G\yg\teng{G}$
together  $\delta ::\ga\vd\q D\imm\q Q$ and inversion on 
$\delta'::D\yd \tend{D}$. We sketch only some cases:
\bit
\itc 
$\gamma$ ends in $\vd\atm$ and $\gamma'$ is $\yg X,\yg\atm\emp,\yg\ga,\atm\top\mbox{ non-rel}$: trivial.
\itc
$\gamma$ ends in $\vd\atm$ and $\gamma'$ ends in $\atm\top\mbox{ rel}$:
\btab
$\ga\vd\q Q$\bh
$\ga\vd\q D\imm\q Q$\bs
$\GG;(\cD\And \top_Q)\vd\q D\imm \q Q$\` By Weakening\\
$\ga\vd\top_Q\Imp\q Q$\br $\vd\Imp$\\
$\ga\vd\teng{Q}$\br $\atm\top\mbox{ rel}$:
\etab
\enit
\end{proof}


\begin{Theorem}
\label{thm:topnormalvdrl}
\renewcommand{\ga}{\GG;\q\cD}
\mbox{}
\ben
\item   $\ga\vd \q G$ if $\GG';\cD'\vd G\yg G^{\top}$ and $\ga\vd\q\teng{ G}$.
\item   $\ga\vd\q  D\imm\q Q$ if $D\yd \tend{D}$ and $\ga\vd\q\tend{ D}\imm\q Q$.
\enen
\end{Theorem}
\begin{proof}
\renewcommand{\ga}{\GG;\q\cD}
By mutual induction on the structure of $\gamma::\ga\vd\q\teng{ G}$ and
$\delta::\ga\vd\q\tend{ D}\imm\q Q$,  as above but using $\top$-Strenghtening
(Lemma \ref{le:topstren}) in place of Weakening. 

\end{proof}

An analogous result can be proven \wrt failure; the latter would
require $\top$-Weakening and Strengthening \wrt the (immediate) denial
relation. On the other hand, the above will suffice, if we restrict to
terminating programs as we do next.







