
Uniform proofs judgments:
\[
\begin{array}{ll}
\sp G & \mbox{Program $\cP$ uniformly entails $G$}\\
\sp D \imm Q & \mbox{Clause  $D$ immediately entails atom $Q$ under 
$\cP$}
\end{array}
\]

\begin{figure}
\label{fig:sf}
\[
\begin{array}{c}
% |-
% \ianc{}{}\ga\sp\top}{\top}\qquad\ianc{}{\gna\fp \perp}{S^{\nvd}_\perp}\vsk
% top and bot
\ianc{\vM = \vN}{\ga\sp \vM \eqd \vN}{S^{\vd}_{\eqd}}\qquad
\ianc{\vM \not = \vN}{\ga\sp \vM \neqd \vN}{S^{\vd}_{\neqd}}\vsk
\ianc{\ga\sp G_1\quad\ga\sp G_{2}}{\ga\sp G_{1}\And G_{2}}{S^{\vd}_\And}
\vsk
\ianc{\ga\sp G_1}{\ga\sp G_{1}\Or G_{2}}{S^{\vd}_{\Or_1}}
\qquad
\ianc{\ga\sp G_1}{\ga\sp G_{1}\Or G_{2}}{S^{\vd}_{\Or_2}}
\vsk
\ianc{D\in\cP\quad \ga\sp D \imm Q}{\ga\sp Q}{S^{\vd}_{ {\rm atm}}}\qquad
% \ianc{ \cP,G_{1}\vd_{u} G_{2}}{\cP\vd_{u} G_{1}\Imp G_{2}}{S^{\vd}_\Imp}
% \qquad
% \ianc{\cP\vd_{u} [a/x]G}{\cP\vd_{u}\Pi x. G}{S^{\vd}_\Pi^{*}}\vsk 

% immediate >>
\ianc{}{\ga\sp\perp\imm  Q}{I^{\vd}_\perp}\vsk
%\ianc{\vN = \vM}{\ga\sp q\ \vN \imm q\ \vM}{I^{\vd}_{\rm atm}}\qquad
\ianc{\mbox{for some $t:A$} \ \ga\sp  [t/x]D \imm Q}{\ga\sp \Pi x:A.D \imm Q}{I^{\vd}_\Pi}\vsk
\ianc{\ga\sp D_{1}\imm Q}{\ga\sp D_{1}\And D_{2}\imm
  Q}{I^{\vd}_{\And_1}}\qquad
\ianc{\ga\sp D_{2}\imm Q}{\ga\sp D_{1}\And D_{2}\imm
  Q}{I^{\vd}_{\And_2}}
\vsk
\ianc{\ga\sp D_{1}\imm Q\quad \ga\sp D_{2}\imm Q}{\ga\sp D_{1}\tensor D_{2}\imm Q}{I^{\vd}_\tensor}\vsk
%\ianc{\sp G}{ \ga\sp (G\Imp Q) \imm Q}{I^{\vd}_\Imp}
%\vsk
\ibnc{\ga\sp \vN\eqd\vM}{\ga\sp G}{\ga\sp (G\Imp q\ \vN) \imm q\ \vM}{I^{\vd}_{\Imp}}
\end{array}
\]
\caption{Provability  in Horn logic without existentials}
\end{figure}

We use $\gna\snp (G)$ for $\mnotg(G) = G'$ and $\gna\sn G'$; 
similarly $\gna\sn\mnotd (D)\imm\neg Q$ for $\mnotd(D) = D'$ and $\gna\sn D'\imm\neg
Q$.
\newcommand{\hence}{hence the thesis by weakening}
\begin{Theorem}[Exhaustivity]
Either $\ga\spp G$ or $ \gna\snp (G)$.
\end{Theorem}
\begin{proof}
We generalize this to:
\ben
\item
Either $\SM ::  \ga\spp G$ or $\SP :: \gna\snp ( G)$.
\item
$\IM :: \ga\spp D \imm Q$ or 
$\IP :: \gna\sn\mnotd(D) \imm \neg Q$.
\enen
\bit
\itc
$$\SM=\ianc{}{\perp_Q\imm Q}{\imm At}$$
Hence by weakening the thesis.
\itc
By the first IH either $\SM ::  \ga\spp G$ or $\SP :: \gna\snp
( G)$. By the Partition Lemma $\vM_1 = \vM_2$ or there is $\vN$ and  a substitution $\q$  such
that $\cdot\vd\q\vN\in\|\mmnot \vM_1\|$ and $\q\vN=\vM_2$. There are
four subcases:
\ben
\item %1.
\btab
 $\SM ::  \ga\spp G$\ba
