\newcommand{\less}{\prec} %change
\renewcommand{\ga}{}
\renewcommand{\gna}{}
\renewcommand{\SP}{{\cal S}^-}
\renewcommand{\SM}{{\cal S}^+}
\renewcommand{\IP}{{\cal I}^-}
\renewcommand{\IM}{{\cal I}^+}
\renewcommand{\SP}{}
\renewcommand{\SM}{}
\renewcommand{\IP}{}
\renewcommand{\IM}{}
%\newcommand{\semic}{::}
\newcommand{\semic}{}
%\renewcommand{\q}{[n/x]  }
%\renewcommand{\s}{[t/x]  }
\newcommand{\foq}{\mbox{\textrm{for all }} \q\,}
\newcommand{\hence}{hence the thesis by weakening.}

\subsection{Terminating Horn programs}

\begin{Definition}
\label{def:goalorder}
Given a program $\cP$, define the binary relation $G_1\less G_2$ with the
intended meaning of ``$G_1$ can arise as a subgoal of $G_2$'' by the
following clauses:
\[
\begin{array}{lr}
G_1\less G_1\And G_2\\
G_2\less G_1\And G_2\\
G_1\less G_1\Or G_2\\
G_2\less G_1\Or G_2\\
\q G\less \exa G&\mbox{for all subst.\  } q\\
G\less Q & \mbox{if } (Q\If G)\in\cP
\end{array}
\]
Moreover we require $\less$ to be closed under substitutions, \ie
$G_1\less G_2$ entails for all $\rho$ $\rho G_1\less \rho G_2$.
We say that $\cP$ is \emph{terminating} whenever the above relation is
well-founded, \ie it admits no infinite descending chains.
\end{Definition}

Uniform proofs judgments (Figures \ref{fig:sf} and \ref{fig:imm}):
\[
\begin{array}{ll}
\ga\sp G & \mbox{Program $\cP$  uniformly entails
  $G$}\\
\ga\fp G & \mbox{Program $\cP$  uniformly denies $G$}\\
\ga\sp D \imm Q & \mbox{Clause  $D$ immediately entails atom $Q$ under 
$\cP$}\\
\ga\fp D \imm Q & \mbox{Clause  $D$ immediately denies atom $Q$ under $\cP$}
\end{array}
\]


\begin{figure}
\label{fig:sf}
\[
\begin{array}{c}
% |-
 \ianc{}{\ga\sp\top}{\vd\top}\qquad\ianc{}{\gna\fp \perp}{{\nprv}_\perp}\vsk
% top and bot
\ianc{\vM = \vN}{\ga\sp \vM \eqd \vN}{{\prv\eqd}}\qquad
\ianc{\vM \not = \vN}{\ga\fp \vM \eqd \vN}{{\nprv\eqd}}\vsk
\ianc{\vM \not = \vN}{\ga\sp \vM \neqd \vN}{{\prv\neqd}}\qquad
\ianc{\vM  = \vN}{\ga\fp \vM \neqd \vN}{{\nprv\neqd}}\vsk
\ibnc{\ga\sp G_1}{\ga\sp G_{2}}{\ga\sp G_{1}\And G_{2}}{{\prv}\And}
\qquad
\ibnc{\ga\fp G_1}{\ga\fp G_{2}}{\ga\fp G_{1}\Or G_{2}}{{\nprv}\Or}
\vsk
\ianc{\ga\sp G_1}{\ga\sp G_{1}\Or G_{2}}{{\prv\Or_1}}
\qquad
\ianc{\ga\fp G_1}{\ga\fp G_{1}\And G_{2}}{{\nprv\And_1}}\vsk
\ianc{\ga\sp G_2}{\ga\sp G_{1}\Or G_{2}}{{\prv\Or_2}}
\qquad
\ianc{\ga\fp G_2}{\ga\fp G_{1}\And G_{2}}{{\nprv\And_2}}
% \qquad i\in 1\ \mbox{or} \ 2
\vsk
\ianc{\ga\sp[t/x]G}{\ga\sp\exa G}{\vd\exists}
\qquad
\ianc{\foq\gna\fp\q G}{\gna\fp\exa G}{\nvd\exists}
\vsk
\ianc{ \ga\sp def(Q) \imm Q}{\ga\sp Q}{{ {\rm atm}}}
\qquad
\ianc{ \gna\fp def(Q) \nimm Q}{\ga\fp Q}{{\nprv {\rm atm}}}\vsk
% HORN --> HHF
% \ianc{\GG;\cD\And D \sp G}{\ga\sp D \Imp G}{{\prv} \Imp}
% \qquad
% \ianc{\GG;\cD\And D \fp G}{\ga\fp D \Imp G}{{\nprv} \Imp}
% \vsk
% \ianc{(\GG,y\oftp A);\cD\sp[y/x]G}{\ga\sp \PIXA G}{{\prv} \Pi}
% \qquad
% \ianc{(\GG,y\oftp A);\cD\fp[y/x]G}{\ga\fp \PIXA G}{{\nprv} \Pi}
\end{array}
\]
\caption{Provability and Denial}
\end{figure}

