We are now in the position to prove the main result of this Chapter,
namely that clause complementation satisfies the boolean rules of
negation, in the form of exclusivity and exhaustivity. We remark that
this holds due to the fact that context schemata allow to pose only
`well-behaved' goals. For example, consider the query $G\equiv\neg
even(0)\Imp even(s(s(0)))$, which is such that both $\emp\vd_{even} G$
and $\emp\vd_{\neg even} \mnotg(G)$ are provable. By definition of
schema satisfaction, this is not a legal query. Similarly, the
following counter-example to exhaustivity $\emp\vd_{even} \PI{x}{nat}
even(x)$ is not allowed. Moreover, the Context Preservation Theorems
(Theorem \ref{thm:poscntpres} and \ref{thm:negcntpres}) guarantees
that, from allowed run-time contexts and goals, only allowed subgoals
are generated.


\section{Exclusivity}
\label{sec:excluproof}

\renewcommand{\ga}{\Gamma;\cD }
\renewcommand{\gna}{ \Gamma;\cD }
\renewcommand{\q}{}
\renewcommand{\PP}{\cP}
\renewcommand{\PM}{\cP}
\renewcommand{\ex}{e_x}
\newcommand{\vnx}{ \ol{N_{\ex}^i}}
\renewcommand{\vN}{\ol{N_n}}
\renewcommand{\vM}{\ol{M_n}}
\newcommand{\vT}{\ol{T_n}}
\renewcommand{\vS}{\ol{S_n}}
\renewcommand{\sn}{\vd_{\cP}}
\renewcommand{\spp}{\vd_{\cP}}
\renewcommand{\sp}{\vd_{\cP}}
\renewcommand{\snp}{\vd_{\cP}\mnotg}
\renewcommand{\PIXA}{\PI{x}{a}}


We use $\ga\sn\mnotg (G)$ for $\mnotg(G) = G'$ and $\gna\sn G'$;
$\ga\sn\mnotd (D)\imm\neg Q$ for $\mnotd(D) = D'$ and $\gna\sn
D'\imm\neg Q$; similarly for $\mnota$.  Recall that $D\in
\defp(q,\cP\And\cD)$ denotes that $D$ is a top-level conjunct in the
static or dynamic definition of $q$. Similarly, $D\in \defp(\neg
q,\cP\And\cD)$ denotes that $D$ is a top-level disjunct in the static
or dynamic definition of $\neg q$. We use $\cP$ to denote the
conjunction of a positive program $\cP^+$ and its negation
$\cP^-=\mnotd(\cP^+)$. Finally, since by Corollary \ref{co:clocomp} a
(run-time) context is closed under negation, $D'\in \defp(\neg q,\cD)$
iff $D'\equiv \mnota(D)$ for $D\in \defp(\neg q,\cD)$.

\begin{Theorem}[Exclusivity] 
\label{thm:exclu}
Let $\models_{\!\csa}\ald(\PP)$ and $\ga\ins\csa$.
For every goals such that 
%$\emp\sla G \ins\csa$
$\ga\sla G \ins\csa$
, it is not the case that both
$\ga\spp G$ and $ \gna\snp (G)$.
\end{Theorem}
\begin{proof}
We generalize this to; let $D\in \defp(q,\cP\And\cD)$:
\ben
\item It is not the case that there is $\SP ::  \ga\spp G$ and there is $\SM
:: \gna\snp ( G)$. 
\item
 It is not the case that
$\IP :: \ga\spp  D \imm Q$ and
$\IM :: \gna\sn D' \imm \mnotg( Q)$, for all $D'\in\defp(\neg q,\cP\And\cD)$.
\enen
We proceed by mutual induction on the structure of $\IP$ and $\SP$,
by assuming their existence. Note that immediately $\mnotg(Q)=\neg Q$. Moreover, the
negative definition implies an atom iff so does every disjunct; thus
it will suffice to show absurdity for one of the latter.
The second statement thus unfolds in four distinct cases:
\ben %start four cases
\item[\fbox{2.1}] %first case
 Let $D\in \defp(q,\PP)$ 
It is not the case that:
$\IP :: \ga\spp  D \imm Q$ and
$\IM :: \gna\sn \mnotd(D)\imm \neg Q$.
\bit
\itc
$$\IP=\ianc{}{\ga\spp\perp\imm  Q}{\imm\perp}$$
But there can be no proof of $\neg Q$ from  $\mnotd(\perp)=\top$.
\itc
$$\IP=\ibnc{\ga\spp\vN\eqd \vM}{\ga\spp G}{\ga\spp (q\ \vN\If G)\imm q\ \vM}{\imm\Imp}$$
and
$\IM$ ends in $\gna\sn \mnotd (q\ \vN\If G)\imm \neg q\
\vM$:
\btab
$\ga\spp\vN\eqd \vM$\bs
$\cdot\vd\vM\in\|\vN\|$ $(*)$\`By definition of \ of $\|\_\|$\\ 
$\SP_1::\ga\spp G$  \bs
% $\gna\sn (\neg q\ \vM_1\If \mnotg(G))\imm \neg q\ \vM_2$\bv
$\gna\sn \BAnd_{\vS\in\mnot(\vN)}\Pi( \neg q\ \vS\If \top) \And  \neg q\ \vN\If
      \mnotg(G)\imm \neg q\ \vM$\` By rule $\mnotd\Imp$
\etab
\bit
\item[\subcase]
\btab
$\gna\sn \BAnd_{\vS\in\mnot(\vN)}\Pi( \neg q\ \vS\If \top)\imm\neg q\
      \vM$\bv
$\gna\sn \Pi( \neg q\ \vS\If \top)\imm\neg q\
      \vM$ for some $\vS$ \bv
$\gna\sn[\s](\neg q\ \vS)\If\top\imm \neg q\ \vM$  for some $\sigma$\bv
$\gna\sn[\s]\vS\eqd\vM$\bv
$\cdot\vd\vM\in\|\mnot (\vN)\|$\` By definition of $\| \_ \|$\\
$\perp$\` By term exclusivity with $(*)$
\etab
\item[\subcase]
\btab
$\gna\sn\neg q\ \vN\If
      \mnotg(G)\imm \neg q\ \vM$\bv
$\gna\snp (G)$\bv
$\perp$\bi $1$ \wrt $\SP_1$
\etab
\enit%end At
\itc %imm\tensor
$$\IP= \ibnc{\ga\sp D_{1}\imm Q}{\ga\sp D_{2}\imm Q}{\ga\sp (D_{1}\tensor
  D_{2})\imm Q}{\imm\tensor}$$
and $\IM$ ends in $\gna\sn\mnotd (D_{1}\tensor
  D_{2})\imm \neg Q$:
\btab
 $\ga\spp  D_1\imm Q$ \bs
$\ga\spp  D_2\imm Q$\bs
$\gna\sn \mnotd (D_1)\And\mnotd (D_2)\imm\neg Q$\br $\mnotd\tensor$
\etab
\bit
\item[\subcase]
\btab
$\gna\sn \mnotd (D_1)\imm\neg Q$\bv
$\perp$\bi $2.1$
\etab
\item[\subcase]
\btab
$\gna\sn \mnotd (D_2)\imm\neg Q$\bv
$\perp$\bi $2.1$
\etab
\enit
\itc%And 1
$$\IP= \ianc{\ga\sp D_{1}\imm Q}{\ga\sp (D_{1}\And
  D_{2})\imm Q}{\imm\And}$$
and $\IM$ ends in $\gna\sn\mnotd (D_{1}\And
  D_{2})\imm \neg Q$:
\btab
 $\ga\spp  D_1\imm Q$ \bs
$\gna\sn \mnotd (D_1)\tensor\mnotd(D_2)\imm\neg Q$\br $\mnotd\And$\\
$\gna\sn\mnotd(D_1)$\bv
$\perp$\bi $2.1$
\etab
\itc%And 2
$$\IP= \ianc{\ga\sp D_{2}\imm Q}{\ga\sp (D_{1}\And
  D_{2})\imm Q}{\imm\And}$$
and $\IM$ ends in $\gna\sn\mnotd (D_{1}\And
  D_{2})\imm \neg Q$:
\btab
 $\ga\spp  D_2\imm Q$ \bv
$\gna\sn \mnotd (D_1)\tensor\mnotd(D_2)\imm\neg Q$\br $\mnotd\And$\\
$\gna\sn \mnotd (D_2)\imm\neg Q$\bv
$\perp$\bi $2.1$
\etab
\itc %\Pi imm
$$\IP= \ibnc{\GG\vd t\hastype A}{ \ga\spp [t/x] D \imm Q}{\ga\spp\PI
 { x}{A}D \imm Q}{\imm\Pi}$$
and $\IM$ ends in $\gna\sn\mnotd(\PI{x}{A}D)\imm\neg Q$:
\btab
$\ga\spp [t/x] D\imm Q$\bs
$\gna\sn\PIXA\mnotd(D)\imm\neg Q$\br $\mnotd\Pi$\\
$\gna\sn [t/x]\mnotd(D)\imm\neg Q$\bv
$\perp$\bi $2.1$
\etab
\enit
\item[\fbox{2.2}] %second case
  Let $D\in \defp(q,\PP)$ and $D'\in  \defp(\neg q,\cD)$. It is not the case that
$\IP :: \ga\spp  D \imm Q$ and
$\IM :: \gna\sn\imm D'\neg Q$.
\bit
\itc
$$\IP=\ianc{}{\ga\spp\perp\imm  Q}{\imm \atm}$$
But there can be no proof of $\neg Q$ from  $\mnota(\perp)=\top$.
\itc
$$\IP=\ibnc{\ga\spp\vS\eqd \vM}{\ga\spp G}{\ga\spp (q\ \vS\If G)\imm q\ \vM}{\imm\Imp}$$
and
$\IM$ ends in $\gna\sn \mnota (q\ \vnx\If H)\imm \neg q\
\vM$, where $q\ \vnx\If H \in \defp(q,\cD)$.
\btab
$\ga\spp\vS\eqd \vM$\bs
$\ga\spp S_i\eqd M_i$ for some  $1\leq i\leq n$ $ (*)$\bs
%$\ga\spp G$\bs
$\gna\sn \BAnd_{x\in dom(\GG)}\BAnd_{\xrq}\mnotxi (q\ \vnx )\And (\neg q\ \vnx\If\mnotg(H)) \imm \neg
q\ \vM$
\` By  rule $\mnota\Imp$
\etab
\bit
\item[\subcase]
\btab
$\gna\sn \BAnd_{x\in dom(\GG)}\BAnd_{\xrq}\mnotxi (q\ \vnx) \imm\neg q
\ \vM$\bv
$\gna\sn \BAnd_{\xrq}\mnotxi (q\ \vnx) \imm\neg q \ \vM$\bv
$\gna\sn \mnotxi (q\ \vnx )\imm \neg q\ \vM$\bv
$\gna\sn \BAnd_{1\leq j\leq n,j\not = i}(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}
      \neg q\ \ol{Z^i_x}\If N_j\neqd Z_j)\imm\neg  q\ \vM$
\br $\mnotxi\Imp$\\
$\gna\sn \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}
      \neg q\ \ol{Z^i_{\ex}}\If N_j\neqd Z_j\imm\neg  q\ \vM$\` By inversion\\
$\ga\sn [\s] \ol{Z^i_{\ex}}\eqd\Mn$\` By inversion and $x\not\in dom(\s)$\\
$\ga\sn \ex\eqd M_i$\bv
%$\ga\sn[M_j/Z_j]Z_j\eqd M_j\And x\eqd M_i$
$\perp$\` From  line $(*)$ and  constructor restriction on $S_i$
\etab
\item[\subcase]
\btab
$\gna\sn \neg q\ \vnx\If\mnotg(H) \imm \neg q\ \vM$\bv
$\gna\sn\vnx\eqd \vM$\bv
$\ga\sn \ex\eqd M_i$\bv
%$\ga\sn[M_j/Z_j]Z_j\eqd M_j\And x\eqd M_i$
$\perp$\` From  line $(*)$ and  constructor restriction on $S_i$
\etab
\enit
%\itc $\IP$ ends in $\imm\tensor,\imm\And,\imm\Pi$: by IH as
%in $2.1$.

\itc %imm\tensor
$$\IP= \ibnc{\ga\sp D_{1}\imm Q}{\ga\sp D_{2}\imm Q}{\ga\sp (D_{1}\tensor
  D_{2})\imm Q}{\imm\tensor}$$
and $\IM$ ends in $\gna\sn\mnota (D'_{1}\tensor  D'_{2})\imm \neg Q$:
\btab
 $\ga\spp  D_1\imm Q$ \bs
$\ga\spp  D_2\imm Q$\bs
$\gna\sn \mnota (D'_1)\And\mnota (D'_2)\imm\neg Q$\br $\mnota\tensor$
\etab
\bit
\item[\subcase]
\btab
$\gna\sn \mnota (D'_1)\imm\neg Q$\bv
$\perp$\bi $2.2$
\etab
\item[\subcase]
\btab
$\gna\sn \mnota (D'_2)\imm\neg Q$\bv
$\perp$\bi $2.2$
\etab
\enit
\itc%And 1
$$\IP= \ianc{\ga\sp D_{1}\imm Q}{\ga\sp (D_{1}\And
  D_{2})\imm Q}{\imm\And}$$
and $\IM$ ends in $\gna\sn\mnota (D'_{1}\And
  D'_{2})\imm \neg Q$:
\btab
 $\ga\spp  D_1\imm Q$ \bs
$\gna\sn \mnota (D'_1)\tensor\mnota(D'_2)\imm\neg Q$\br $\mnota\And$\\
$\gna\sn\mnota(D'_1)$\bv
$\perp$\bi $2.2$
\etab
\itc%And 2
$$\IP= \ianc{\ga\sp D_{2}\imm Q}{\ga\sp (D_{1}\And
  D_{2})\imm Q}{\imm\And}$$
and $\IM$ ends in $\gna\sn\mnota (D'_{1}\And
  D'_{2})\imm \neg Q$:
\btab
 $\ga\spp  D_2\imm Q$ \bv
$\gna\sn \mnota (D'_1)\tensor\mnota(D'_2)\imm\neg Q$\br $\mnota\And$\\
$\gna\sn \mnota (D'_2)\imm\neg Q$\bv
$\perp$\bi $2.2$
\etab
\itc %\Pi imm
$$\IP= \ibnc{\GG\vd t\hastype A}{ \ga\spp [t/x] D_1 \imm Q}{\ga\spp \PI
 { x}{a}D_1 \imm Q}{\imm\Pi}$$
and $\IM$ ends in $\gna\sn\mnota(\PI{x}{a}D')\imm\neg Q$:
\btab
$\ga\spp [t/x] D_1\imm Q$\bs
$\gna\sn\PIXA\mnota(D')\imm\neg Q$\br $\mnota\Pi$\\
$\gna\sn [t/x]\mnota(D')\imm\neg Q$\bv
$\perp$\bi $2.2$
\etab

%%%%%%%%%%
\enit
\item[\fbox{2.3}] %third case
  Let $D\in \defp(q,\cD)$ and $D'\in \defp(\neg q,\cP)$.  It is not
  the case that $\IP :: \ga\spp D \imm Q$ and $\IM :: \gna\sn D'\imm
  \neg Q$.
\bit
\itc
$$\IP=\ibnc{\ga\sp\vnx\eqd\Mn}{\ga\sp H}{\ga\sp q\ \vnx\If H \imm q\
  \vM}{\imm\Imp}$$
and $\IM$ ends in $\gna\sn\mnotd (q\ \vS\If G)\imm\neg q \ \Mn$.
\btab 
$\ga\sp\vnx\eqd\Mn$\bs
$\ga\sp \ex\eqd M_i$ $(*)$ for some $1\leq i\leq n$\bs
$\gna\sn \BAnd_{\vT\in\mnot(\vS)}\Pi( \neg q\ \vT\If \top )\And
(\neg q\ \vS\If \mnotg(G))\imm\neg q\
      \Mn$\` By rule $\mnotd\Imp$
\etab
\bit
\item[\subcase]
\btab
$\gna\sn \BAnd_{\vT\in\mnot(\vS)}\Pi( \neg q\ \vT\If\top )\imm q\ \Mn$
\bv
$\gna\sn \Pi( \neg q\ \vT\If\top )\imm q\ \Mn$ for some $\vS$ \bv
$\gna\sn[\s](\neg q\ \vT)\If \top \imm \neg q\ \Mn$   for some $\sigma$\bv
$\gna\sn[\s]\vT\eqd\Mn$\bv
$\gna\sn [\s] T_i\eqd M_i$\bv
$\perp$\` Above line, $(*)$ and eigenvariable condition
\etab
\item[\subcase]
\btab
$\gna\sn\neg q\ \vS\If \mnotg(G)\imm\neg q\ \Mn$ \bv
$\gna\sn\vS\eqd\Mn$\bv
$\gna\sn S_i\eqd M_i$\bv
$\perp$\` From  line $(*)$ and  constructor restriction on $S_i$
\etab
\enit
\itc $\IP$ ends in $\imm\tensor,\imm\And\imm\Pi$: symmetric to case $2.2$.
\enit
\item[\fbox{2.4}] %\fourth case
  Let $D\in \defp(q,\cD)$ and $D'\in \defp(\neg q,\cD)$.  It is not
  the case that $\IP :: \ga\spp D \imm Q$ and $\IM :: \gna\sn D' \imm
  \neg Q$.
\bit
\itc
$$\IP=\ibnc{\ga\sp\vnx\eqd\Mn}{\ga\sp G}{\ga\sp q\ \vnx\If G \imm q\
  \vM}{\imm\Imp}$$
and $\IM$ ends in $\gna\sn\mnota (q\ \vnx\If G)\imm\neg q \
\Mn$.
\btab
$\SP_1::\ga\sp G$\bs
$\ga\sp\vnx\eqd\Mn$\bs
$\ga\sp N_j\eqd M_j$ $(+)$ for some  $1\leq i,j\leq n, i\not= j$\bv
$\gna\sn\BAnd_{x\in dom(\GG)}\BAnd_{\xrq}\mnotxi (q\
\vnx)\And(\neg q\ \vnx)\If\mnotg(G))\imm\neg q \ \Mn$\` By rule $\mnota\Imp$
\etab
\bit
\item[\subcase]
\btab
$\gna\sn\BAnd_{x\in dom(\GG)}\BAnd_{\xrq}\mnotxi (q\
\vnx)\imm\neg q \ \Mn$\bv
$\gna\sn\BAnd_{\xrq}\mnotxi (q\vnx)\imm\neg q \ \Mn$\bv
$\gna\sn\mnotxi (q\ \ol{N_{\ex}^i})\imm\neg q \ \Mn$\bv
%$\gna\sn\mnotxi (q\ \ol{N^x_i})\imm\neg q \ \Mn$\` By rule $\mnota\Imp$\\
$\gna\sn \BAnd_{1\leq j\leq n,j\not = i}(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}
      \neg q\ \ol{Z^i_{\ex}}\If Z_j\neqd N_j)\imm\neg  q\ \vM$\bv
$\gna\sn (\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ \ol{Z^i_{\ex}}\If
      Z_j\neqd N_j)\imm\neg  q\ \vM$\bv 
$\ga\sn[M_j/Z_j]Z_j\neqd N_j$\bv
$\perp$\` Above line and $(+)$
\etab
\item[\subcase]
\btab
$\gna\sn\neg q\ \vnx\If\mnotg(G)\imm\neg q \ \Mn$\bv
$\gna\sn\mnotg(G)$\bv
$\perp$\bi $1$ on $\SP_1$
\etab
\enit
\itc $\IP$ ends in $\imm\tensor,\imm\And,\imm\Pi$: by IH as in case
$2.1$ with $\mnota$ in place of $\mnotd$.
\enit
\enen
 %end four cases
 %start \vd G
\bit
\itc
$$\SP=\ianc{ \ga\spp  \defp(q,\PP\And\cD)\imm Q}{\ga\spp Q}{ \vd  {\rm atm}}$$
and $\SM$ ends in $\gna\snp (Q)$:
\btab
$\ga\spp  \defp(q,\PP\And\cD)\imm Q$\bs
$\ga\spp D\imm Q$ for $D\in  \defp(q,\PP\And\cD)$\bs
$\gna\sn\neg Q$\br $\mnotg\atm$\\
$\gna\sn \defp(\neg q,\cP\cD)\imm \neg Q$\bv
$\ga\sn D'\imm \neg Q$ for $D'\in  \defp(\neg q,\PP\And\cD)$\bv
$\perp$\bi $2$
\etab
%And
\itc
$$\SP=\ibnc{\ga\spp G_1}{\ga\spp G_{2}}{\ga\spp G_{1}\And G_{2}}
{ \vd\And}$$
and $\SM$ ends in $\gna\snp (G_1\And G_2)$
\btab
 $\ga\spp G_1$\bs
 $\ga\spp G_2$\bs
 $\gna\sn\mnotg(G_1)\Or\mnotg(G_2)$\br $\mnotg\And$
\etab
\bit
\item[\subcase]
\btab
$\gna\snp(G_1)$\bv
$\perp$\bi $1$
\etab
\item[\subcase]
\btab
$\gna\snp(G_2)$\bv
$\perp$\bi $1$
\etab
\enit
%Or 1
\itc
$$\SP=\ianc{\ga\spp G_1}{\ga\spp G_{1}\Or G_{2}}
{ \vd\Or}$$
and $\SM$ ends in $\gna\snp (G_1\Or G_2)$
\btab
 $\ga\spp G_1$\bs
$\gna\sn\mnotg(G_1)\And\mnotg(G_2)$\br $\mnotg\Or$\\
 $\gna\snp (G_1)$\bv
 $\gna\snp (G_2)$\bv
$\perp$\bi $1$
\etab
%Or 2
\itc
$$\SP=\ianc{\ga\spp G_2}{\ga\spp G_{1}\Or G_{2}}
{ \vd\Or}$$
and $\SM$ ends in $\gna\snp (G_1\Or G_2)$. Symmetrical.
% \btab
%  $\ga\spp G_2$\bv
% $\gna\sn\mnotg(G_1)\And\mnotg(G_2)$\bv
%  $\gna\snp (G_1)$\bv
%  $\gna\snp (G_2)$\bv
% $\perp$\bi $1$
% \etab
\itc %\PI
$$\SP=\ianc{(\GG,y\oftp A);\cD\sp[y/x]G'}{\ga\sp \Pixa G'}{{\prv}
  \Pi^*}$$
and $\SM$ ends in $\gna\sp\mnotg(\Pixa G')$:
\btab
$(\GG,y\oftp A);\cD\sp[y/x]G'$\bs
$\gna\sp\Pixa\mnotg(G')$\br $\mnotg\Pi$\\
$(\GG,y\oftp A);\cD\sn[y/x]\mnotg(G')$\bv
$\perp$\bi $1$
\etab
\itc %\Imp
$$\SP= \ianc{\GG;(\cD\And D') \sp G'}{\ga\sp D' \Imp G'}{{\prv} \Imp}$$
and $\SM$ ends in $\gna\sp\mnotg(D'\Imp G')$:
\btab
$\GG;(\cD\And D') \sp G'$\bs
$\gna\sn D'\Imp \mnotg(G')$\br $\mnotg\Imp$\\
$\GG;(\cD\And D') \sp \mnotg(G')$\bv
$\perp$\bi $1$
\etab
\itc The (dis)equality case follows from the decidability of the (dis)equality
 judgment.
\enit% main bit
\end{proof}

Note that the proof goes through as there is no `bad' interaction
between the static and dynamic definition of a predicate; namely in
sub-case $2.2$ there is no overlap between a clause from $\defp(q,\PP)$
and $\defp(\neg q,\cD)$ since in every atomic assumption there must be an
occurrence of a new parameter \emph{and} every term at the same
position in a program clause
head must start with a constructor . Symmetrically for $2.3$. Sub-case $2.4$
holds 
% either because atoms in $\defp(q,\PP)$ and $\defp(\neg q,\cD)$ have a
% different pivot parameter or, if it the same, an appropriate
% disequation is inferred. 
because an appropriate disequation is inferred; this approximates what
happens in the first case $2.1$, which is based on term exclusivity
(Corollary \ref{le:part}). In the latter case, it suffices to
consider, for $D\in \defp(q,\cP)$, only $\ga\spp D\imm Q$ and
$\ga\sn\mnotd(D)\imm\neg Q$, because the positive definition is a
conjunction, while the negative one is a disjunction; the same remark
applies when the definition is dynamic ($2.4$).

The condition for programs to require clause heads with rigid terms
%and assumptions with parameters only in head position 
may seem too restrictive and we thus comment on it. As we remarked
earlier, it applies only to non-Horn predicate definitions; secondly,
only one of those terms which occur in the same position of a
parameter in each assumptions needs to be rigid; more formally, if $q\ 
\Mn\If G\yg\cS$ is a HHF formula yielding a schema $\cS$ and say $q\ 
N^i_{\ex}$ is in $\cS$ for \emph{some} $1\leq i\leq n$, then only
$M_i$ must be rigid. Thus, any HHF program which uses a `catch-all'
clause is those positions is forbidden; nevertheless it is easy to
avoid catch-all clauses via explicit coercion or partial evaluation.
Finally, we remark that any other (decidable) condition which avoids
overlap between static and dynamic clauses will do; the one we have
proposed is statically checkable, certainly not `ad hoc' and has been
dictated by the practice of logical frameworks.