$\ga\spp\vM_1=\vM_2$\ba
$\ga\spp (q\ \vM_1\If G)\imm q\ \vM_2$\br\\
hence the thesis by weakening
\etab
\item %2.
\btab
 $\SP :: \gna\snp ( G)$\ba
$\ga\spp\vM_1=\vM_2$\ba
$\gna\sn (\neg q\ \vM_1\If \mnotg(G))\imm \neg q\ \vM_2$\br\\
$\gna\sn \BAnd_{\vN\in
        \cdot\vd\mnot(\vM)}\Pi( \neg (q\ \vN)\If \top) \And  \neg (q\ \vM)\If
      \mnotg(G)\imm \neg q \vM_2$\\
\br\\
$\gna \snp(q\ \vM_1\If G)\imm \neg q\ \vM_2 $\br\ $\mnot\If$\\
hence the thesis by weakening
\etab
\item %3.
\btab
$\ga\spp G$\ba
$\ga\spp\q\vN=\vM_2$\ba
$\gna\sn(\neg q\ \q\vN\If \top)\imm \neg q\ \vM_2$\br\\
$\gna\sn\Pi(\neg q\vN\If \top)\imm \neg q\ \vM_2$\br\\
$\gna\sn \BAnd_{\vN\in
        \cdot\vd\mnot(\vM)}\Pi( \neg (q\ \vN)\If \top) \And  \neg (q\ \vM)\If
      \mnotg(G)\imm \neg q \vM_2$\\
\br\\
$\gna \snp( q\ \vM_1\If G)\imm \neg q\ \vM_2 $\br\ $\mnot\If$\\
hence the thesis by weakening
\etab
\item %4 
\btab
$\gna\snp G$\ba
$\ga\spp\q\vN=\vM_2$\ba
as above as the first hypothesis is not used.
\etab
\enen
\itc %imm\tensor
By the second IH $\ga\spp D_1\imm Q$ or $\gna\sn\mnotd(D_1)\imm \neg Q$ and $\ga\spp
D_2\imm Q$ or $\gna\sn \mnotd(D_2)\imm \neg Q$:
\ben
\item %1
\btab
 $\ga\spp D_1\imm Q$ \ba
$\ga\spp D_2\imm Q$\ba
$\ga\spp D_1\tensor D_2\imm Q$\br\\
\hence
\etab
\item %2
\btab
 $\ga\spp D_1\imm Q$ \ba
$\gna\sn \mnotd(D_2)\imm \neg Q$\ba
$\gna\sn \mnotd(D_1)\And \mnotd(D_2)\imm\neg Q$\br\\
$\gna\sn\mnotd(D_1\tensor D_2)\imm \neg Q$\br $\mnotd\tensor$\\
\hence
\etab
\item %3
\btab
 $\ga\spp D_2\imm Q$ \ba
$\gna\sn \mnotd(D_1)\imm \neg Q$\ba
$\gna\sn \mnotd(D_1)\And \mnotd(D_2)\imm\neg Q$\br\\
$\gna\sn\mnotd(D_1\tensor D_2)\imm \neg Q$\br $\mnotd\tensor$\\
\hence
\etab
\item %4
\btab
$\gna\sn \mnotd(D_1)\imm \neg Q$\ba
$\gna\sn \mnotd(D_2)\imm \neg Q$\ba
$\gna\sn \mnotd(D_1)\And \mnotd(D_2)\imm \neg Q$\br\\
$\gna\sn\mnotd(D_1\tensor D_2)\imm \neg Q$\br\\
\hence
\etab
\enen
\itc%And
By the second IH $\ga\spp D_1\imm Q$ or $\gna\sn\mnotd(D_1)\imm \neg Q$ and $\ga\spp
D_2\imm Q$ or $\gna\sn \mnotd(D_2)\imm \neg Q$:
\ben
\item %1
\btab
$\ga\spp D_1\imm Q$ \ba
$\ga\spp D_2\imm Q$\ba
$\ga\spp D_1\And D_2\imm Q$\br\\
\hence
\etab
\item %2
\btab
 $\ga\spp D_1\imm Q$ \ba
