\section{Augmentation}
\label{sec:aug}

% \bmeta
% The $\dsat$ judgment has \emph{no} context
% \emeta


\renewcommand{\gfald}{\ald}
\renewcommand{\emp}{\cdot;\top}
\newcommand{\vdfg}{\vd}
\renewcommand{\vdf}{\vd}
Now that we have discussed how to perform clause, assumption and goal
complementation, we synchronize it together in a phase we call
\emph{augmentation}, which simply insert the correct assumption
complementation in a goal and in turn in a clause. We give
one judgment to augment a program, $\gfald(D)$, which merely
recurs on the structure of clauses until it calls goal augmentation,
$\ga\vdfg\alg(G)$. The latter traverses a goal collecting
parameters in $\GG$ and assumptions in $\cD$. When it reaches an atom,
either it stops, as no parameter has been introduced, or it passes
$\GG,\cD$ to assumption complementation. Some examples will make the whole process clear:

\begin{figure}
  \[
  \begin{array}{c}
    \ianc{X\in\{ \top,\perp\}}{\gfald(X)  =  X}{\ald X}\vsk
    \ibnc{\gfald(D_1) = D_1^a}{\gfald(D_2) = D_2^a}
    {\gfald(D_{1}\And D_{2})  = D_{1}^a\And D_{2}^a}{\ald\And}\vsk
    \ibnc{\gfald(D_1) = D_1^a}{\gfald(D_2) = D_2 ^a}
    {\gfald(D_{1}\tensor D_{2})  = D_{1}^a\tensor
    D_{2}^a}{\ald\tensor}\vsk
  \ianc { \ald([u/x]D)=[u/x]D^a}
  {\gfald(\PIXA D)=\PIXA D^a}{\ald\Pi^u}\vsk
% OK AS SECOND-ORDER
    \ibnc{\ald(D)=D^a}{\cdot;\top\vdfg\alg(G) = G_a}{\gfald(D\If G )= D^a \If G_a}{\ald\If}
%    \ianc{\ga\vdfg\alg(G) = G_a}{\gfald(Q\If G )= Q \If G_a}{\ald\If}
  \end{array}
  \]
  \caption{Clause Augmentation: $\gfald(D) = D^a$}
  \label{fig:augd}
\end{figure}


\begin{figure}

\[
\begin{array}{c}
  \ianc{X\in\{ \top,\perp\} \mbox{ or  (dis)eq}}{\ga\vdfg\alg(X)=X}{\alg X}\vsk
 %  \ianc{}{\ga\vdfg\alg(\top)=\top}{\alg\top}\vsk  %% CHECK!!
%    \ianc{}{\ga\vdfg\alg(\bot)=\bot}{\alg\bot}\vsk
%   \ianc{}{\ga\vdfg\alg(\vM\eqd\vN)=(\vM\eqd\vN)}{\alg\eqd}\vsk
%   \ianc{}{\ga\vdfg\alg(\vM\neqd\vN)=(\vM\neqd\vN)}{\alg\neqd}\vsk
\ianc{}{\cdot;\top\vdfg\alg(Q)=Q}{\alg\atm^\top}\vsk
  \ianc{\GG\vdf\mnota(\cD)=\cD_{\neg}}{\ga\vdfg\alg(Q)  =\cD_{\neg}\Imp Q}{\alg At}\vsk
%OK second-order
  \ianc{\GG;(\cD\And D)\vdfg\alg(G)=G^a}{\ga\vdfg\alg(D\Imp  G)=D\Imp
  G^a}{\alg\Imp}\vsk
%  \ibnc{\gfald(D)=D^a}{\GG;(\cD\And D)\vdfg\alg(G)=G^a}
%{\ga\vdfg\alg(D\Imp  G)=D^a\Imp G^a}{\alg\Imp}\vsk
  \ianc{(\GG,y\oftp A);\cD\vdfg\alg([y/x]G)=[y/x]G^a}{\ga\vdfg\alg(\PIXA
  G)= \PIXA G^a}{\alg\Pi^y}\vsk
\ianc{\ga\vdfg\alg([u/x]G)=[u/x]G^a}{\ga\vdfg\alg(\exa G)=\exa G^a}{\alg\exists^u}\vsk
 \ibnc{\ga\vdfg\alg(G_1) = G_1^a}{\ga\vdfg\alg(G_2) = G_2 ^a}
    {\ga\vdfg\alg(G_{1}\And G_{2})  = G_{1}^a\And G_{2}^a}{\alg\And}\vsk
    \ibnc{\ga\vdfg\alg(G_1) = G_1^a}{\ga\vdfg\alg(G_2) = G_2 ^a}
    {\ga\vdfg\alg(G_{1}\Or G_{2})  = G_{1}^a\Or
    G_{2}^a}{\alg\Or}\vsk
 %  \ianc{}{\ga\vdfg\alg(\vM\eqd\vN)=\vM\eqd\vN}{\alg\eqd}\vsk
%   \ianc{}{\ga\vdfg\alg(\vM\neqd\vN)=\vM\neqd\vN}{\alg\neqd}
\end{array}
\]
\caption{Goal Augmentation: $\ga\vdfg\alg(G)= G_a$}
\label{fig:augg}
\end{figure}

