\renewcommand{\Pixa}{\PI{x}{a}}
\renewcommand{\q}{}
\renewcommand{\s}{}
\newcommand{\Sn}{\ol{S_n}}
\renewcommand{\fpp}{\nvd_{\cP}}
\renewcommand{\ex}{e_x}
\renewcommand{\qmx}{q\ \mxi}
\newcommand{\nxi}{\ol{N_n}}
\newcommand{\mxi}{\ol{M^i_{\ex}}}

\section{Exhaustivity}
\label{sec:exh}

% In the following we will be fairly informal with the treatment of
% substitutions, is so far as we will identify for example $\q(G_1\And G_2)$
%  with $\q G_1 \And \q G_2$.

\begin{Theorem}[Exhaustivity]
\label{thm:exhau}
Let $\models_{\!\csa}\ald(\PP)$ and $\ga\ins\csa$. For every goal $G$ such
that $\ga\sla G\ins\csa$, if $\ga\fpp G$ then $ \gna\sn\mnotg (G)$.
\end{Theorem}

\begin{proof}
\renewcommand{\ga}{\Gamma;\cD }
\renewcommand{\gna}{ \Gamma;\cD }
\renewcommand{\snp}{\vd_{\!\cP}\mnotg}
\renewcommand{\foq}{}
Note that $\GG;\cD\sn\defp(\neg q,\cP\And\cD)\imm \neg Q$ iff so does every
 disjunct. We generalize this to:% : let $\theta,\sigma$ be well-typed
%  substitutions such that $\GG\vd\sigma,\GG\vd\theta$:
\ben
\item
If  $\foq\SM ::  \ga\fpp \q G$, then  $\SP :: \gna\snp (G)$.
\item[2.1]
If  $D\inn \defp(Q,\PP)$
$\IM :: \ga\fpp \q D  \nimm \q Q$, then  
$\IP :: \gna\sn \s \mnotd(D) \imm \s \neg Q$.
\item[2.2]
If $D\inn \defp(Q, \cD)$
$\IM :: \ga\fpp \q D  \nimm \q Q$, then  
$\IP :: \gna\sn \s \mnota(D) \imm \s \neg Q$.
\enen
The proof is by mutual induction on the structure of $\SM$ and
$\IM$. We start with part $2.1$:
\bit % main BIT
\item[\fbox{2.1}]
\mbox{}
\bit
\itc 
$$\IM = \ianc{}{\foq\ga\fpp\top\nimm\q Q}{\not\imm\top}$$
  Then $\mnotd (\top) =\perp$ and %by Weakening