\begin{figure}
\label{fig:imm}
\[
\begin{array}{c}
% immediate >>
\ianc{}{\ga\sp\perp\imm  Q}{\imm\perp}\qquad
\ianc{}{\ga\fp \top\nimm Q}{\not\imm \top}\vsk
%\ianc{\vN = \vM}{\ga\sp q\ \vN \imm q\ \vM}{\imm{\rm atm}}\qquad
%\ianc{\vN \neq \vM}{\ga\fp q\ \vN \nimm q\ \vM}{\not\imm{\rm atm}}\vsk
\ibnc{\mbox{for some $\vd t\hastype A$}}{ \ga\sp  [t/x]D \imm
  Q}{\ga\sp \PIXA D \imm Q}{\imm\Pi}\qquad
\ibnc{\mbox{for all $\vd n\hastype A$} }{ \ga\fp [n/x]D \nimm
  Q}{\ga\fp \PIXA D \nimm Q}{\not\imm\Pi}\vsk
\ianc{\ga\sp D_{1}\imm Q}{\ga\sp D_{1}\And D_{2}\imm Q}{\imm{\And_1}}\qquad
\ianc{\ga\fp D_{1}\nimm Q}{\ga\sp D_{1}\tensor D_{2}\nimm
  Q}{\not\imm{\tensor_1}}\vsk
\ianc{\ga\sp D_{2}\imm Q}{\ga\sp D_{1}\And D_{2}\imm Q}{\imm{\And_2}}\qquad
\ianc{\ga\fp D_{2}\nimm Q}{\ga\sp D_{1}\tensor D_{2}\nimm Q}{\not\imm{\tensor_2}}\vsk
\ibnc{\ga\sp D_{1}\imm Q}{ \ga\sp D_{2}\imm Q}{\ga\sp D_{1}\tensor D_{2}\imm 
Q}{\imm\tensor}\qquad
\ibnc{\ga\fp D_{1}\nimm Q}{\ga\fp D_{2}\nimm Q}{\ga\fp D_{1}\And D_{2}\nimm
Q}{\not\imm\And}\vsk
\ibnc{\ga\sp\vN\eqd\vM}{\ga\sp G}{ \ga\sp ( q\  \vN\If G) \imm q\ \vM}{\imm\Imp}
\vsk
\ianc{\ga\fp \vN\eqd\vM}{\ga\fp (q\ \vN\If G) \nimm q\ \vM}{\not\imm{\Imp_1}}
\qquad
\ibnc{\ga\fp \vN\neqd\vM}{\fp G} {\ga\fp (q\ \vN\If G) \nimm q\ \vM}{\not\imm{\Imp_2}}
% to avoid dependency pos-neg 
% \ianc{\ga\sp Q'\imm Q\quad\sp G}{ \ga\sp (G\Imp Q') \imm Q}{\imm\Imp}
% \vsk
% \ianc{\ga\fp Q'\nimm Q}{ \ga\fp (G\Imp Q') \nimm Q}{\not\imm{\Imp_1}}
% \qquad
% \ianc{\ga\sp Q'\imm Q\quad\fp G} { \ga\fp (G\Imp Q') \nimm Q}{\not\imm{\Imp_2}}
\end{array}
\]
\caption{Immediate Entailment and Denial}
\end{figure}


