\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 inserts the correct assumption
complementation in a goal and in turn in a clause. We give one
judgment to augment a program, $\gfald(D)$, depicted in
\ref{fig:augd}. which merely recurs on the structure of clauses until
it calls goal augmentation, $\ga\vdfg\alg(G)$ (Figure \ref{fig:augd}).
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. 
\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(\glob G) = \glob G^a}{\gfald(\Pi(Q\If G) )= \Pi(Q \If G^a)}{\ald\If^{\rho}}
  \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}

%\pagebreak
\newcommand{\qqquad}{\qquad\qquad} 
Some examples will make the whole
process clear;
%\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 judgment $\ald(cplam)$ calls $\alg(\PI
{x}{ exp} copy\ x\ x\Imp copy\ (E\ x) \ (F\ x))$,
 which collects the context $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.
We start by noting that $\mnotr(copy\ x \ x)=\top$, since the
conditions on rule $\mnotr$ are not satisfied. Then, note that 
$x\oftp exp\vd\mnot(x)=\{lam\ F', app\ F_1\ F_2\}$.
  This yields: 
$$x\oftp exp\vd \mnot^x_1(copy\ x\ x)=(\PI{F',F_1,F_2}{exp} \neg copy\ x\ (lam\
F')\And \neg copy\ x\ (app\ F_1\ F_2))$$
% Secondly: $$ \mnot^x_2(copy\ x\ x)=  (\PI{E'}{exp} \neg copy\ E'\ x\If
% x\neqd E')$$
Symmetrically: $$ x\oftp exp\vd\mnot^x_2(copy\ x\ x)= \PI{F'',F_3,F_4}{exp} \neg copy\  (lam\
F'') \ x\And \neg copy\  (app\ F_3\ F_4)\ x)$$
This will yield the augmented clause:
% 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 (\PI{F',F'',F_1,F_2,F_3,F_4}{exp} \\
&& \qqquad \neg copy\ x\ (lam\ F')\And \neg copy\ x\ (app\ F_1\ F_2)\And\mbox{}\\
&& \qqquad \neg copy\  (lam\ F'') \ x\And \neg copy\  (app\ F_3\ F_4)\ x)\\
%& & \qquad\qquad (\PI{F'}{exp} \neg copy\ x\ F'\If x\neqd F')\And\\
%& & \qquad\qquad (\PI{E'}{exp} \neg copy\ E'\ x\If x\neqd E')\Imp\\
&& \qquad\qquad\qquad
\Imp 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$:
\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 first:
\beq
\mnotr(copy'\ x\ y)& = & (\PI{E''}{exp} \neg copy'\ E''\ x)\\
\mnot^C_y(copy'\ x\ y)& = & (\PI{F''}{exp} \neg copy'\ y\ F'').
\eneq
Secondly, by computing, respectively, for $\GG=x\oftp exp,y\oftp exp $,
$\GG\vd\mnot(y)$ and
$\GG\vd\mnot(x)$: 
\beq
\GG\vd\mnot^x_1(copy'\ x\ y)& = &(\PI{F_0,F_1,F_2}{exp} \neg copy'\ x\ (lam\
F_0)\And \neg copy'\ x\ (app\ F_1\ F_2)\And \neg copy' x\ x)\\
\GG\vd\mnot^y_2(copy'\ x\ y)& = & 
(\PI{F'_0,F'_1,F'_2}{exp} \neg copy'\  (lam\
F'_0) \ y\And \neg copy'\  (app\ F'_1\ F'_2)\ y\And \neg copy'\ y\ y)\\
\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{y}{exp}\\
& & \qquad\qquad (\PI{E'}{exp} \neg copy'\ E'\ x)\And\\
& & \qquad\qquad (\PI{F'}{exp} \neg copy'\ y\ F') \And\\
&&\qqquad \Pi( \neg copy'\ x\ (lam\
F_0)\And \neg copy'\ x\ (app\ F_1\ F_2)\And \neg copy' x\
x\And\mbox{}\\
& & \qqquad \neg copy'\  (lam\
F'_0) \ y\And \neg copy'\  (app\ F'_1\ F'_2)\ y\And \neg copy'\ y\ y)\\
%& & \qquad \qquad(\PI{F''}{exp} \neg copy'\ F''\ y\If x\neqd F'')\And\\
%& & \qquad\qquad (\PI{E''}{exp} \neg copy'\ x\ E''\If x\neqd E')\Imp\\
&& \qquad\qquad\qquad \Imp 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
$\mnotr,\mnot^C_y$ are, in this case, 
 useless; however since this kind of data
flow analysis is in general undecidable, the augmentation procedure
inserts the negation of a clause for every `odd' position relevant to the
pivot parameter.
\smallskip
Now, consider the typing clause for lambda terms:
\beq
oflam &:&  \PI{E}{exp\Imp exp}\PI{T_1,T_2}{tp}\\
&& of\ (lam\ E) \ (arrow\ T_1\ T_2)\\
& & \qquad\If( \PI{x}{exp} of\ x\ T_1 \Imp  of\ (E\ x) \ T_2).
\eneq
As $T_1$ is an input term, normalization of input variables  inserts
the  appropriate equation, where \texttt{oflam} $\mapd $ \texttt{oflam'}:
\beq
oflam' &:& \PI{E}{exp\Imp exp}\PI{T_1,T_2}{tp}\\
&& of\ (lam\ E) \ (arrow\ T_1\ T_2)\\
& &\qqquad (\PI{T}{tp}  of\ x\ T\If T\eqd T_1)\Imp\\
&&\qqquad\qquad  of\ (E\ x) \ T_2).
\eneq
Both $\mnotr$ and $\mnot_x^1$ generate no contribution; in
particular $x\oftp exp \vd\mnot_x^1(\PI{T}{tp}  of\ x\ T)$ calls the
$\mnotxi$ rule, but term complementation (applied to the
existential variable $T$) yields the trivial clause. 
Therefore, by $\mnotg(T\eqd T_1)$,  augmentation will result into:
\beq
\ald(oflam) &:& \PI{E}{exp\Imp exp}\PI{T_1,T_2}{tp}\\
&& of\ (lam\ E) \ (arrow\ T_1\ T_2)\\
& & \qquad \If(\PI{x}{exp} of\ x\ T_1 \Imp\\
& &\qqquad (\PI{T}{tp} \neg of\ x\ T\If T\neqd T_1)\Imp\\
&&\qqquad\qquad  of\ (E\ x) \ T_2).
\eneq
Consider now a predicate which counts the number of bound variables in a
lambda-term:
% \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
\beq
cntlam & : & \PI {E}{exp\Imp exp} \PI {N} {nat} \\
& & cnt\ (lam\ E) \ N\\
& &  \qquad\If(\PI {x}{exp} cnt\ x \ s(0)\Imp \\
& & \qqquad   cnt\ (E\ x)  \ N).
\eneq
The call to $x\oftp exp\vd\mnota (cnt\ x\ s(0))$
leads to $\mnot_x^1(cnt\ x\ s(0))$, since, again, $\mnotr$ does not
contribute: $\mnotxi$ collects the term complement of
$s(0)$ in the \emph{empty} context,  that is $\{0, s(s(M)) \}$:
\beq
\ald(cntlam) & : & \PI {E}{exp\Imp exp} \PI {N} {nat} \\
& & cnt\ (lam\ E) \ N\\
& &  \qquad\If(\PI {x}{exp} (\neg cnt\ x\ 0 \And \PI {M}{nat} \neg cnt\
x\ s(s(M)))\\ 
& & \qqquad  \Imp cnt\ (E\ x)  \ N).
\eneq
\smallskip
Let us see how rule $\mnota\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 $\mnota\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}


\begin{Example}
Let us apply the complement algorithm to the \texttt{linx} predicate
definition; note the vacuous
application $E_2\ x^0$:
\beq
linxx& : & linx(\lx x).\\
linxap1& : & linx(\lx app\ (E_1\ x) \ (E_2\ x^0)) \If  linx(\lx E_1\ x).\\
linxap2& : & linx(\lx app\ (E_1\ x^0) \  (E_2\ x)) \If  linx(\lx E_2\ x).\\
\ald(linxlm)& : &linx(\lx lam(\ly E\ x\ y)) \If (\PI{y}{exp} \top_{linx}\Imp
linx (\lx E\ x\
y)).
\vsk
\lefteqn{\mnotd(def(linx))=}\\
\lefteqn{ \mnotd(linxx)\tensor\mnotd(linxap1)\tensor\mnotd(linxap2)\tensor\mnotd(linxlm)=}\\
  && (\neg linx(\lx app\ (E_1\ x) \ (E_2\ x))\And \neg linx(\lx lam( \ly (E\ x\
y))))\tensor\mbox{}\\ 
  && (\neg linx(\lx x)\And  \neg linx(\lx lam( \ly (E\ x\ y)))\And\neg linx(\lx app\ (E_1\ x) \ (E_2\ x^1) )\\
&& \mbox{}\And\neg linx(\lx app\ (E_1\ x) \ (E_2\ x^0) )\If\neg linx(\lx E_1\ x))\tensor\mbox{}\\
  &&( \neg linx(\lx x)\And  \neg linx(\lx lam( \ly (E\ x\ y)))\And \neg
linx(\lx app\ (E_1\ x^1) \ (E_2\ x ))\\
 &&  \If\neg linx(\lx app\ (E_1\ x^0) \ (E_2\ x))\If \neg linx(\lx E_2\ x))\tensor\mbox{}\\
  && (\neg linx(\lx x)\And \neg linx(\lx app\ (E_1\ x) \ (E_2\ x)) \\
 &&\mbox{}\And\neg   linx (\lx lam(\ly (E\ x\ y) ))\If (\PI{y}{exp} \neg linx(\lx
y)\Imp \neg linx (\lx E\ x\ y ))).
\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\mbar(\GG;\some{\Phi}\cD))= \csa\mbar(\GG;\some{\Phi} \cD^a)}{aug\mbar}
\end{array}\]

Now, the usual lemma on schema membership:

\begin{Lemma}
\label{le:inaug}
If $\gapp\in\cS$ then $\GG\vd\GG';\ald(\cD')\in aug(\cS)$.
\end{Lemma}
\begin{proof}
By  induction on the structure of $\pi::\ga\in\cS$.
\bit
\itc$$
\ibnc{\GG\vd\q\hastype\Phi}{(\GG';\cD')\equiv_{\alpha}(\GG'';\q\cD)}
{\GG\vd(\GG';\cD')\in \cS\mbar(\GG'';\some{\Phi} \cD)}{\in_1}$$
% \itc
% $$\pi=\ianc{(\GG';\cD')\equiv_{\alpha}(\GG;\q\cD)}{(\GG';\cD')\in
% \cS\mbar 
% (\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)\mbar\GG'';\some{\Phi} \ald(\cD)$\br $\in_1$\\
%$\GG';\ald(\cD')\in aug(\cS)\mbar\GG;aug(\some{\Phi} \cD)$\br\\
$\GG';\ald(\cD')\in aug(\cS\mbar\GG'';\some{\Phi} \cD)$\br $aug\mbar$
\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=\ianc
%\dsat \glob Q
{\emp\sla\glob G\inss}{\dsat \Pi(G\Imp  Q)}{\dsat\Imp^{\s}}$$
\btab
%$\dsat \glob Q$\bs
%$\dsats \ald(D)$\bi $1$\\
$\emp\sla \glob G\inss$\bs
$\emp\sla \alg(\glob G)\insss$\bi $2$\\
$\dsats \alg(\glob G)\Imp \glob Q$\br $\dsat\Imp$\\
$\dsats \ald(\Pi(G\Imp Q))$\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}$$
By sub-derivation $\ga\inss$; there are two ways to augment an atom:
\bit
\item[\subcase] $\emp\vd \alg(Q)=Q$:
\btab
%$\cdot;\top\inss$\bs
%$\cdot;\top\vdf\ald(\top)=\top$\br $\ald\top$\\
$\cdot;\top\insss$\br $\ins_1$\\
$\emp\sla Q\insss$\br $\alg\atm\top$\\ 
$\emp\sla\alg(Q)\insss$\br $\sla\atm$
\etab
\item[\subcase] $\ga\vd aug(Q)= \mnota(\cD)\Imp Q$:
\btab
%$\ga\inss$\bs
$\GG;\ald(\cD)\insss$\bi $3$\\
$\GG;\ald(\cD)\sla Q\insss$\br $\sla \atm$\\
$\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\vd(\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$\\
$\GG\vd\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}


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)$. We will need the following technical remark:

\begin{Remark}
\label{le:negfactsat}
If $\vM$ is a simple term, then
$\dsats\BAnd_{\vN\in\mnot(\vM)}\Pi( \neg (q\ \vN)\If\top)$.
\end{Remark}
\begin{proof} By   rules
  $\dsats\And,\dsat\Pi,\dsats\Imp,\sla\top,\dsat\atm,\sla\atm$.
\end{proof}

\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(\Pi(q\ \vM\If G))$:
 \btab
 $\dsats(\Pi(q\ \vM)\If\alg(G))$\br $\ald\Imp$\\
%$\ald(q\ \vM)=q\ \vM$\br $\ald\atm$\\
%$\dsats\neg (q\ \vN)$ for $\vN\in\mnot(\vM)$\br $\dsat\atm$\\
$\emp\sla\alg(\glob G)\insss$\`By inversion on rule $\dsat\Imp$\\
$\emp\sla\mnotg(\alg(\glob G))\insss$\bi $2$\\
$\dsats \glob (\neg q\ \vM)$\br $\dsats\atm$\\
$\dsats  \Pi( \neg q\ \vM\If \mnotg(\alg(G)))$ \br $\dsats\Imp$\\
$\dsats\BAnd_{\vN\in\mnot(\vM)}\Pi( \neg (q\ \vN))$
\` By Remark \ref{le:negfactsat}\\
$\dsats\BAnd_{\vN\in\mnot(\vM)}\Pi( \neg (q\ \vN)\If\top) \And
\Pi ( \neg q\ \vM\If \mnotg(\alg(G)))$\br $\dsats\And$\\
%$\dsats\mnotd(q\ \vM\If \alg(G))$\br $\ald\Imp$\\
$\dsats\mnotd(\Pi(q\ \vM)\If \alg( G))$\br $\mnotd\Imp$\\
$\dsats\mnotd(\ald(\Pi(q\ \vM\If G)))$\br $\ald\Imp$
 \etab

% %PIXA no more
% \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$:\\
By sub-derivation $\ga\inss$; there are two ways to augment an atom:
\bit
\item[\subcase] $\emp\vd \alg(Q)=Q$:
\btab
$\emp\sla\ Q\insss$\br $\sla\atm$\\
%$\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] $\ga\vd alg(Q)= \mnota(\cD)\Imp G$:
\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\mbar\cS'}
\renewcommand{\dsats}{\models_{\!\cS\mbar\cS'} \!}