\newcommand{\qqquad}{\qquad\qquad}


\begin{Example}
 Consider the \texttt{copy} program on $\l$-terms:
\beq
cpapp &:& \PI{E_1,E_2,F_1,F_2}{exp}\\
& & copy\ (app\ E_{1}E_{2}) \ (app\ F_{1}F_{2})\\
&& \qquad\If  copy\ E_{1} \ F_{1}\\ 
&& \qquad\If copy\ E_{2}\ F_{2}.\\
cplam &:& \PI{E}{exp\Imp exp}\PI{F}{exp\Imp exp} \\
& & copy\ (lam\ E) \ (lam\ F)\\
& & \qquad\If (\PI
{x}{ exp} copy\ x\ x\\
%{x}{ exp}\PI{y}{exp} copy\ x\ y\\
& & \qquad\qquad\Imp copy\ (E\ x) \ (F\ x)).
%& & \qquad\qquad\Imp copy\ (E\ x) \ (F\ y)).
\eneq
The augmentation procedure $\ald(cplam)$ yields $\alg(\PI
{x}{ exp} copy\ x\ x\Imp copy\ (E\ x) \ (F\ x))$,
 which collects $x\oftp exp; copy\ x\ x$ and 
 calls $x\oftp exp\vd \mnota( copy\ x\ x)$.
%, glossing over the context $\Phi$ which
%is not active in this case.
 First