$\gna\sn \mnotd(D_2)\imm \neg Q$\ba
$\ga\spp D_1\And D_2\imm Q$\br\\
\hence
\etab
\item %3
\btab
 $\ga\spp D_2\imm Q$ \ba
$\gna\sn \mnotd(D_1)\imm \neg Q$\ba
$\ga\spp D_1\And D_2\imm Q$\br\\
\hence
\etab
\item %4
\btab
$\gna\sn \mnotd(D_1)\imm \neg Q$\ba
$\gna\sn \mnotd(D_2)\imm \neg Q$\ba
$\gna\sn \mnotd(D_1)\tensor\mnotd(D_2)\imm \neg Q$\br\\
$\gna\sn\mnotd(D_1\And D_2)\imm \neg Q$\br\\
\hence
\etab
\enen
\itc %\Pi imm
By the second IH $\ga\spp [t/x]D\imm Q$ or $\gna\sn\mnotd([t/x]D)\imm\neg Q$:
\ben
\item %1
\btab
$\ga\spp [t/x]D\imm Q$\ba
$\ga\spp\PIXA D\imm Q$\br\\
\hence
\etab
\item %2
\btab
$\gna\sn\mnotd([t/x]D)\imm\neg Q$\ba
$\gna\sn \PI{x}{A}\mnotd(D)\imm\neg Q$\br\\
$\gna\sn\mnotd(\PIXA D)$\br\\
\hence
\etab
\enen
%start \vd G
\itc
By the second IH $\ga\spp D\imm Q$ or $\gna\sn\mnotd(D)\imm \neg Q$:
\ben
\item %1
\btab
$\ga\spp D\imm Q$\ba
$\ga\spp Q$\br\\
\hence
\etab
\item %2
\btab
 $\gna\sn\mnotd(D)\imm \neg Q$\ba
$\gna\snp(Q)$\br\\
\hence
\etab
\enen
\itc
By the first IH $\ga\spp G_1$ or $\gna\snp(G_1)$ and $\ga\spp G_2$ or
 $\gna\snp(G_2)$:
\ben
\item % 1
\btab
$\ga\spp G_1$\ba
$\ga\spp G_2$\ba
$\ga\spp G_1\And G_2$\br\\
\hence
\etab
\item %2
\btab
$\ga\spp G_1$\ba
$\gna\snp(G_2)$\ba
$\gna\snp(G_2)\Or\mnotg(G_1)$\br\\
$\gna\snp(G_1\And G_2)$\br\\
\hence
\etab
\item %3
\btab
$\ga\spp G_2$\ba
$\gna\snp(G_1)$\ba
$\gna\snp(G_2)\Or\mnotg(G_1)$\br\\
$\gna\snp(G_1\And G_2)$\br\\
\hence
\etab
\item %4
\btab
$\gna\snp (G_1)$\ba
$\gna\snp(G_2)$\ba
$\gna\snp(G_2)\Or\mnotg(G_1)$\br\\
$\gna\snp(G_1\And G_2)$\br\\
\hence
\etab
\enen
\itc %or
By the first IH $\ga\spp G_1$ or $\gna\snp(G_1)$ and $\ga\spp G_2$ or
 $\gna\snp(G_2)$:
\ben
\item % 1
\btab
$\ga\spp G_1$\ba
$\ga\spp G_2$\ba
$\ga\spp G_1\Or G_2$\br\\
\hence
\etab
\item %2
\btab
$\ga\spp G_1$\ba
$\gna\snp(G_2)$\ba
$\ga\spp G_2\Or G_1$\br\\
\hence
\etab
\item %3
\btab
$\ga\spp G_2$\ba
$\gna\snp(G_1)$\ba
$\ga\spp G_2\Or G_1$\br\\
\hence
\etab
\item %4
\btab
$\gna\snp( G_1)$\ba
$\gna\snp(G_2)$\ba
$\gna\snp(G_2)\And\mnotg(G_1)$\br\\
$\gna\snp(G_1\Or G_2)$\br\\
\hence
\etab
\enen
\itc The (dis)equality case follows from the decidability of the $=$
 judgment to be detailed later in the unification logic judgment.
\enit% main bit
\end{proof}

