\documentclass{book}
 \usepackage{lcom}
 \usepackage{latexsym}
 \usepackage{cdsty2}
 \usepackage{fancyheadings}
% % \usepackage{prooftree}
 \def\zzctdrawdotedge{\drawdotedge{4pt}0}
 \def\ctabutborderlr{1em}
 \def\ctabutbordertb{1ex}
 \lhead[\fancyplain{}{\thepage}]{\fancyplain{}{\rightmark}}
 \rhead[\fancyplain{}{\leftmark}]{\fancyplain{}{\thepage}}
 \cfoot{\footnotesize \it Draft of \today}

%\setlength{\textwidth}{15.2cm}
\pagestyle{fancyplain}
\begin{document}

\bibliographystyle{alpha}
%\tableofcontents
%\listoffigures




\input{htermprf}


\input{context}

\input{cc}

\input{augment}

\input{excluproof}

\input{exh}

\input{tensor}
%\end{document}


\bibliography{not,framework}
\end{document}








% We present two definitions: the first (eager complementation) computes
% complementation of ground terms via the auxiliary judgment $\gf\mnotxij
% (D) \yield D'$, while the second (lazy complemetation) always
% introduces disequations, even when they are unsatisfiable:

% \begin{Definition}[Eager Assumption Complementation]
%   \label{def:nota}
% Let 
% for  $0\leq j\leq n$, 
% $Z_j$ be a fresh logic variable of correct type: the judgment
% $\gf\mnotxi(D)=D'$ is realized by the following rules:
%   \[
%   \begin{array}{c}
%  \ianc{}{\gf\mnotxi(\bot_q)  =   \top_q}{\mnotxi\bot}\vsk
%     \ianc{head(Q)=q, \Sigma(q)= \An\Imp \prop}
%     {\gf\mnotxi(\top_q)  =
%       \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ Z_1\dots Z_{i-1}\ x\
%       Z_{i+1}\dots Z_n}{\mnotxi\top}\vsk
% %\mbox{no case for $\GG=\cdot$}\footnote{\mbox{does not make sense,
% %    since $x\in\GG$}}\vsk 
%  %  \ianc{M_i \mbox{ \ \textrm{closed}}}
% %   {\GG,x\oftp A\vdf \mnotxi\ q(M_1\mdots  M_i\mdots M_m, x,\Nn) \yield 
% %     \BAnd_{N\in\cdot\vd\mmnot M_i}\Pi(\neg q(M_1\mdots N\mdots M_m,
% %     x,\Nn)\If\top) }{\mnotxi\mmnot}\vsk
% %   \ianc{M_i
% % \mbox{ \textrm{no case for $M_j$ local gvar}}\vsk
% %{\gf\mnotxi  q(M_1\mdots  M_i\mdots M_m,
% %      x,\Nn)\yield \top}{\mnotxi At\_else}\vsk
%   \ibnc{\gf\mnotxi(D_1) =  D_1'}{\gf\mnotxi(D_2) =  D_2 '}
%     {\gf\mnotxi(D_{1}\And D_{2})  =  D_{1}'\tensor D_{2}'}{\mnotxi\And}\vsk
%     \ibnc{\gf\mnotxi(D_1) =  D_1'}{\gf\mnotxi(D_2) =  D_2 '}
%     {\gf\mnotxi(D_{1}\tensor D_{2})  =  D_{1}'\And
%     D_{2}'}{\mnotxi\tensor}\vsk
%   \ianc {\gf \mnotxi(D)= D' }{\gf\mnotxi(\PI{y}{B} D)= \PI{y}{B}
%     D'}{\mnotxi\Pi}\vsk
%   \ianc{p\not\equiv head(Q)}{\gf\mnotxi(p\ \Mn\If G)= \top_q}{\mnotxi At-nmr}\vsk
%     \ibnc{\gf\mnotxij(q\ \Mn)=D'}{\gf\mnotg(G) =  G'}{\gf\mnotxi(q\ \Mn\If G )=
%     D'\And\neg q\ \Mn \If G'}{\mnotxi\If}\vsk\vsk

%     \ianc{ \exists j\oftp 1\leq j\leq n, j\not\equiv i\,.\,M_j\in\GG\cup\Phi
%    }{\gf\mnotxij  (q\ \Mn)\yield
%     \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ Z_1\dots Z_{i-1}\ x\
%     Z_{i+1}\dots Z_n\If M_j\neqd Z_j}{\mnotxij Atc}\vsk
%      \ianc{\exists j\oftp 1\leq j\leq n, j\not\equiv i}
%      {\gf\mnotxij  (q\ \Mn)\yield\BAnd_{N\in\mnot(M_j)}\Pi(
%     %\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} 
%        \neg q\ Z_1\dots\ N\ \dots\ x\ 
%        \dots Z_n)\If\top_q}{\mnotxij At}
%   \end{array}
%   \]
% where
% $$\gf\mnotxij(D)=\BAnd D'\mid \gf\mnotxij(D)\yield D'$$
% \end{Definition}

% In the rule $\mnotxij At$ we choose a term $M_j$ in the source atom
%   such that it is either an input term or another parameter, in a CLP
%   style, we add the relative disequation. Otherwise we compute its
%   complement with a call to $\mnot$. In particular, if $M_j$ is an
%   essentially existential variable, its complement is empty and
%   $\top_Q$ is returned.


% \begin{Theorem}[Positive Conservativity]
% \label{thm:conservaug}
% If $G$ is positive, then $\ga\vdf G$ iff $\ga\vdf\alg(G)$.
% \end{Theorem}

% \begin{proof}
% We generalize this...
% \end{proof}
