$ \mnot^x_1(copy\ x\ x)= (\PI{E'}{exp} \neg copy\ E'\ x\If
x\neqd E')$, secondly $
 \mnot^x_2(copy\ x\ x)= (\PI{F'}{exp} \neg copy\ x\ F'\If x\neqd F')$, yielding:
% First
% $ \mnot^x_1(copy\ x\ y= (\PI{E'}{exp} \neg copy\ E'\ y\If
% x\neqd E')$, secondly $
%  \mnot^y_2(copy\ x\ y)= (\PI{F'}{exp} \neg copy\ x\ F'\If y\neqd F')$, yielding:
\beq
\ald(cplam)&:& \PI{E}{exp\Imp exp}\PI{F}{exp\Imp exp} \\
& &  copy\ (lam\ E) \ (lam\ F)\\
& & \qquad \If (\PI{x}{ exp}\\
& & \qquad\qquad (\PI{E'}{exp} \neg copy\ E'\ x\If x\neqd E')\And\\
& & \qquad\qquad (\PI{F'}{exp} \neg copy\ x\ F'\If x\neqd F')\Imp\\
&& \qquad\qquad\qquad
 copy\ x\ x \Imp copy\ (E\ x) \ (F\ x)).
% & & \qquad \PI{x}{exp}\PI {y}{ exp}\\
% & & \qquad (\PI{E'}{exp} \neg copy\ E'\ y\If x\neqd E')\And\\
% & & \qquad (\PI{F'}{exp} \neg copy\ x\ F'\If y\neqd F')\Imp\\
% && \qquad\qquad
%  copy\ x\ y) \Imp copy\ (E\ x) \ (F\ y)
\eneq
while of course, $\ald(cpapp)=cpapp$, as enforced by $\alg \atm\top$. If
we had a two-parameter version of $copy$,  \ie
\beq
cplam' &:& \PI{E}{exp\Imp exp}\PI{F}{exp\Imp exp} \\
& & copy'\ (lam\ E) \ (lam\ F)\\
& & \qquad \If(\PI{x}{ exp}\PI{y} {exp}  (copy'\ x\ y)\\
& & \qquad\qquad\Imp copy'\ (E\ x) \ (F\ y)).
\eneq
Then we would get four calls, namely to:
\beq
  \mnot^x_1(copy'\ x\ y)& = &
(\PI{E'}{exp} \neg copy'\ x\ E'\If x\neqd E')\\
  \mnot^x_2(copy'\ 
x\ y)& = & (\PI{E''}{exp} \neg copy'\ E''\ x\If x\neqd E'')\\
\mnot^y_1(copy'\ x\ y)& = & (\PI{F'}{exp} \neg copy'\ x\ F'\If y\neqd F')\\
 \mnot^y_2(copy'\ x\ y)& = & (\PI{F''}{exp} \neg copy'\ F''\ y\If y\neqd F'')
\eneq
yielding the augmented clause:
\beq
\ald(cplam')&:& \PI{E}{exp\Imp exp}\PI{F}{exp\Imp exp} \\
& &  copy'\ (lam\ E) \ (lam\ F) \\
& & \qquad\If ( \PI{x}{exp} \PI{x}{exp}\\
& & \qquad\qquad (\PI{E'}{exp} \neg copy'\ E'\ x\If x\neqd E')\And\\
& & \qquad\qquad (\PI{E''}{exp} \neg copy'\ x\ E''\If
x\neqd E')\And\\
& & \qquad\qquad (\PI{F'}{exp} \neg copy'\ x\ F'\If x\neqd F')\And\\
& & \qquad \qquad(\PI{F''}{exp} \neg copy'\ F''\ y\If y\neqd F'') \Imp\\
&& \qquad\qquad
 copy'\ x\ y \Imp copy'\ (E\ x) \ (F\ y)).
\eneq
Note that by static analysis of  \texttt{copy'}, we know that $x$
will never end up in the second argument of \texttt{copy'} and
symmetrically this applies to $y$, too. Thus the call to
$\mnot^x_2,\mnot^y_1$ are useless; however since this kind of data
flow analysis is in general undecidable, the augmentation procedure
inserts the negation of a clause for every position relevant to the
pivot parameter.

Take the typing clause for lambda terms:
\beq
oflam &:&  \PI{E}{exp\Imp exp}\PI{T1,T2}{tp}\\
&& of\ lam(E) \ arrow(T1,T2)\\
& & \qquad\If( \PI{x}{exp} of\ x\ T1 \Imp  of\ (E\ x) \ T2).
\eneq
As $T1$ is an input term, the correspondent diseqution is inserted:
\beq
\ald(oflam) &:& \PI{E}{exp\Imp exp}\PI{T1,T2}{tp}\\
&& of\ lam(E) \ arrow(T1,T2)\\
& & \qquad \If(\PI{x}{exp} of\ x\ T1 \Imp\\
& &\qqquad (\PI{T}{tp} \neg of\ x\ T\If T\neqd T1)\Imp\\
&&\qqquad\qquad  of\ (E\ x) \ T2).
\eneq

Consider now a predicate to perform instantiation of a binding
operator (in the pattern fragment):
\beq
inlam & : & \PI {E}{exp\Imp exp} \PI {F} {exp} \\
& & inst\ (lam\ E) \ F\\
& &  \qquad\If(\PI {x}{exp} (\PI {H}{exp} copy\ x\ H)\\
& & \qqquad  \Imp copy\ (E\ x)  \ F).
\eneq
The call to $x\oftp exp\vd\mnota (\PI {H}{exp}
copy\ x\ H)$ leads to $\mnot_x^1(\PI {H}{exp}
copy\ x\ H)$, which yields the unsatisfiable clause $\PI{H}{exp}\PI{Z}{exp}
\neg copy\ x\ Z\If Z\neqd H$, while $\mnot_x^2(\PI {H}{exp}
copy\ x\ H)$ yields  $\PI{Z}{exp}
\neg copy\ x\ Z\If Z\neqd x$. The augmentation will simply to
\beq
\ald(inlam) & : & \PI {E}{exp\Imp exp} \PI {F} {exp} \\
& & inst\ (lam\ E) \ F\\
& &  \qquad\If(\PI {x}{exp} (\PI {H}{exp} copy\ x\ H)\And\\
& & \qquad (\PI{Z}{exp}\neg copy\ x\ Z\If Z\neqd x)\\
& & \qqquad  \Imp copy\ (E\ x)  \ F).
\eneq

Let us see how rule $\mnotxi\top$ enters the picture: recall the
$\top$-normalized \texttt{linx} lambda clause:
\beq
linxlam &: & \PI{ E}{ exp\Imp exp\Imp exp} \\
& & linx\ (\lx lam(\ly  E\ x\ y)) \\
& & \qquad \If( \PI {z} {exp} \top_{linx}\Imp linx\ (\lx E\ x\ z)).
\eneq
The judgment
$z\oftp exp;\top_{linx}\vdfg\alg( linx\ E\ x\ z)$
triggers the rule $\mnotxi\top$; in turn $\cdot\vd sh(z,exp\Imp exp)=\ly z$
and  thus $\mnot^z_1(\top_{linx})= \neg linx\ (\lx z)$:
\beq
\ald(linxlam)&:& \PI{ E}{ exp\Imp exp\Imp exp}\\
& &  linx\ (\lx lam(\ly  E\ x\ y))\\
& & \qquad \If(\PI {z } {exp} \neg linx\ (\lx z)\Imp linx\ (\lx E\ x\ z)).
\eneq
\end{Example}


\bigskip
We prove that augmented clauses and goals satisfy the augmented
schema, where we define $\GG;\ald(\cD)$ as $\GG;\cD\And\neg\cD$, for
$\GG\vd\mnota(\cD)=\neg\cD$ and 
\[\begin{array}{c}
\ianc{}{aug(\ecs)=\ecs}{aug\ecs}\vsk
\ibnc{aug(\cS)=\csa} {\gfald(\cD)=\cD^a}
{aug(\cS\bar(\GG;\some{\Phi}\cD))= \csa\bar(\GG;\some{\Phi} \cD^a)}{aug\bar}
\end{array}\]

Now, the usual lemma on schema membership:

\begin{Lemma}
\label{le:inaug}
If $\ga\in\cS$ then $\GG;\ald(\cD)\in aug(\cS)$.
\end{Lemma}
\begin{proof}
By  induction on the structure of $\pi::\ga\in\cS$.
\bit
\itc $$\pi=\ianc{(\GG';\cD')\equiv_{\alpha}(\GG;\q\cD)}{(\GG';\cD')\in \cS\bar
(\GG;\some{\Phi} \cD)}{\in_1}$$
\btab
$\gap\equiv_{\alpha}\GG;\q\cD$\bs
$\GG';\ald(\cD')\equiv_{\alpha}\GG;\q\ \ald(\cD)$\` By definition\\
$\GG';\ald(\cD')\in aug(\cS)\bar\GG;\some{\Phi} \ald(\cD)$\br $\in_1$\\
%$\GG';\ald(\cD')\in aug(\cS)\bar\GG;aug(\some{\Phi} \cD)$\br\\
$\GG';\ald(\cD')\in aug(\cS\bar\GG;\some{\Phi} \cD)$\br $aug\bar$
\etab
\itc $\pi$ ends in $\in_2$: by IH.
\enit
\end{proof}

\renewcommand{\dsats}{\models_{\!\csa}}
\newcommand{\gda}{\ga}
\renewcommand{\insss}{\ins\csa}
\newcommand{\bg}{\block{\Gamma'}}
%\newcommand{\bd}{\block{\cD'}}

\newcommand{\gdains}{\GG;\ald(\cD)\ins}

We use $\dsats\ald(D)$ for $\vdf\ald(D)=D_a$ and $\dsats
D^a$; analogously for $\alg(G)$.

\begin{Lemma}[Schema Augmentation]
\label{le:saug}
Let $\ga\inss$ and $aug(S)=\csa$. Then:
\ben
\item If $\dsat D$, then $\dsats \ald(D)$.
\item If $\ga\sla G\inss$, then $\gda\sla \alg(G)\insss$.
\item If $\ga\ins\cS$ then $\gdains \csa$.
\enen
\end{Lemma}

\begin{proof}
By mutual induction on the structure of $\pi::\  \dsat D$, $\gamma
::\ga\sla G\inss$ and  $\sigma::\ga\ins\cS$. We show the crucial cases:
\bit
\itc $$\pi=\ianc{X\in\{Q,\top,\perp\}}{\dsat X}{\dsat X}$$
Immediately $\ga\vd\ald(X)=X$ and 
$$\pi'=\ianc{X\in\ \{Q,\top,\perp\}}{\dsats X}{\dsat X}$$

\itc$$\pi=\ibnc{\dsat D}{\emp\sla G\inss}{\dsat G\Imp  D}{\dsat\Imp}$$
\btab
$\dsat D$\bs
$\dsats \ald(D)$\bi $1$\\
$\emp\sla G\inss$\bs
$\emp\sla \alg(G)\insss$\bi $2$\\
$\dsats \alg(G)\Imp \ald(D)$\br $\dsat\Imp$\\
$\dsats \ald(G\Imp D)$\br $\ald\Imp$
\etab
\itc $$\gamma=\ibnc{X\in\{\top,\perp\}\mbox{ or (dis)eq}}{\ga\inss}
{\ga\sla X\inss}{\sla X}$$
\btab
$\ga\inss$\bs
$\GG;\ald(\cD)\insss$\bi $3$\\
$\ga\vd\alg(X)=X$\br $\alg X$\\
$\GG;\ald(\cD)\sla X\insss$\br $\sla X$
\etab
\itc $$\gamma= \ianc{\ga\inss}{\ga\sla Q\inss}{\sla\atm}$$
\bit
\item[Subcase]
\btab
$\cdot;\top\inss$\bs
%$\cdot;\top\vdf\ald(\top)=\top$\br $\ald\top$\\
$\cdot;\top\insss$\br $\ins_1$\\
$\emp\vd Q\insss$\br $\alg\atm\top$\\ 
$\emp\sla\alg(Q)\insss$\br $\sla\atm$
\etab
\item[Subcase]
\btab
$\ga\inss$\bs
$\GG;\ald(\cD)\insss$\bi $3$\\
$\GG;\ald(\cD)\sla Q\insss$\br $\sla Q$\\
$\GG;\cD\And \mnota(\cD)\sla Q\insss$ \` By
def.\ of $\ald(\cD)$\\
$\GG;\cD\sla\ \mnota(\cD)\Imp Q\insss$\br $\alg\atm$\\
$\GG;\cD\sla\alg(Q)\insss$\br $\sla\Imp$
\etab
\enit
\itc$$\gamma=\ibnc{\dsat D}{\GG;\cD\And D\sla G\inss}{\ga\sla D\Imp
  G\inss}{\sla\Imp}$$
\btab
$\dsat D$\bs
$\dsats \ald(D)$\bi $1$\\
$\GG;\cD\And D\sla G\inss$\bs
$\GG;\cD\And D\sla \alg(G)\insss$\bi $2$\\
$\gda\sla D\Imp \alg(G)\insss$\br $\sla\Imp$\\
$\gda\sla \alg(D\Imp G)\insss$\br $\alg\Imp$
\etab
\itc $$\sigma=\ianc{}{\cdot;\top\ins \cS}{\ins_1}$$
Then immediately:
 $$\sigma'=\ianc{}{\cdot;\top\ins \csa}{\ins_1}$$
\itc$$\sigma=\ianc{(\GG';\cD')\in
\cS\quad \dsat\cD'\quad(\GG;\cD)\ins \cS}
{(\GG,\block{\GG'});(\cD\And\block{\cD'})\ins\cS}{\ins_2}$$
\btab
$\ga\inss$\bs
$\GG;\ald(\cD)\insss$\bi $3$\\
$\gap\in\cS$\bs
$\GG';\ald(\cD')\in\csa$\bl{le:inaug}
$\dsat\cD'$\bs
$\dsats \ald(D')$\bi $1$\\
$(\GG,\block{\GG'});\ald(\cD)\And\ald(\block{\cD')})\insss$\br $\ins_2$\\
$(\GG,\block{\GG'});\ald(\cD\And\block{\cD'})\insss$\br $\ald\And$
\etab
\enit
\end{proof}
\begin{Lemma}
\label{le:negfactsat}
If $\vM$ is a simple term, then
$\dsats\BAnd_{\vN\in\mnot(\vM)}\Pi( \neg (q\ \vN)\If\top)$.
\end{Lemma}
\begin{proof} By   rules
  $\dsats\And,\dsat\Pi,\dsats\Imp,\sla\top,\dsat\atm,\sla\atm$.
\end{proof}

The following Lemma ensures that augmented clauses are closed under
negation. In particular, for $\ga\insss$, if $D\in\cD$, so is
$\GG\vd\mnota(D)$. 
We use $\ga\sla\mnotg(G)\insss$ for $\mnotg(G)=G_{\neg}$ and
$\ga\sla G_{\neg} \insss$. Similarly for $\mnotd(D)$.

\begin{Lemma}[Negative Schema Augmentation]
\label{le:negaug}
Let $\ga\insss$. Then:
\ben
\item If $\dsats \ald(D)$, then $\dsats \mnotd(\ald(D))$.
\item If $\ga\sla \alg(G)\insss$, then $\ga\sla\mnotg( \alg(G))\insss$.

\enen
\end{Lemma}


\begin{proof}
\renewcommand{\inss}{\insss}
By mutual induction on the structure of $\pi::\  \dsats\ald( D)$ and  $\gamma
::\ga\sla \alg(G)\inss$.
\bit
\itc $$\pi=\ianc{}{\dsats \ald(\perp)}{\dsats\perp}$$
By rule $\ald(\perp)=\perp$ and $\vdf\mnotd(\perp)=\top$: thus
$$\pi'=\ianc{}{\dsats \top}{\dsats\top}$$

\itc $$\pi=\ianc{}{\dsats \ald(\top)}{\dsats\top}$$
By rule $\ald(\top)=\top$ and $\vdf\mnotd(\top)=\perp$: thus
$$\pi'=\ianc{}{\dsats \perp}{\dsats\perp}$$

\itc $\pi$ ends in $ \dsats\ald(q\ \vM\If G)$:
 \btab
 $\dsats\ald(q\ \vM)\If\alg(G)$\br $\ald\Imp$\\
%$\ald(q\ \vM)=q\ \vM$\br $\ald\atm$\\
$\dsats \neg q\ \vM$\br $\dsats\atm$\\
%$\dsats\neg (q\ \vN)$ for $\vN\in\mnot(\vM)$\br $\dsat\atm$\\
$\emp\sla\alg(G)\insss$\br $\dsat\Imp$\\
$\emp\sla\mnotg(\alg(G))\insss$\bi $2$\\
$\dsats   \neg q\ \vM\If \mnotg(\alg(G))$ \br $\dsats\Imp$\\
$\dsats\BAnd_{\vN\in\mnot(\vM)}\Pi( \neg (q\ \vN))$
\bl{le:negfactsat}
$\dsats\BAnd_{\vN\in\mnot(\vM)}\Pi( \neg (q\ \vN)\If\top) \And
 ( \neg q\ \vM\If \mnotg(\alg(G)))$\\
\br $\dsats\And$\\
$\dsats\mnotd(q\ \vM\If \alg(G))$\br $\ald\Imp$\\
$\dsats\mnotd(\ald(q\ \vM)\If \alg(G))$\br $\mnotd\Imp$\\
$\dsats\mnotd(\ald(q\ \vM\If G))$\br $\ald\Imp$
 \etab

%PIXA
\itc $\pi$ ends in $\dsats\ald(\PIXA D)$:
\btab
$\dsats\PIXA\ald(D)$\br $\ald\Pi$\\
$\dsats[u/x]\ald(D)$\br $\dsats\Pi$\\
$\dsats[u/x]\mnotd(\ald(D))$\bi $1$\\
$\dsats\PIXA\mnotd(\ald(D))$\br $\dsats\Pi$\\
$\dsats\mnotd(\PIXA\ald(D))$\br $\mnotd\Pi$\\
$\dsats\mnotd(\ald(\PIXA D))$\br $\ald\Pi$
\etab
%And
\itc $\pi$ ends in $\dsats\ald( D_1\And D_2)$:
\btab
$\dsats\ald(D_1)\And\ald(D_2)$\br $\ald\And$\\
$\dsats\ald(D_1)$ and $\dsats\ald(D_2)$\br $\dsat\And$\\
$\dsats\mnotd(\ald(D_1))$ and $\dsats\mnotd(\ald(D_2))$\bi $1$\\
$\dsats\mnotd(\ald(D_1))\Or\mnotd(\ald(D_2))$\br $\dsat\Or$\\
$\dsats\mnotd(\ald( D_1)\And\ald(D_2))$\br $\mnotd\And$\\
$\dsats\mnotd(\ald( D_1\And D_2))$\br $\ald\And$
\etab
%tensor
\itc $\pi$ ends in $\dsats\ald( D_1\tensor D_2)$:
\btab
$\dsats\ald(D_1)\tensor\ald(D_2)$\br $\ald\tensor$\\
$\dsats\ald(D_1)$ and $\dsats\ald(D_2)$\br $\dsat\tensor$\\
$\dsats\mnotd(\ald(D_1))$ and $\dsats\mnotd(\ald(D_2))$\bi $1$\\
$\dsats\mnotd(\ald(D_1))\And\mnotd(\ald(D_2))$\br $\dsat\And$\\
$\dsats\mnotd(\ald( D_1)\tensor\ald(D_2))$\br $\mnotd\tensor$\\
$\dsats\mnotd(\ald( D_1\tensor D_2))$\br $\ald\tensor$
\etab
%%% G
%TOP
\itc $\gamma$ ends in $\ga\sla \alg(\top)\inss$:
\btab
$\ga\sla\top\insss$\br $\alg\top$\\
$\ga\inss$\bs
$\ga\vd\mnotg(\top)=\perp$\br $\mnotg\top$\\
$\ga\sla \perp\insss$\br $\sla \perp$
\etab
% PERP
\itc $\gamma$ ends in $\ga\sla \alg(\perp)\inss$:
\btab
$\ga\sla\perp\insss$\br $\alg\perp$\\
$\ga\inss$\bs
$\ga\vd\mnotg(\perp)=\top$\br $\mnotg\perp$\\
$\ga\sla \top\insss$\br $\sla \perp$
\etab
%EQD
\itc $\gamma$ ends in $\ga\sla \alg(\vM\eqd\vN)\inss$:
\btab
$\ga\sla\vM\eqd\vN\insss$\br $\alg\eqd$\\
$\ga\inss$\bs
$\ga\vd\mnotg(\vM\eqd\vN)=(\vM\neqd\vN)$\br $\mnotg\eqd$\\
$\ga\sla \vM\neqd\vN\insss$\br $\sla \neqd$
\etab
%NEQD
\itc $\gamma$ ends in $\ga\sla \alg(\vM\neqd\vN)\inss$:
\btab
$\ga\sla\vM\neqd\vN\insss$\br $\alg\neqd$\\
$\ga\inss$\bs
$\ga\vd\mnotg(\vM\neqd\vN)=(\vM\eqd\vN)$\br $\mnotg\neqd$\\
$\ga\sla \vM\eqd\vN\insss$\br $\sla \neqd$
\etab
% Q
\itc $\gamma$ ends in $\ga\sla \alg(Q)\insss$:
\bit
\item[Subcase]
\btab
$\emp\sla\ Q\insss$\br $\alg\atm\top$\\
$\emp\insss$\bs
$\emp\sla\neg Q\insss$\br $\mnotg\atm$\\
$\emp\sla\mnotg(Q)\insss$\br $\mnotg\Imp$\\
$\emp\sla\mnotg(\alg(Q)) \insss$\br $\alg\atm\top$
\etab
\item[Subcase]
\btab
$\ga\sla\mnota(\cD)\Imp Q\insss$\br $\alg\atm$\\
$\GG;(\cD\And\mnota(\cD))\sla Q\insss$\br $\sla\Imp$\\
$\GG;(\cD\And\mnota(\cD))\insss$\bs
$\GG;(\cD\And\mnota(\cD))\sla \neg Q\insss$\br $\sla\atm$\\
$\ga\sla\mnota(\cD)\Imp\neg Q\insss$\br $\sla\Imp$\\
$\ga\sla\mnota(\cD)\Imp\mnotg(Q)\insss$\br $\mnotg\atm$\\
$\ga\sla\mnotg(\mnota(\cD)\Imp Q)\insss$\br $\mnotg\Imp$\\
$\ga\sla\mnotg(\alg(Q)) \insss$\br $\alg\atm$
\etab
\enit

\itc $\gamma$ ends in $\ga\sla \alg(D\Imp  G)\inss$:
\btab
$\ga\sla \ald(D)\Imp  \alg(G)\inss$\br $\alg\Imp$\\
$\dsats\ald(D)$ and 
%$\dsats \ald(D)$\bi $1$\\
$\GG;(\cD\And D)\sla\alg( G)\inss$\br $\sla\Imp$\\
$\GG;(\cD\And \ald(D))\sla \mnotg(\alg(G))\insss$\bi $2$\\
$\gda\sla \ald(D)\Imp \mnotg(\alg(G))\insss$\br $\sla\Imp$\\
$\gda\sla \mnotg(\ald(D)\Imp \alg(G))\insss$\br $\mnotg\Imp$\\
$\gda\sla \mnotg(\alg(D\Imp G))\insss$\br $\alg\Imp$
\etab
\itc $\gamma$ ends in $\ga\sla\alg(\PIXA G)\insss $:
\btab
$\ga\sla\PIXA\alg(G)\insss $\br $\alg\Pi$\\
$(\GG,y\oftp A);\cD\sla[y/x]\alg(G)\insss $\br $\sla\Pi$\\
$(\GG,y\oftp A);\cD\sla[y/x]\mnotg(\alg(G))\insss $\bi $2$\\
$\ga\sla\PIXA\mnotg(\alg(G))\insss $\br $\sla\Pi$\\
$\ga\sla\mnotg(\PIXA\alg(G))\insss $\br $\mnotg\Pi$\\
$\ga\sla\mnotg(\alg(\PIXA G))\insss $\br $\alg\Pi$\\
\etab
\itc $\gamma$ ends in $\ga\sla\alg(G_1\Or G_2)\insss $:
\btab
$\ga\sla\alg(G_1)\Or \alg(G_2)\insss $\br $\alg\Or$\\
$\ga\sla\alg(G_1)\insss $ and $\ga\sla\alg(G_2)\insss$\br $\sla\Or$\\
$\ga\sla\mnotg(\alg(G_1))\insss $ and $\ga\sla\mnotg(\alg(G_2))\insss$\bi $2$\\
$\ga\sla\mnotg(\alg(G_1))\And \mnotg(\alg(G_2)\insss $\br $\sla\And$\\
$\ga\sla\mnotg(\alg( G_1)\Or \alg(G_2))\insss $\br $\mnotg\Or$\\
$\ga\sla\mnotg(\alg( G_1\Or G_2))\insss $\br $\alg\Or$
\etab
\itc $\gamma$ ends in $\ga\sla\alg(G_1\And G_2)\insss $:
\btab
$\ga\sla\alg(G_1)\And \alg(G_2)\insss $\br $\alg\And$\\
$\ga\sla\alg(G_1)\insss $ and $\ga\sla\alg(G_2)\insss$\br $\sla\And$\\
$\ga\sla\mnotg(\alg(G_1))\insss $ and $\ga\sla\mnotg(\alg(G_2))\insss$\bi $2$\\
$\ga\sla\mnotg(\alg(G_1))\Or\mnotg(\alg(G_2)\insss $\br $\sla\Or$\\
$\ga\sla\mnotg(\alg( G_1)\And \alg(G_2))\insss $\br $\mnotg\And$\\
$\ga\sla\mnotg(\alg( G_1\And G_2))\insss $\br $\alg\And$
\etab
\enit
\end{proof}

We can combine the two latter lemmata \ref{le:saug} and
\ref{le:negaug} to prove that augmentation guarantees that 
static and dynamic clauses are closed under complementation.

\begin{Corollary}[Closure under Complementation]
\label{co:clocomp}
\mbox{}
\\
If $\dsat D$, then $\dsats\mnotd(\ald(D))$.
\end{Corollary}

\renewcommand{\insss}{\ins\cS\bar\cS'}
\renewcommand{\dsats}{\models_{\!\cS\bar\cS'}}