Note that $\not\imm\Pi$ and $\nvd\exists$ are pseudo-rules, given the
meta-linguistic extensional universal quantification on all terms. Also
remark the `guards' in the immediate denial rules are constructed so
as to make the positive and negative judgment mutually independent.

\begin{Theorem}[Termination]
\label{thm:termination}
Assume $\cP$ is terminating. Then for every  goal either $\ga\sp
G$ or $ \gna\fp G$.
\end{Theorem}
\begin{proof}
We generalize this to: 
%such that $x\not\in dom(\s)\cap dom(\q).
\ben
\item
Either there is a (well-typed substitution) $\s$ such that $\SM \semic   \ga\sp \s G$ or for all
substitutions $\q$ $\SP \semic  \gna\fp\q G$.
\item
Either there is a substitution  $\s$ such that $\IM \semic  \ga\sp \s  D \imm \s Q$
or  for all substitutions $\q$ 
$\IP \semic  \gna\fp \q D \imm  \q Q$.
\enen
We proceed by mutual induction on the goal ordering induced by $\cP$
terminating and on the structure of $D$:
\bit
\itc $D=\s\perp=\perp$. Then
$$\IM=\ianc{}{\ga\sp\perp_Q\imm Q}{\imm At}$$
Hence by weakening the thesis.
\itc $ D=\q\top=\top\ \foq$. Then
$$\IP=\ianc{}{\gna\fp\top_Q\imm Q}{\nimm At}$$
Hence by weakening the thesis.
\itc $D=Q\If G$. Hence for all $\rho $ $\rho G\less \rho Q$ by termination.
By the first IH either $\SM \semic   \ga\sp \s G$ or $\foq\SP \semic \gna\fp\q
G$ and $\vM_1=\vM_2$ or $ \vM_1=\vM_2$. There are
four subcases:
\ben
\item %1.
\btab
 $\SM \semic   \ga\sp \s G$\ba
$\ga\sp\s\vM_1\eqd \s\vM_2$\br\\
$\ga\sp \s(q\ \vM_1\If G)\imm \s(q\ \vM_2)$\br\\
hence the thesis by weakening.
\etab
\item %2.
\btab
 $\SP \semic    \foq\gna\fp \q G$\ba
$\foq\ga\sp\q\vM_1\eqd \q\vM_2$\br\\
$\foq\ga\fp\q(\vM_1\neqd \vM_2)$\br\\
$\foq\gna\fp\q ( q\ \vM_1\If G)\imm  \q q\ \vM_2$\br\\
hence the thesis by weakening.
\etab
\item %3.
\btab
$\ga\sp \s G$\ba
$\foq\ga\fp\q\vM_1\eqd \q\vM_2)$\br\\
$\foq\gna\fp \q( q\ \vM_1\If G)\imm \q( q\ \vM_2)$\br\\
hence the thesis by weakening.
\etab
\item %4 
\btab
$\foq\gna\fp \q G$\ba
$\foq\gna\fp\q\vM_1\eqd \q\vM_2$\br\\
$\foq\gna\fp \q( q\ \vM_1\If G)\imm \q( q\ \vM_2)$\br\\
hence the thesis by weakening.
\etab
\enen
\itc %imm\tensor
By the second IH $\ga\sp\s D_1\imm\s Q$ or for all $\gna\fp \q D_1
\imm  \q Q$ and $\ga\sp
\s D_2\imm\s Q$ or for all $\gna\fp \q D_2 \imm  \q Q$:
\ben
\item %1
\btab
 $\ga\sp \s D_1\imm\s Q$ \ba
$\ga\sp \s D_2\imm\s Q$\ba
$\ga\sp \s(D_1)tensor \s (D_2)\imm \s Q$\br\\
$\ga\sp \s(D_1\tensor D_2)\imm \s Q$\br\\
\hence
\etab
\item %2
\btab
 $\ga\sp \s D_1\imm \s Q$ \ba
$\foq\gna\fp \q D_2 \imm \q Q$\ba
$\foq\gna\fp \q D_1\tensor \q D_2 \imm \q Q$\br \\
$\foq\gna\fp \q (D_1\tensor  D_2) \imm \q Q$\br \\
\hence
\etab
\item %3
\btab
 $\ga\sp \s D_2\imm \s Q$ \ba
$\foq\gna\fp\q  D_1 \imm\q  Q$\ba
$\foq\gna\fp \q D_1\tensor \q D_2 \imm\q  Q$\br \\
$\foq\gna\fp \q (D_1\tensor  D_2) \imm\q  Q$\br \\
\hence
\etab
\item %4
\btab
$\foq\gna\fp \q D_1 \imm \q Q$\ba
$\foq\gna\fp \q D_2 \imm  \q Q$\ba
$\foq\gna\fp \q D_1\tensor \q D_2 \imm \q Q$\br \\
$\foq\gna\fp \q (D_1\tensor  D_2) \imm \q Q$\br \\
\hence
\etab
\enen
\itc%And
By the second IH $\ga\sp \s D_1\imm \s Q$ or $\foq\gna\fp \q D_1 \imm \q Q$ and $\ga\sp\s
D_2\imm\s Q$ or $\foq\gna\fp\q  D_2 \imm \q Q$:
\ben
\item %1
\btab
$\ga\sp \s D_1\imm\s Q$ \ba
$\ga\sp \s D_2\imm\s Q$\ba
$\ga\sp\s (D_1\And D_2)\imm \s Q$\br\\
\hence
\etab
\item %2
\btab
 $\ga\sp\s D_1\imm \s Q$ \ba
$\foq\gna\fp  \q D_2 \imm \q  Q$\ba
$\ga\sp \s (D_1\And D_2)\imm\s Q$\br\\
\hence
\etab
\item %3
\btab
 $\ga\sp \s D_2\imm\s Q$ \ba
$\foq\gna\fp\q  D_1 \imm \q Q$\ba
$\ga\sp \s(D_1\And D_2)\imm \s Q$\br\\
\hence
\etab
\item %4
\btab
$\foq\gna\fp\q  D_1 \imm  \q Q$\ba
$\foq\gna\fp\q  D_2 \imm  \q Q$\ba
$\foq\gna\fp  \q D_1 \And \q D_2 \imm \q Q$\br\\
$\foq\gna\fp\q( D_1\And D_2) \imm  \q Q$\br\\
\hence
\etab
\enen
\itc %\Pi imm
By the second IH for some $t$, $\ga\sp \s\cdot[t/x] D\imm\s\cdot[t/x] Q$ or for all $n$
 $\foq\gna\fp \q\cdot[n/x] D\imm\q\cdot[n/x] Q$:
\ben
\item %1
\btab
$\ga\sp \s\cdot[t/x] D\imm\s\cdot[t/x] Q$\ba
$\ga\sp\s\PIXA D\imm \s\cdot[t/x] Q$\br\\
$\ga\sp\s\cdot[t/x]\PIXA D\imm \s\cdot[t/x] Q$\`Trivially \\
\hence
\etab
\item %2
\btab
$\foq\gna\fp \q\cdot[n/x] D)\imm \q\cdot[n/x] Q$\ba
$\foq\gna\fp \q(\PI{x}{A} D)\imm \q\cdot[n/x] Q$\br\\
$\foq\gna\fp \q\cdot[n/x](\PI{x}{A} D)\imm \q\cdot[n/x] Q$\`Trivially\\
\hence
\etab
\enen
%start \vd G
\itc
By the second IH $\ga\sp \s D\imm\s Q$ or $\foq\gna\fp \q D\imm \q Q$:
\ben
\item %1
\btab
$\ga\sp \s D\imm\s Q$\ba
$\ga\sp\s Q$\br\\
\hence
\etab
\item %2
\btab
$\foq\gna\fp \q D\imm\q  Q$\ba
$\foq\gna\fp\q Q$\br\\
\hence
\etab
\enen
\itc
By the first IH $\ga\sp\s G_1$ or $\foq\gna\fp\q G_1 $ and $\ga\sp\s  G_2$ or
 $\foq\gna\fp\q G_2 $:
\ben
\item % 1
\btab
$\ga\sp\s  G_1$\ba
$\ga\sp\s  G_2$\ba
$\ga\sp\s  (G_1\And G_2)$\br\\
\hence
\etab
\item %2
\btab
$\ga\sp\s  G_1$\ba
$\foq\gna\fp\q G_2 $\ba
$\foq\gna\fp\q (G_1\And G_2 )$\br\\
\hence
\etab
\item %3
\btab
$\ga\sp\s  G_2$\ba
$\foq\gna\fp\q G_1 $\ba
$\foq\gna\fp\q (G_1\And G_2) $\br\\
\hence
\etab
\item %4
\btab
$\foq\gna\fp\q G_1 $\ba
$\foq\gna\fp\q G_2 $\ba
$\foq\gna\fp\q (G_1\And G_2) $\br\\
\hence
\etab
\enen
\itc %or
By the first IH $\ga\sp\s  G_1$ or $\foq\gna\fp\q G_1 $ and $\ga\sp\s  G_2$ or
 $\foq\gna\fp\q G_2 $:
\ben
\item % 1
\btab
$\ga\sp\s  G_1$\ba
$\ga\sp\s  G_2$\ba
$\ga\sp\s  (G_1\Or G_2)$\br\\
\hence
\etab
\item %2
\btab
$\ga\sp\s  G_1$\ba
$\foq\gna\fp\q G_2 $\ba
$\ga\sp\s  (G_2\Or G_1)$\br\\
\hence
\etab
\item %3
\btab
$\ga\sp\s  G_2$\ba
$\foq\gna\fp\q G_1 $\ba
$\ga\sp\s   (G_2\Or G_1)$\br\\
\hence
\etab
\item %4
\btab
$\foq\gna\fp\q  G_1 $\ba
$\foq\gna\fp\q G_2 $\ba
$\foq\gna\fp\q (G_1\Or G_2) $\br\\
\hence
\etab
\enen
\itc %exa
By the first IH for some $t$, $\ga\sp\s \cdot[t/x] G$ or for all $n$, $\foq\gna\fp\q\cdot[n/x] G $:
\ben
\item %1
\btab
$\ga\sp\s \cdot[t/x]G$\ba
$\ga\s(\exa G)$\br\\
$\ga\sp\s\cdot[t/x](\exa G)$\`Trivially\\
\hence
\etab
\item 
\btab
$\foq\gna\fp\q\cdot[n/x] G$\ba
$\foq\gna\fp\q(\exa G)$\br\\
$\foq\gna\fp\q\cdot[n/x](\exa G)$\`Trivially\\
\etab
\enen
\itc The (dis)equality case follows from the decidability of the $\eqd $
 judgment to be detailed later in the unification logic judgment.
\enit% main bit
\end{proof}

\begin{Lemma}
\label{le:derivs}
The following is a derived rule of inference:

$$
%\ianc{\mbox{for some $\GG\vd t\hastype A$}}{ \ga\sp  [t/x]D \imm
 % Q}{\ga\sp \PIXA D \imm Q}{\imm\Pi}
\ianc{\mbox{for some } \rho\,\ga\sp\rho\vN\eqd\vM}{\ga\sp\Pi(q\
  \vN\If \top)\imm q\ \vM}{\Pi\rho\imm}
$$
\end{Lemma}
\begin{proof}
A straightforward induction on the number of free variables in $\vN$.
\end{proof}

% Note that in the above rules denial depends on provability, while this 
% is not the case for the system in Figure \ref{fig:sf}. Still they make 
% the main proof easier.

\renewcommand{\snp}{\vd_{\!\PM}\s\mnotg}
We use $\gna\sn\mnotg (G)$ for $\gna\vd\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{\foq}{\mbox{\textrm{for all }} \q\,}
\renewcommand{\SP}{{\cal S}^+}
\renewcommand{\SM}{{\cal S}^-}
\renewcommand{\IP}{{\cal I}^+}
\renewcommand{\IM}{{\cal I}^-}

\begin{Proposition}[Exhaustivity]
\label{thm:exhau}
If $\ga\fpp G$ then $ \gna\sn\mnotg (G)$.
\end{Proposition}
\begin{proof}
We generalize this to:
\ben
\item
If   $\foq\SM ::  \ga\fpp \q G$ then there is a  $\s$ such that  $\SP :: \gna\snp (G)$.
\item
If, for all  $\q$,
%such that $dom(\q) = var(def(Q))$, 
$\IM :: \ga\fpp \q (def(Q)) \nimm \q Q$, then here is a $\s$ such that 
% there is a substitution $\q$ such that $dom(\q) = var(def(\neg Q))$ and
$\IP :: \ga\sn \s (def(\neg Q)) \imm \s \neg Q$.
\enen
The proof is by mutual induction on the structure of $\SM$ and $\IM$.
\bit
\itc 
$$\IM = \ianc{}{\ga\fpp\top\nimm Q}{\not\imm\top}$$
as, $\foq\q\top=\top$.  Then $\s\mnotd (\top) =\s \perp=\perp$ and
$$ \IP = \ianc{}{\ga\sn\perp\imm \s \neg Q}{\imm\perp}$$
\newpage
\itc
$$ \IM = \ianc{\foq\ga\fpp\q\vN \eqd \q\vM}{\foq\ga\fpp \q(q\ \vN \If
  G)\nimm\q q\ \vM}{\not\imm\Imp^1}$$
\btab
$\foq\ga\fpp\q\vN \eqd \q\vM$\bv
$\vN \not= \q\vM$\br\\
$\cdot\prv \vM\not\in\| \vN\|$\` By definition of $\|\_\|$\\
 $\cdot\prv \vM\in \|\mnot (\vN)\|$\` By term exhaustivity (\ref{le:part})\\
$\vM=\rho\vec{S}$ for some $\rho$ and $\vec{S}\in\mnot(\vN)$\` By definition of $\|\_\|$\\
$\ga\sn\s \vM\eqd\rho\cdot\s\vec{S}$ for some $t$\br\ and composition
of subst.\\
$\ga\sn\s\Pi(\BAnd_{\vec{S}\in\mnot(\vN)} q\ \vec{S}\If \top)\imm\s
\neg q\ \vM$\br\\
$\ga\sn\s(\Pi(\BAnd_{\vec{S}\in\mnot(\vN)} q\
\vec{S}\If \top)\And \neg q\ \vM \If \mnotg(G))\imm \s \neg q\ \vM$\\\br\\
 $\ga\sn\s\mnotd(q\ \vN\If G)\imm \s \neg q\ \vM$\br
\etab
\itc 
$$\IM = \ibnc{\foq\ga\fpp \q\vN\neqd\q\vM }{\foq \ga\fpp\q G}{\foq\ga\fpp \q( q\ \vN\If G)
\nimm\q q\ \vM} {\not\imm{\Imp_2}}$$
\btab
$\foq\ga\fpp \q\vN\neqd\q\vM $\bv
$\ga\sn \s\vN\eqd \s\vM$ for some $t$ \br\\
$\foq \ga\fpp \s G$\bv
$\gna\snp (G)$\bi $1$\\
$\ga\sn\s( \neg q\ \vN \If \mnotg (G))\imm \s\neg q\ \vM$ \br\\
$\ga\sn\s(\Pi(\BAnd_{\vec{S}\in\mnot(\vN)} q\
\vec{S}\If \top)\And \neg q\ \vM \If \mnotg(G))\imm\s q\ \vM$\\\br\\
%$\gna\sn(\mnotd (q\ \vN\If\top)\And \neg q\ \vN 
%\If \mnotg (G))\imm \neg q\ \vM$\br\\
$\ga\sn\s \mnotd(q\ \vN\If G) \imm \s\neg q\ \vM$\br
\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$\bv
$\ga\sn\s \mnotd (D_{1})\imm \neg Q$\bi $2$\\ 
$\ga\sn\s \mnotd (D_{1})\And 
\mnotd(D_{2})\imm \s \neg Q$ \br $\nprv{\And_1}$\\
 $\ga\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$\bv
$\ga\sn\s \mnotd (D_{1})\imm \s \neg Q$\bi $2$\\
$\ga\sn\s\mnotd (D_{2})\imm \s \neg Q$\bi $2$\\
$\ga\sn\s\mnotd (D_{1})\tensor \s\mnotd(D_{2})\imm \s \neg Q$\br
$\imm\tensor$\\
 $ \ga\sn\s\mnotd (D_{1}\And D_{2})\imm \s \neg Q$\br \\
\etab
\itc
$$\IM = 
\ianc{\mbox{for all $\q$, } \q \ga\fpp\q\cdot [n/x] D \nimm\q
  Q}{\foq\ga\fpp\q\PIXA D \nimm \q Q}{\not\imm\Pi}$$
\btab
$ \foq \ga\fpp \q\cdot[n/x] D \nimm\q Q$\bv
 $\ga\sn\s\cdot[t/x]\mnotd ( D)\imm \s \neg Q$\bi $2$\\
$\ga\sn\s\mnotd (\PIXA D)\imm \s \neg Q$\br
\etab
\itc
$$\SM = \ianc{ \foq\ga\fpp\q def(Q) \nimm\q Q}{\foq\ga\fpp\q Q}{\nvd{ {\rm 
atm}}}$$
\btab
$ \foq\ga\fpp\q def(Q) \nimm\q Q$\bv
$\ga\sn\s def(\s \neg Q) \imm \s \neg Q$\bi $2$\\
 $\ga\snp (Q)$\br
\etab
\itc
$$\SM=\ianc{}{\gna\fpp\bot}{\nvd\bot}$$
Then $\ga\snp (\bot)=\s\top=\top$ and
$$\SP=\ianc{}{\ga\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$\bv\\
$\foq\ga\fp \q G_2$\bv\\
$ \ga\snp (G_{1})$\bi $1$\\
 $\ga\snp (G_{2})$\bi $1$\\
 $\ga\sn\s \mnotg (G_{1})\And \s\mnotg (G_{2})$\br\\
$ \ga\snp (G_{1} \Or G_{2})$\br
\etab
\itc 
$$\SM =
\ianc{\foq\ga\fp\q G_1}{\foq\ga\fp\q ( G_{1}\And G_{2})}{\nprv{\And_i}}$$
\btab
$\foq\ga\fp\q G_1$\bv
 $ \ga\snp (G_{1})$ \bi $2$
$\ga\sn\s \mnotg (G_{1})\Or \mnotg (G_{2})$\br\\
$ \ga\snp (G_{1} \And G_{2})$\br
\etab
\itc 
$$\SM =
\ianc{\foq\ga\fp\q G_2}{\foq\ga\fp\q ( G_{1}\And
  G_{2})}{\nprv{\And_i}}$$
Symmetrical to the above.
\itc (dis)equations: delayed to unification logic
% $$ \SM =
% \ianc{\vM \not = \vN}{\ga\fpp \vM \eqd \vN}{\nprv{\eqd}}$$
% Then $\ga\sn\s  \vM \neqd \vN$ and $\ga\sn\s\mnotg( \vM \eqd \vN)$.
% \itc
% $$ \SM =
% \ianc{\vM  = \vN}{\ga\fpp \vM \neqd \vN}{\nprv{\neqd}}$$
% Then $\ga\sn\s\vM \eqd \vN$ and $\ga\sn\s\mnotg( \vM \neqd \vN)$.
\enit
\end{proof}