$$ \IP = \ianc{}{\ga\sn\perp\imm \s \neg Q}{\imm\perp}$$
\itc
$$ \IM = \ianc{\mbox{for all $\theta$ } \ga\fpp[\theta]\vN \eqd \q\vM}
{\foq\ga\fpp \Pi(q\ \vN \If  G)\nimm\q q\ \vM}{\not\imm\Imp^1}$$
\btab
for all $\theta$ $\foq\ga\fpp[\theta]\vN \eqd \q\vM$\bs
for all $\theta$  $\foq [\theta]\vN \not= \vM$\br $\nvd\eqd$\\
$\cdot\prv \vM\not\in\| \vN\|$\` By definition of $\|\_\|$\\
 $\cdot\prv \vM\in \|\mnot (\vN)\|$\` By term exhaustivity (\ref{le:part})\\
$\vM=[\sigma]\Sn$ for some $\sigma$ and $\Sn\in\cdot\vd\mnot(\vN)$\` By definition of $\|\_\|$\\
$\gna\sn\s \vM\eqd[\sigma]\s\Sn$ \br $\vd\eqd$\\
$\gna\sn\s\Pi(\neg q\ \Sn\If \top)\imm\s
\neg q\ \vM$\br $\imm\Pi$\\
$\gna\sn\s\BAnd_{\Sn\in\cdot\vd\mnot(\vN)} \Pi(\neg q\ \Sn\If \top)\imm\s
\neg q\ \vM$\` By appropriate applications of rule $\imm\And$\\
$\gna\sn\s\BAnd_{\Sn\in\cdot\vd\mnot(\vN)} \Pi(\neg q\
\Sn\If \top)\And \Pi(\neg q\ \vM \If \mnotg(G))\imm \s \neg q\ \vM$\br $\imm\And_1$\\
 $\gna\sn\s\mnotd(\Pi(q\ \vN\If G)\imm \s \neg q\ \vM)$\br $\mnotd\imm$
\etab
\itc 
$$\IM = \ibnc{ \ga\fpp [\sigma]\vN\neqd\q\vM }{\foq \ga\fpp[\sigma] G}{\foq\ga\fpp \Pi( q\ \vN\If G)\nimm\q q\ \vM} {\not\imm{\Imp_2}}$$
\btab
$\foq\ga\fpp [\sigma]\vN\neqd\q\vM $\bs
$\gna\sn [\sigma]\vN\eqd \s\vM$  \br $\vd\neqd$\\
$\foq \ga\fpp [\sigma] G$\bs
$\gna\snp[\sigma] (G)$\bi $1$\\
$\gna\sn\s\Pi( \neg q\ \vN \If \mnotg (G))\imm \s\neg q\ \vM$ \br $\imm\Imp$\\
$\gna\sn\s\BAnd_{\Sn\in\cdot\vd\mnot(\vN)} \Pi(\neg q\
\Sn\If \top)\And \Pi(\neg q\ \vN \If \mnotg(G))\imm\s \neg q\ \vM$\br $\imm\And_2$\\
%$\gna\sn(\mnotd (q\ \vN\If\top)\And \neg q\ \vN 
%\If \mnotg (G))\imm \neg q\ \vM$\br\\
$\gna\sn\s \mnotd(\Pi(q\ \vN\If G)) \imm \neg q\ \vM$\br $\mnotd\Imp$
\etab
\itc %tensor
$$ \IM = \ianc{\foq\ga\fpp \q D_{1}\nimm\q Q}{\foq\ga\fpp \q(D_{1}\tensor 
D_{2})\nimm\q Q}{ \not\imm\tensor_1}$$
\btab
$\foq\ga\fpp \q D_{1}\nimm\q Q$\bs
$\gna\sn\s \mnotd (D_{1})\imm \s\neg Q$\bi $2.1$\\ 
$\gna\sn\s \mnotd (D_{1})\And \s\mnotd(D_{2})\imm \s \neg Q$ \br $\imm\And_1$\\
 $\gna\sn\s \mnotd (D_{1}\tensor D_{2})\imm \s \neg Q$\br $\mnotd\tensor$
\etab
\itc %tensor
$$ \IM = \ianc{\foq\ga\fpp \q D_{2}\nimm\q Q}{\foq\ga\fpp \q(D_{1}\tensor 
D_{2})\nimm\q Q}{ \not\imm\tensor_2}$$
 Symmetrical to the above.
\itc %And
$$\IM = \ibnc{\foq\ga\fpp\q D_{1}\nimm\q Q}{\foq \ga\fpp\q D_{2}\nimm\q Q}
{\foq\ga\fpp\q( D_{1}\And D_{2})\nimm\q Q}{\not\imm\And}$$
\btab
$\foq\ga\fpp\q D_{1}\nimm\q Q$\bs
$\foq\ga\fpp\q D_{2}\nimm\q Q$\bs
$\gna\sn\s \mnotd (D_{1})\imm \s \neg Q$\bi $2.1$\\
$\gna\sn\s\mnotd (D_{2})\imm \s \neg Q$\bi $2.1$\\
$\gna\sn\s\mnotd (D_{1})\tensor \s\mnotd(D_{2})\imm \s \neg Q$\br
$\imm\tensor$\\
 $ \gna\sn\s\mnotd (D_{1}\And D_{2})\imm \s \neg Q$\br $\mnotd\And$
\etab
% \itc PIXA no more
% $$\IM = 
% \ianc{\mbox{for all $\q,n$,  }  \ga\fpp\q\cdot [n/x] D \nimm\q
%   Q}{\foq\ga\fpp\q\PIXA D \nimm \q Q}{\not\imm\Pi}$$
% \btab
% $ \mbox{for all $\q,n$,  } \ga\fpp \q\cdot[n/x] D \nimm\q Q$\bs
%  $\gna\sn\s\cdot[t/x]\mnotd ( D)\imm \s \neg Q$\bi $2.1$\\
% $\gna\sn\s\PIXA\mnotd ( D)\imm \s \neg Q$\br $\imm\Pi$\\
% $\gna\sn\s\mnotd (\PIXA D)\imm \s \neg Q$\br $\mnotd\Pi$
% \etab
\enit
\item[\fbox{2.2}] Recall that $q\ \mxi$ stands for $q\ M_1\dots
  M_{i-1} \ \ex\ M_{i+1}\dots M_n$, for $x\oftp A\in\GG$:
\mbox{}
\bit
\itc %top aug
$$\IM = \ianc{}{\foq\GG;\cD\fpp\top_{q}\nimm\q \qmx}{\not\imm\top}$$
\btab
%$\Mn=\Mn$\bh
$\GG;\cD\sn [\mxi / \Zn] \Zn\eqd \s\mxi$\br $\vd\eqd$\\
$\GG;\cD\sn\s\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ \zi
\ol{Z_n}\imm \s\neg\qmx$\br $\imm\Pi$\\
$\GG;\cD\sn\s\mnotr(\top_{q})\imm\s\neg \qmx$\br $\mnotr$\\
$\GG;\cD\sn\s\BAnd_{x\in dom(\GG)}\BAnd_{1\leq i\leq n,\xrq
         }\mnotxi(\top_q)\imm\s\neg \qmx$\` By appropriate applications of
       rule $\imm\And$\\
$\GG;\cD\sn\s\mnota(\top_{q})\imm\s\neg \qmx$\br $\mnota\top$
\etab
%\itc No case for $\xoa$ not relevant to $q$.
% $$\IM = \ianc{}{\foq\GG;\q\cD\fpp\top_{q}\nimm\q q\ \vM}{\not\imm\top}$$
% where $x$ is \emph{not} relevant to $q$.
% \begin{metanote} I need a lemma here\end{metanote}
% Then for any $D\in\cP$ it holds $\gna\snp(D)\imm\q\neg q\ \vM$.
\itc %%% Imp>>q
$$ \IM = \ianc{x\oftp a\in \GG, \mbox{ for all $\theta$ }\foq\ga\fpp\q\nxi \eqd \q\mxi}{\foq\ga\fpp \q\Pi(q\ \nxi \If  G)\nimm\q \qmx}{\not\imm\Imp^1}$$
\btab
for all $\theta$ $\foq\GG;\q\cD\fpp\q[\theta]\nxi \eqd \qmx$ and
$x\oftp a\in \GG$ \bs
\etab
\bit
\item[\subcase] $\ex\neqd[\theta] N_i$, $ N_i$ rigid by
  definition  for some $1\leq i\leq n$:
\btab
$\GG;\cD\sn [\mxi / \Zn] \Zn\eqd \s\mxi$\br $\vd\eqd$\\
$\GG;\cD\sn\s\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ \zi\imm
\s\neg\qmx$\br $\imm\Pi$\\ 
$\GG;\cD\sn(\BAnd_{1\leq i\leq n}\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg
q\ \zi)\imm \s\neg\qmx$\\
\` By appropriate applications of rule $\imm\And$\\
$\GG;\cD\sn\s\mnotr(q\ \nxi)\imm\s\neg \qmx$\br $\mnotr$\\
$\ga\sn(\BAnd_{x\in
dom(\GG)} \mnotr(q\ \Mn)\And (\BAnd_{1\leq
i\leq n,xR^{i}q}\GG\vd\mnotxi(q\ \Mn))) \And \Pi( \neg q\ \Mn)\If G'
\imm \s \neg q\ \mxi$\\
\` By appropriate applications of rule $\imm\And$\\
$ \GG;\s\cD\sn\s\mnota(\Pi(q\ \nxi\If G))\imm \s \neg q\ \mxi$\br $\mnota\Imp$
\etab
\item[\subcase] $\ex\eqd[\theta] N_i, M_j\neqd[\theta]N_j$ for $1\leq
  i,j\leq n, i\not=i$:
% \bit
% \item[\emph{Subsubcase}] $head(M_j)\in\GG$:
% \btab
% %$\foq\GG;\q\cD\fpp\q N_{j} \eqd \q M_{j}$  for some $1\leq j\leq
% %n,j\not= i$\br $\nvd\eqd$\\
% %$ \GG;\s\cD\sn\s N_{j} \neqd \s M_{j}$\br $\vd\neqd$\\
% $ \GG;\s\cD\sn[\mxi / \Zn] (\neg q\ \ol{Z_n} \If N_j\neqd Z_j)\imm\s\neg q\ \mxi$\br $\imm\Imp$\\
% $ \GG;\s\cD\sn\s(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ 
% \zi \If N_j\neqd Z_j)\imm\s\neg q\ \mxi$\br $\imm\Pi$\\
% $ \GG;\s\cD\sn\s\BAnd_{1\leq j \le n}(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ 
% \zi \If N_j\neqd Z_j)\imm\s\neg q\ \mxi$\\ \` By
% repeated applications of rule  $\imm\And$\\
% $ \GG;\s\cD\sn\s\mnotxi(q\ \nxi\If \top)\imm \s \neg q\ \mxi$  
% %some $x$ and $1\leq i\leq n,i\not=j$\br
%  $\mnotxi\atm\GG$ \\
% %$ \GG;\s\cD\sn\s\mnotxi(q\ \nxi)\imm \s \neg q\ \mxi$\br $\mnotxi\GG$\\ 
% $\ga\sn(\BAnd_{x\in
%            dom(\GG)} \mnotr(q\ \Mn)\And (\BAnd_{1\leq
%            i\leq n,xR^{i}q}\GG\vd\mnotxi(q\ \Mn))) \And \Pi( \neg q\ \Mn)\If G'\imm \s \neg q\
% \mxi$\\ \` By repeated applications of rule  $\imm\And$\\
% $ \GG;\s\cD\sn\s\mnota(\Pi(q\ \nxi\If G))\imm \s \neg q\ \mxi$\br $\mnota\Imp$
% \etab
% \item[\emph{Subsubcase}]  $head(M_j)\in\Sigma$:
\btab
%for all $\theta$ $\foq\ga\fpp[\theta]N_j \eqd M_j$\bs
for all $\theta$  $\foq [\theta]N_j \not= M_j$\br $\nvd\eqd$\\
$\GG\prv M_j\not\in\| N_j\|$\` By definition of $\|\_\|$\\
 $\GG\prv M_j\in \|\mnot (N_j)\|$\` By term exhaustivity (\ref{le:part})\\
$M_j=[\sigma]N$ for some $\sigma$ and $N\in\GG\vd\mnot(N_j)$\` By definition of $\|\_\|$\\
$\gna\sn\s M_j\eqd[\sigma] N$ \br $\vd\eqd$\\
$\ga\sn\Pi(\neg q\ \zij\If \top)\imm \neg q\ \mxi$\br $\imm\Imp$\\
$\ga
\sn\BAnd_{N\in\GG\vd\mnot(M_j)}\Pi(\neg q\ \zij\If \top)\imm \neg q\ \mxi$\\
\` By appropriate applications of rule  $\imm\And$\\
$\ga\sn\BAnd_{1\leq j\leq n}\BAnd_{N\in\GG\vd\mnot(M_j)}\Pi(\neg q\
\zij\If \top)\imm \neg q\ \mxi$\\ \` By appropriate applications of rule
$\imm\And$\\ 
$\ga\sn\mnotxi(\q \nxi)\imm\neg q\ \mxi$\br $\mnotxi$\\
$\ga\sn(\BAnd_{1\leq  i\leq n,xR^{i}q}\mnotxi(\q \nxi)\imm\neg q\
\mxi$
\\ \` By appropriate applications of rule  $\imm\And$\\
$\ga\sn(\BAnd_{x\in
           dom(\GG)} \mnotr(q\ \Mn)\And (\BAnd_{1\leq
           i\leq n,xR^{i}q}\mnotxi(q\ \Mn))) \imm \s \neg q\
\mxi$\\ \` By appropriate applications of rule  $\imm\And$\\
$\ga\sn(\BAnd_{x\in
           dom(\GG)} \mnotr(q\ \Mn)\And (\BAnd_{1\leq
           i\leq n,xR^{i}q}\mnotxi(q\ \Mn))) \And \Pi( \neg q\ \Mn\If G')\imm \s \neg q\
\mxi$\\
\br  $\imm\And_2$\\
$ \GG;\s\cD\sn\s\mnota(\Pi(q\ \nxi\If G))\imm \s \neg q\ \mxi$\br $\mnota\Imp$
\etab
%\enit %inner subcase
\enit %main subcase
\itc 
$$\IM = \ibnc{\foq\ga\fpp \q[\sigma]\nxi\neqd\q\mxi }{\foq \ga\fpp\q
  [\sigma]G}{\foq\ga\fpp \q\Pi( q\ \nxi\If G)\nimm\q q\ \mxi}
{\not\imm{\Imp_2}}$$
\btab $\foq\ga\fpp \q[\sigma]\nxi\neqd\q\mxi $\bs
$\gna\sn [\sigma]\nxi\eqd \s\mxi$  \br $\vd\neqd$\\
$\foq \ga\fpp \q [\sigma]G$\bs
$\gna\snp [\sigma](G)$\bi $1$\\
$\gna\sn\s\Pi( \neg q\ \nxi \If \mnotg (G))\imm \s\neg q\ \mxi$ \br $\imm\Imp$\\
$\ga\sn(\BAnd_{x\in
           dom(\GG)} \mnotr(q\ \Mn)\And (\BAnd_{1\leq
           i\leq n,xR^{i}q}\mnotxi(q\ \Mn))) \And \Pi( \neg q\ \Mn)\If G'\imm \s \neg q\ \mxi$\\  \br $\imm\And_2$\\
%$\gna\sn\s\BAnd_{x\in dom(\GG)}\BAnd_{\xrq}\mnotxi(q\ \mxi)\And \Pi(\neg
%q\ \mxi \If \mnotg(G))\imm\s \neg q\ \mxi$
%$\gna\sn(\mnota (q\ \nxi\If\top)\And \neg q\ \nxi 
%\If \mnotg (G))\imm \neg q\ \mxi$\br\\
$\gna\sn\s \mnota(\Pi(q\ \nxi\If G)) \imm \s\neg q\ \mxi$\br $\mnota\Imp$
\etab
\itc %tensor
$$ \IM = \ianc{\foq\ga\fpp \q D_{1}\nimm\q Q}{\foq\ga\fpp \q(D_{1}\tensor 
D_{2})\nimm\q Q}{ \not\imm\tensor_1}$$
\btab
$\foq\ga\fpp \q D_{1}\nimm\q Q$\bs
$\gna\sn\s \mnota (D_{1})\imm \s\neg Q$\bi $2.2$\\ 
$\gna\sn\s \mnota (D_{1})\And \s\mnota(D_{2})\imm \s \neg Q$ \br $\imm\And_1$\\
 $\gna\sn\s \mnota (D_{1}\tensor D_{2})\imm \s \neg Q$\br $\mnota\tensor$
\etab
\itc %tensor
$$ \IM = \ianc{\foq\ga\fpp \q D_{2}\nimm\q Q}{\foq\ga\fpp \q(D_{1}\tensor 
D_{2})\nimm\q Q}{ \not\imm\tensor_2}$$
 Symmetrical to the above
\itc %And
$$\IM = \ibnc{\foq\ga\fpp\q D_{1}\nimm\q Q}{\foq \ga\fpp\q D_{2}\nimm\q Q}
{\foq\ga\fpp\q( D_{1}\And D_{2})\nimm\q Q}{\not\imm\And}$$
\btab
$\foq\ga\fpp\q D_{1}\nimm\q Q$\bs
$\foq\ga\fpp\q D_{2}\nimm\q Q$\bs
$\gna\sn\s \mnota (D_{1})\imm \s \neg Q$\bi $2.2$\\
$\gna\sn\s\mnota (D_{2})\imm \s \neg Q$\bi $2.2$\\
$\gna\sn\s\mnota (D_{1})\tensor \s\mnota(D_{2})\imm \s \neg Q$\br
$\imm\tensor$\\
 $ \gna\sn\s\mnota (D_{1}\And D_{2})\imm \s \neg Q$\br $\mnotd\And$
\etab
% \itc PIXA no more
% $$\IM = 
% \ianc{\mbox{for all } \theta,n \   \ga\fpp\q\cdot [n/x] D \nimm\q
%   Q}{\foq\ga\fpp\q\PIXA D \nimm \q Q}{\not\imm\Pi}$$
% \btab
% $ \mbox{for all $\theta, n$  } \ga\fpp \q\cdot[n/x] D \nimm\q Q$\bs
%  $\gna\sn\s\cdot[t/x]\mnota ( D)\imm \s \neg Q$\bi $2.2$\\
% $\gna\sn\s\PIXA\mnota ( D)\imm \s \neg Q$\br $\imm\Pi$\\
% $\gna\sn\s\mnota (\PIXA D)\imm \s \neg Q$\br $\mnota\Pi$
% \etab
\enit
\item[\fbox{1}]
\mbox{}
%starts \vd
\bit
\itc
$$\SM = \ianc { \foq\ga\fpp\q \defp(Q,\cP\And \cD)  \nimm\q Q}{\foq\ga\fpp\q Q}{\nvd{ {\rm 
atm}}}$$
\bit
\item[\subcase] $D\inn \defp(Q,\cP)$
\btab
$ \foq\ga\fpp\q D  \nimm\q Q$\bs
$\gna\sn\s \mnotd(D) \imm \s \neg Q$\bi $2.1$\\
$\gna\sn\s\defp(\neg Q,\cP)\imm\neg Q$\`By repeated applications of
rule $\imm\tensor$\\
 $\gna\snp (Q)$\br $\vd\atm$
\etab
\item[\subcase] $D\inn \defp(Q,\cD)$
\btab
$ \foq\ga\fpp\q D  \nimm\q Q$\bs
$\gna\sn\s \mnota(D) \imm \s \neg Q$\bi $2.2$\\
$\gna\sn\s\defp(\neg Q,\cD)\imm\neg Q$\` By repeated applications of $\imm\tensor$\\
 $\gna\snp (Q)$\br $\vd\atm$
\etab
\enit
\itc
$$\SM=\ianc{}{\ga\fpp\bot}{\nvd\bot}$$
Then $\mnotg(\bot)=\s\top=\top$ and
$$\SP=\ianc{}{\gna\snp(\top)}{\vd\top}$$
\itc 
$$\SM = \ibnc{\foq\ga\fp \q G_1}{\foq\ga\fp \q G_{2}}{\foq\ga\fp \q(G_{1}\Or
G_{2})}{\nprv\Or}$$
\btab
$\foq\ga\fp \q G_1$\bs
$\foq\ga\fp \q G_2$\bs
$ \gna\snp (G_{1})$\bi $1$\\
 $\gna\snp (G_{2})$\bi $1$\\
 $\gna\sn\s \mnotg (G_{1})\And \s\mnotg (G_{2})$\br $\vd\And$\\
$ \gna\snp (G_{1} \Or G_{2})$\br $\mnotg\And$
\etab
\itc 
$$\SM =
\ianc{\foq\ga\fp\q G_1}{\foq\ga\fp\q ( G_{1}\And G_{2})}{\nprv{\And_1}}$$
\btab
$\foq\ga\fp\q G_1$\bs
 $ \gna\snp (G_{1})$ \bi $1$\\
$\gna\sn\s \mnotg (G_{1})\Or\s \mnotg (G_{2})$\br $\vd\Or$\\
$ \gna\snp (G_{1} \And G_{2})$\br $\mnotg\Or$
\etab
\itc 
$$\SM =
\ianc{\foq\ga\fp\q G_2}{\foq\ga\fp\q ( G_{1}\And
  G_{2})}{\nprv{\And_2}}$$
Symmetrical to the above.
\itc %Imp
$$\SM=\ianc{\foq\GG;\q\cD\And\q D'\fp\q G'}{\foq\ga\fp\q D' \Imp G'}{{\nprv} \Imp}$$
\btab
$\foq\GG;\q\cD\And\q D'\fp\q G' $\bs
$\GG;\s\cD\And\s D'\snp (G')$\bi $1$\\
$\gna\sn\s D'\Imp\s\mnotg(G')$\br $\vd\Imp$\\
%$\gna\sn\s (D'\Imp\mnotg(G'))$
$\gna\snp(D'\Imp G')$\br $\mnotg\Imp$\\
\etab
\itc %\PI
$$\SM=\ianc{\foq(\GG,y\oftp a);\q\cD\fp[y/x]G'}{\ga\fp\q \Pixa G'}{\nprv
  \Pi}$$
\btab
$\foq(\GG,y\oftp a);\q\cD\fp[y/x]G'$\bs
$(\GG,y\oftp a);\s\cD\sn[y/x]\mnotg(G')$\bi $1$\\
$(\GG,y\oftp a);\s\cD\sn\s\PI{x}{a}\mnotg(G')$\br $\vd\Pi$\\
$\gna\snp(\Pixa G')$\br $\mnotg\Pi$
\etab
\itc (dis)equations: immediate.
% $$ \SM =
% \ianc{\vM \not = \vN}{\ga\fpp \vM \eqd \vN}{\nprv{\eqd}}$$
% Then $\gna\sn\s  \vM \neqd \vN$ and $\gna\sn\s\mnotg( \vM \eqd \vN)$.
% \itc
% $$ \SM =
% \ianc{\vM  = \vN}{\ga\fpp \vM \neqd \vN}{\nprv{\neqd}}$$
% Then $\gna\sn\s\vM \eqd \vN$ and $\gna\sn\s\mnotg( \vM \neqd \vN)$.
\enit
\enit %main BIT
\end{proof}

\begin{Corollary}
\label{co:ccbool}
Clause complementation satisfies the boolean rules of negation.
\end{Corollary}


\renewcommand{\q}{\theta}
\renewcommand{\s}{\sigma}










