\chapter{The Relative Complement Problem for Higher-Order Patterns}
\label{cap:relcomp}

\section{Towards Complementation}
\label{sec:strictcomp}


Now that we have developed a calculus which is potentially strong
enough to represent the negation of linear patterns, we need to
answer two questions: how do we embed the original $\lambda$-calculus,
and is the calculus now closed under complement?

We require that our complement operator satisfies the usual boolean 
rules for negation, that is:
\ben
\item (Disjointness) It is not the case that $M$ is both a ground 
instance of $N$  and of $\mmnot(N)$.
\item (Exhaustivity) $M$ is a ground instance of $N$ or $M$ is a 
ground instance of $\mmnot(N)$.
\enen


Unfortunately, while the first property follows quite easily from 
Corollary \ref{co:disj}, it turns out that the exhaustivity does not hold in 
general as we allow logic variables in partially applied terms. 
 However, our algorithm is sound and
complete for the fragment which results from the natural embedding of the
original simply-typed $\lambda$-calculus which is sufficient for all
applications we have presently considered (see Section
\ref{sec:concl}).

%must therefore isolate the right fragment of the strict calculus: 
This entails two separate phases:
\bit
\item restrict to a class of terms (that we call \emph{simple}) for
which exhaustivity can be established.
\item
bring to full application those terms.
\enit

%Note that the first item is not required for disjointness.


\subsection{Simple Terms}

% We now address the issue of exhaustivity: once we have allowed 
% existential variables,  we would like  the 
% following to hold:
% \[ \GG\vd M \in \|E\ z^{1}\|  \mbox{\textrm{ or }}  \GG\vd M \in \|\mmnot (E\ 
% z^{1})\|\]
% \ie
% \[ \GG\vd M \in \|E\ z^{1}\|  \mbox{\textrm{ or }}  \GG\vd M \in \|F\ 
% z^{0}\|\]

Recall that we introduced strictness to capture occurrence conditions on
variables in canonical forms.  This means that constants (and by extension
bound variables) should be considered \emph{strict} functions of their
argument, since these arguments will indeed occur in the canonical form.  On
the other hand, if we have a second order constant, we cannot restrict the
argument function to be either strict or vacuous, since this would render
our representations inadequate.


\begin{example}
\label{ex:excont}
 Continuing Example \ref{ex:lam}, we see
\[
\begin{array}{rcl}
\rep{\lambda x.\, \lambda y.\, x} = lam\ (\lamb{x}{exp} lam\ (\lamb{y}{exp} x))
\end{array}
\]
 so the argument to the first occurrence of\ $lam$ is a strict function,
while the argument to the second occurrence is an invariant function.
If we can give only one type to $lam$ is must therefore be
$(exp \GImp{u} exp) \GImp{1} exp$.
\end{example}

Generalizing this observation means that positive occurrence of function
types are translated to strict functions, while negative occurrences to
undetermined functions.  We can formalize this as an embedding of the
simply-typed $\l$-terms into a fragment of strict terms via two mutually
recursive functions $()^{-}$ and $()^{+}$.  First, the definition on
types.
\beq
(A\Imp B)^{-} & = & A^{+} \TImp B^{-}\\
(A\Imp B)^{+} & = & A^{-} \RImp B^{+}\\
P^{-} = P^{+} & = & P
\eneq
We extend it to canonical terms (including existential variables), signatures,
and contexts as follows:
\beq
(\lxa M)^{-} & = & \lamb{x^{u}}{A^{+}} M^{-}\\
M^{-} & = & M^{+} \qquad \mbox{for $M$ of base type}\\
x^{+} & = & x\\
c^{+} & = & c\\
(E_A\ x_1\dots x_n)^{+} &=& F_{A^{-}} \ x_1^u\dots x^u_n \\
(M\ N)^{+} & = & M^{+}\ (N^{-})^{1}\\
[1em]
(\cdot)^{+} & = & \cdot\\
(\GG,x\oftp A)^{+} & = & \GG^{+}, x\oftp A^{+}\\
(\Sigma,P\oftp type)^{+} & = & \Sigma^{+}, P\oftp type\\
(\Sigma,c\oftp A)^{+} & = & \Sigma^{+}, c\oftp A^{+}
\eneq

% But consider the following:
% \begin{example}
% \[
% \begin{array}{l}
% y\oftp ((a\Imp a)\Imp a)\Imp a, x\oftp a\vd y(\lamb{f}{a\Imp a} f\ 
% x) \\
% y\oftp ((a\Imp a)\Imp a)\Imp a, x\oftp a\vd y(\lamb{f}{a\Imp a} x)
% \end{array}
% \]
% Note that $y$ is well-typed but the above term does not satisfy exhaustivity. 
% \end{example}

% The idea is then to make the status of terms as determined as 
% possible, while preserving the possibility of well-typing sub-terms 
% as $y$ above.  The trick is to keep undetermined every negative 
% occurrence of the arrow, while making determined the positive ones.

% \smallskip
% We now formalize this an  embedding of the simply-typed $\l$-terms 
% into a fragment of strict terms. This is accomplished through the two mutually recursive 
% functions $\_^{-}$ and $\_^+$:
% \beq
% (A\Imp B)^{-} & = & A^{+} \TImp B^{-}\\
% (A\Imp B)^{+} & = & A^{-} \RImp B^{+}\\
% P^{\pm} & = & P
% \eneq
% We then extend it to terms (including logic variables), 
% signatures and contexts as follows:
% \beq
% (\lxa M)^{-} & = & \lamb{x^{u}}{A^{+}} M^{-}\\
% M^{-} & = & M^{+}\\
% x^{+} & = & x\\
% c^{+} & = & c\\
% (E_A\ \xn)^{+} &=& F_{A^{-}} \ \xn^u\\
% (M\ N)^{+} & = & (M^{+}\ N^{-})^{1}\\
% [1em]
% (\cdot)^{+} & = & \cdot\\
% (\GG,x\oftp A)^{+} & = & \GG^{+}, x\oftp A^{+}\\
% (\Sigma,P\oftp type)^{+} & = & \Sigma^{+}, P\oftp type\\
% (\Sigma,c\oftp A)^{+} & = & \Sigma^{+}, c\oftp A^{+}
% \eneq

% The example before is translated as follows:
% %  \begin{example}
% \beq
% \lefteqn{(y\oftp ((a\Imp a)\Imp a)\Imp a, x\oftp a)^{+}\vd (y(\lamb{f}{a\Imp a} f\ 
% x))^{+}  = }\\
% & & y\oftp ((a\RImp a)\TImp a)\RImp a, x\oftp a\emp\vd y(\lamb{f^{u}}{a\RImp a} f\ 
% x^{1})^{1}\\
% \lefteqn{(y\oftp (a\Imp a)\Imp a, x\oftp a)^{+}\vd (y(\lamb{f}{a\Imp a} x))^{+}  = }\\
% & & y\oftp ((a\RImp a)\TImp a)\RImp a, x\oftp a\emp\vd y(\lamb{f^{u}}{a\RImp a} x)^{1}
% \eneq
% % \end{example}
\begin{example} Continuing Example
 \ref{ex:excont}
\beq
 (lam\ (\lamb{x}{exp} lam\ (\lamb{y}{exp} x)))^+& = & 
 lam\ (\lamb{x^u}{exp} lam\ (\lamb{y^u}{exp} x)^1)^1
\eneq
\end{example}

The image of the embedding of the canonical forms of the simply-typed 
$\lambda$-calculus gives rise to the following fragment, which we 
call:

\[ \begin{array}{rrcl}
\mbox{\textit{Simple Terms}} & M & \bnfas &  \lam x^{u}\oftp
A^{+}\ldot M \bnfalt (\dots (h\ M_1)^{1} \dots M_n)^{1} \bnfalt 
 E_{A^{-}}\ x^u_{1}\dots x^u_{n}
\end{array} \]
We sometimes abridge $(\dots (h\ M_1)^{1} \dots M_n)^{1}$ in $h\ 
\Mns$. Note that by the restriction to long normal
forms such terms and applications of pattern variables must be of base type.
 Moreover, for every judgment $\cal J$ on simple terms,
 we will shorten  $\GG\emp\vd \cal J$ into $\GG\vd \cal J$.
\smallskip

To prove the correctness of the embedding, we will need the following:

\newcommand{\ctx}{\GG^{+}}

\begin{Lemma}
\label{le:aminus}
If $\GG\vd E_{A}\ \xn \hastype P$, then $\ctx\vd F_{A^{-}}\ 
\ol{x^u_n}\hastype P$.
\end{Lemma}
\begin{proof}
A straightforward induction on $A$.
\end{proof}

The following theorem requires the usual inductive 
definition of canonical terms in the simply-typed $\l$-calculus,
which can be obtained via Theorem \ref{thm:conserv}.

\begin{Theorem}[Correctness of $()^{\pm}$]
\label{thm:embed}
\mbox{}
\ben
\item
If $\GG\vd M\bua A$ then $\ctx\vd M^{-}\bua A^{-}$. 
\item
If $\GG\vd M\da A$ then $\ctx\vd M^{+}\da A^{+}$. 
\enen
\end{Theorem}
\begin{proof}
By mutual induction on the proofs of $\cD::\GG\vd M\bua A$ and 
$\cD'::\GG\vd M\da A$.
\bit
\itc 
\[\cD'= \ianc{c\oftp A\in\Sigma}{\GG\vd c\da A}{atm\_var}\]
Since $c^{+}= c$ and $\Sigma^{+}(c) = A^{+}$ we conclude
$$\ianc{}{\ctx\vd c^{+}\da A^{+}}{cIdc}$$
\itc 
\[\cD'= \ianc{}{(\GG,x\oftp A)\vd x\da A}{atm\_var}\]
Since $x^{+}= x$ and $\GG^{+}(x) = A^{+}$ we conclude
$$\ianc{}{(\GG^{+},x\oftp A^{+})\emp\vd x^{+}\da A^{+}}{cId^{u}}$$
\itc
\[\cD'=\ibnc{\GG\vd M\da B\Imp A}{\GG\vd N\bua B}{\GG\vd M\ N \da 
A}{atm\_app}\]
\btab
$\GG\vd M\da B\Imp A$\bv
$\ctx\vd M^{+}\da (B\Imp A) ^{+}$\bi\\
$\ctx\vd M^{+}\da B^{-}\RImp A ^{+}$\` By the embedding\\
$\GG\vd N\bua B$\bv
 $\ctx\vd N^{-}\bua B^{-}$\bi\\
$\ctx\vd (M^{+}N^{-})^{1}\da A^{+}$\br\\
$\ctx\vd ((M\ N)^{+} )^{1}\da A^{+}$ \` By the embedding
\etab
\itc
\[\cD'=
\ianc{\GG\vd E_{A}\ \xn\hastype P}{\GG\vd E_{A}\ \xn\da 
P}{can\_Pat}\]
\btab
$\GG\vd E_{A}\ \xn\hastype P$\bv
$\ctx\vd F_{A^{-}}\ \ol{x^u_n}\hastype P$
\`   By Lemma \ref{le:aminus} \\
$\ctx\vd F_{A^{-}}\ \ol{x^u_n}\da P$ \br\\
$\ctx\vd (E_{A}\ \xn)^{+}\hastype P^{+}$\`  By the embedding
\etab
\itc
\[\cD=\ianc{\GG\vd M\da P}{\GG\vd M\bua P}{can\_atm}\] 
\btab
$\GG\vd M\da P$\bv
$\ctx\vd M^{+}\da P^{+}$\bi\\
$\ctx\vd M^{+}\bua P^{+}$\br\\
 $\ctx\vd M^{-}\bua P^{-}$\`   By the embedding
\etab
 \itc
\[\cD= \ianc{\GG,x\oftp A\vd M\bua B}{\GG\vd\lxa M\bua A\Imp 
B}{can\_lam}\] 
\btab
$\GG,x\oftp A\vd M\bua B$\bv
$(\GG^{+},x\oftp A^{+})\emp\vd M^{-}\bua B^{-}$\bi\\
$\ctx\vd\lamb{x^{u}}{A^+} M \bua A^{+}\TImp B^{-}$ \br\\
$\ctx\vd (\lxa M)^{-}\bua (A \Imp B)^{-}$\` By the embedding
\etab
\enit\end{proof}

From now on we drop the $()^{\pm}$ embedding annotations from terms, 
types and contexts. We may also hide the $()^1$ decoration
from strict application of constants in examples.

\smallskip
We can now prove the crucial tightening lemma.
 It expresses
that every  \emph{closed simple term} is either strict or vacuous in a given
undetermined variable.

\newcommand{\cu}{(\GG, x\oftp C);\Omega;\Delta}
\newcommand{\cxtr}{\GG;\O; (\D, x\oftp C)}
\newcommand{\cxto}{\GG; (\O,x\oftp C);\D}

\begin{Lemma}[Tightening]
\label{le:exh} 
Let $M$ be a simple pattern  without existential variables such that $\cu\vd M\buda A$. Then:
\ben
\item
 $\cxtr\vd M\da A$ or $\cxto\vd M\da A$.
\item
 $\cxtr\vd M\bua A$ or $\cxto\vd M\bua A$.
\enen
\end{Lemma}
\begin{proof}
By mutual induction on $\cD_{1}::\cu\vd M\da A$ and 
$\cD_{2}::\cu\vd M\bua A$.
\bit
\itc 
$$\cD = \ianc{c\oftp A\in\Sigma}{(\GG,x\oftp C);\O;\cdot \prv  c\da A}{cIdc}$$
Then
$$\cE= \ianc{c\oftp A\in\Sigma}{\GG;(\O,x\oftp C);\cdot \prv  c\da A}{cIdc}$$
and by weakening the thesis.
\itc
$$\cD = \ianc{}{(\GG,x\oftp C,y\oftp A);\O; \cdot  \prv  y\da 
A}{cId^{u}}$$
Then 
$$\cE = \ianc{}{(\GG,y\oftp A);(\O,x\oftp C); \cdot  \prv  y\da 
A}{cId^{u}}$$
and by weakening the thesis.
\itc
$$\cD = \ianc{}{(\GG,x\oftp C);\O;\cdot \prv  x\da C}{cId^{u}}$$
Then
$$\cE= \ianc{}{\GG;\O;x\oftp C \prv  x\da C}{cId^{1}}$$
and by weakening the thesis.
\itc 
$$\cD= \ianc{}{(\GG,x\oftp C);\O;y\oftp A\vd y\da A}{Id^{1}}$$
Then $$\cE= \ianc{}{\GG;(\O,x\oftp C);y\oftp A\vd y\da A}{Id^{1}}$$
and by weakening the thesis.
% \itc
% $$\cD=
% \ianc{\cu\vd E_{A}\ \xnl \hastype P}{\cu \vd E_{A}\ \xnl \da  
% P}{cPat}$$
% \btab
% $\cu\vd E_{A}\ \xnl \hastype P$\bv
% $\cdot;\cdot;\cdot\vd E_{A}\hastype A$\bv
% $\cxto\vd E_{A}\ \xnl \hastype P$\br\\
% $\cxto\vd E_{A}\ \xnl \da P$\br\\
% hence by weakening the thesis.
% \etab
 
\itc
$$\cD = \ianc{\cu\prv  M\da P}{\cu \prv  M\bua P} {cAt}$$
\btab
$\cu\prv  M\da P$ \` By inversion\\ 
$\cxtr \prv  M\da P$  \` By the left horn of the IH\\
$\cxtr \prv  M\bua P$ \` By rule $cAt$\\
$\cxtr \prv  M\bua P$ or $\cxto \prv  M\bua P$ \` By weakening\\
$\cxto \prv  M\da P$ \`  By the right horn of the IH \\
$\cxto \prv  M\bua P$ \` By rule $cAt$\\
$\cxtr \prv  M\bua P$ or $\cxto \prv  M\bua P$ \` By weakening
\etab
\itc
$$\cD = \ianc{(\GG,x\oftp C,y\oftp A);\Omega;\Delta \prv M\bua B}{\cu\prv(\lamb{y^u}{A} M) \bua 
A\TImp B} {c\TImp I}$$
\btab
$(\GG,x\oftp C,y\oftp A);\Omega;\Delta \prv M\bua B$ \` By inversion\\
$(\GG,y\oftp A);\Omega;(\Delta,x\oftp C)\vd M\bua $ \` By the left horn of the IH\\
$\cxtr\prv(\lamb{y^u}{A} M) \bua A\TImp B$ \` By rule $c\TImp I$\\
$\cxtr\prv(\lamb{y^u}{A} M) \bua A\TImp B$ or $\cxto\prv(\lamb{y^u}{A} M) 
\bua A\TImp B$\\
 \` By weakening\\
$(\GG,y\oftp A);(\O,x\oftp C);\Delta\vd M\bua $ \` By the right horn of the IH\\
$\cxtr\prv(\lamb{y^u}{A} M) \bua A\TImp B$ or $\cxto\prv(\lamb{y^u}{A} M) 
\bua A\TImp B$\\
 \` Similarly
\etab

\itc
 $$\cD = \ibnc{(\GG,x\oftp C,\D_N);\O;\D_M \vd M \da A \RImp 
B}{(\GG,x\oftp C,\D_M);\O;\D_N \vd N \bua A}{(\GG,x\oftp C);\O;\dmn 
\vd M\ N^1 \da B}{c\RImp E}$$
There are four  sub-cases, stemming from the IH:
\ben
\item
\btab
$(\GG,\D_N);\O;(\D_M,x\oftp C)\vd M\da A\RImp B$
\` By  IH\\
$(\GG\D_{M});\O;(x\oftp C,\D_N)\vd N\bua A$
\` By  IH\\
$(\GG,\D_M,x\oftp C);\O;\D_N\vd N\bua A$ 
\` By Loosening$^{1}$\\
$\GG;\O;(\D_M,x\oftp C,\D_N)\vd M\ N^{1}\da B$
\` By rule\\
 hence  by weakening the thesis.
 \etab

\item 
\btab
$(\GG,\D_N);(\O,x\oftp C);\D_M\vd M\da A\RImp B$ \` By  IH\\
$(\GG,\D_M);(\O,x\oftp C);\D_N\vd N\bua A$ \` By IH\\
$\GG;(\O,x\oftp C);\dmn\vd M\ N^{1}\da B$ \` By rule\\
 hence  by weakening the thesis.
\etab
\item
\btab
$(\GG,\D_N);\O;(\D_M,x\oftp C)\vd M\da A\RImp B$
\` By IH\\
$(\GG,\D_M);(\O,x\oftp C);\D_N\vd N\bua A$ 
\` By IH\\
$(\GG,x\oftp C);\O;(\D_M\vd N\bua A$ 
\` By Loosening$^{0}$\\
$\GG;\O;(\D_M,x\oftp C,\D_N)\vd M\ N^{1}\da B$
\` By rule\\
hence  by weakening the thesis.
\etab
\item Symmetrical to $3.$
%
\enen
\enit
\end{proof}

% \begin{Corollary}
% \label{co:exh} 
% If $(\GG,\O,\D)\emp\vd M\hastype C$, then either $\god\vd M\hastype C$ 
% or there is $x\oftp A$ such that $(\GG,\O,\D)- x\oftp A;\cdot;x\oftp 
% A;\vd M\hastype C$ or $(\GG,\O,\D)- x\oftp A;\cdot;x\oftp A 
% \vd M\hastype C$.
% \end{Corollary}
\begin{Corollary}
\label{co:exh} 
Let $(\GG,\O,\D,x\oftp C)\emp\vd M\hastype A$; then
\ben
\item
either $\GG;(\O,x\oftp C);\D\vd M\hastype A$ or 
$(\GG,\O,\D);\cdot;x\oftp C;\vd M\hastype A$.
\item 
either $\GG;\O;(\D,x\oftp C)\vd M\hastype A$ or $(\GG,\O,\D);\cdot;x\oftp C 
\vd M\hastype A$.
\enen\end{Corollary}
\begin{proof}
By repeated application of Lemma \ref{le:exh},
Loosening$^{0}$ and Loosening$^{1}$.
\end{proof}


\subsection{Full Application}
\newcommand{\LBimp}{\longleftrightarrow}

It simplifies the presentation of the algorithms for complement and
later unification if we extend every term to be applied to all bound
variables in their declaration order.  This is possible for simple
linear patterns without changing the set of its ground instances.  We
just insert vacuous applications, which guarantees that the extra
variables are not used.  We furthermore permute the argument to the
standard order, which also does not affect the set of ground instances
of linear patterns.  In slight abuse of notation we call the resulting
terms \emph{fully applied}.

We describe in Fig.\ \ref{fig:trans} the judgment $\GG\vd M\LBimp N$
which turns a term $M$ into an equivalent fully applied term $N$:
while we need this translation specialized to simple terms, it is
clear how to generalize this judgment to the canonical forms of any
strict term. The notation $\pi(\GG)$ stands for a permutation of
$dom(\GG)$.


% same context
\begin{figure}
\label{fig:trans}  
\[
\begin{array}{c}
\ianc{}{(\GG,\Omega)\prv  E\ \pi(\GG^{u}) \LBimp Z\ \GG^{u} \
\Omega^{0}}{\mbox{\rm Trn\_Pat}} 
\vsk
\ianc{ (\GG,x\oftp A) \prv  M \LBimp  N }
{\GG\prv \lxua M \LBimp  \lamb{x^u}{A }N }{\mbox{\rm Trn\_Lam}}\vsk
\ianc{  \GG\prv  M_{1}  \LBimp   N_{1}\cdots \GG\prv  M_{n} \LBimp   N_{n} }
{\GG\prv h\  \Mns \LBimp   h\ \Nns} {\mbox{\rm Trn\_App}}
\end{array}
\]
\caption{Full application translation}
\end{figure}


\begin{example}
The simple term from Example \ref{ex:etardx}
$$lam\ (\lamb{x^u}{exp} app\ E\ x)$$ has fully applied form
$$lam\ (\lamb{x^u}{exp} app\ (Z\ x^0)\ x)$$ for a fresh existential
variable $Z$ of type $exp \GImp{0} exp$.
\end{example}

We have now arrived to the following language, where the labeling 
on flexible patterns is unrestricted, that we still call:

\[ \begin{array}{rrcl}
\mbox{\textit{Simple Terms}} & M & \bnfas &  \lam x^{u}\oftp
A^{+}\ldot M \bnfalt (\dots (h\ M_1)^{1} \dots M_n)^{1}\bnfalt E\ 
x^{l_{1}}_{1}\dots{x^{l_{n}}_{n}}
\end{array} \]

To prove the adequacy of the translation, we need  the 
following irrelevance Lemma:


% \newcommand{\cx}{x\oftp C;\cdot;\cdot}
% \newcommand{\cxom}{ x\oftp C;\Omega;\cdot}
\newcommand{\cgm}{\GG;(\O,\xoc);\D}
\newcommand{\cgmom}{ \GG;\Omega;\D}

\begin{Lemma}[Irrelevance]
\label{le:fat}
If $M$ is a simple term without existential variables, then 
\begin{enumerate}
\item 
if $\cgm\vd M\bua A$ then $\cgmom\vd M\bua A$.
\item
if $\cgm\vd M\da A$ then $\cgmom\vd M\da A$.
\end{enumerate}
\end{Lemma}

\begin{proof}
 By mutual induction on $\cD_{1}::\cgm\vd M\da A$ and
 $\cD_{2}::\cgm\vd M\bua A$.
\bit
\itc  $$\cD = \ianc{c\oftp A\in\Sigma}{\GG;(\O,\xoc);\cdot \prv  c\da A}{cIdc}$$
Then
$$\cE= \ianc{c\oftp A\in\Sigma}{\GG;\O;\cdot\prv  c\da A}{cIdc}$$
 
\itc  $$\cD = \ianc{}{(\GG, y\oftp A) ;(\O,\xoc); \cdot  \prv  y \da 
A}{cId^{u}}$$
Then
$$\cE = \ianc{}{(\GG, y\oftp A); \O;\cdot  \prv  y\da A}{cId^{u}}$$

\itc $$\cD = \ianc{}{\GG ;(\O,\xoc); y\oftp A  \prv  y \da 
A}{cId^{1}}$$

Then
$$\cE = \ianc{}{\GG; \O;y\oftp A  \prv  y\da A}{cId^{1}}$$

% \itc  $$\cD = \ianc{\cgm\vd E\ \ol{x_{n}^{l}} \hastype P}{\cgm \vd E\ \ol{x_{n}^{l}} \da  P}{cPat}$$
% \btab
% $\cgm\vd E\ \ol{x_{n}^{l}} \hastype P$\bv
%  $\GG;\Omega;\cdot\vd E\ \ol{x_{n}^{l}} \hastype P$\` By 
%  Weakening$^0$\\
%   $\GG;\Omega;\cdot\vd E\ \ol{x_{n}^{l}} \da P$\br
%   \etab
 \itc  $\cD$ ends in $cAt$: by IH.
% \itc  $$\cD = \ianc{\cgm\prv  M\da P}{\cgm \prv  M\bua P} {cAt}$$
% By inversion $\cgm\prv  M\da P$, by IH  $\cgmom \prv  M\da 
% P$ and hence   $\cgmom \prv  M\bua P$.
 
 
\itc  $$\cD= \ianc{(\GG,y\oftp A);(\O,\xoc);\D \prv M\bua B}{\cgm\prv(\lamb{y^u}{A} M) \bua 
A\TImp B} {c\TImp I}$$
\btab
$(\GG,y\oftp A);(\O,\xoc);\D \prv M\bua B$\bv
$(\GG,y\oftp A);\O;\D\prv M\bua B$ \bi\\
 $\cgmom\prv(\lamb{y^u}{A} M) \bua A\TImp B$\br
 \etab
 
\itc  $$\cD = \ibnc{(\GG,\D_N);(\O,\xoc);\D_M \vd M \da A \RImp
  B}{(\GG,\D_M);(\O,\xoc);\D_N\vd N \bua A}{\GG;(\O,\xoc);\dmn\vd M\ N^1 \da B}{c\RImp E}$$
\btab
$\cD_{1}::(\GG,\D_N);(\O,\xoc);\D_M \vd M \da A \RImp B$\bv
$\cD_{2}:: (\GG,\D_M);(\O,\xoc);\D_N \vd N \bua A$\bv
$\cE_{1}:: (\GG,\D_N);\O;\D_M \vd M \da A \RImp B$ \bi\\
 $\cE_{2}:: (\GG,\D_M);\O;\D_N \vd N \bua A$\bi\\
$\GG;\O;\dmn\vd M\ N^{1}\da B$\br
\etab
\enit
\end{proof}


\subsubsection{Ground Instances}

We recall that we assume every type to be inhabited, so that every 
term can be seen as the intensional representation of the set of its 
ground instances.  The judgment in Fig.\  \ref{fig:grinst} $\GG 
\prv M\in\| N\|\hastype A $ formalizes conditions for  a simple term $M$ to be a 
ground instance of $N$ at type $A$.  
\begin{Remark}
\label{rmrk:gr}
 $\GG \prv M \in\| 
E_A\ \xnl\|\hastype P$ iff $M\equiv t \ \xnl$ and $\cdot\prv t 
\hastype A$, that is $t\equiv \l \xnl\,.\,S$ and if $\xnl = 
(\GG^{u},\O^{0},\D^{1})$ then $\god\vd S \hastype P$.  
\end{Remark}
This fact will be 
heavily used in the following. Moreover we write $\GG\prv M \not\in \| N \|\hastype A$,
 when it is not the case that $\GG\prv M \in \| N \|\hastype A$.

\begin{figure}
\label{fig:grinst}
\[
\begin{array}{c}
\ianc{M\equiv t \ \xnl  \quad \cdot\prv  t \hastype A}
{\GG \prv   M  \in\| E_A\ \xnl\|\hastype P}{grFlx} 
\vsk
\ianc{(\GG,x\oftp A);\Omega;\Delta\prv   M  \in\| N\|\hastype B}
{\GG \prv  \lxua M  \in\|\lxua N \|:A\TImp B}{grLam}
\vsk
% \ianc{\GG \prv h \oftp  A_1\RImp\mdots\RImp A_n \RImp P\quad \GG \prv  \ M_1 \in\| 
% N_{1}\|\hastype A_1\cdots \GG \prv  M_n \in\| N_n\|\hastype A_n }
%  {\GG \prv  h\ \Mns \in\|h\ \Nns
% \|\hastype P} {grApp}
\ianc{\GG \prv h \oftp  A_1\RImp\mdots\RImp A_n \RImp P\quad \GG \prv  \ M_i \in\| 
N_{i}\|\hastype A_i\quad 1\leq i\leq n}
 {\GG \prv  h\ \Mns \in\|h\ \Nns
\|\hastype P} {grApp}
\vsk
\ianc{\god\prv  M \in \|N_{i}\|:A\quad 1\leq i\leq n}
{\god\prv  M \in \|N_{1}\cdots N_{n}\|:A}{gr_{i}} 
\end{array}
\]
\caption{$M$ is a ground instance of $N$ at type $A$}
\end{figure}


\begin{Lemma}[Ground Instance Weakening]
\label{le:giweak}
If $\Gamma\vd M \in \|N\|\hastype AC$ then $(\Gamma, x\oftp A)\vd M 
\in \|N\|\hastype AC$.
\end{Lemma}
\begin{proof}
By induction on the structure of the given derivation.
\end{proof}

We implicitly use the above lemma to  weaken different 
contexts with common basis to an unique one.

\smallskip Now we can prove the set-theoretic adequacy of the full 
application translation.

\begin{Theorem}[Adequacy of Full Application Translation]
\label{thm:fat}
Let $N$ be a simple term of type $A$, such that $\GG \vd N 
\LBimp Q$; then $\GG\vd M\in\|N\|\hastype A$ iff $\GG \vd 
M\in \|Q\|\hastype A$.
\end{Theorem}
\begin{proof}
By induction on the structure of $\cD::\GG\vd M\LBimp 
N$.
\bit
\itc
$\cD$ ends in Trn\_Pat:
\item[$(\Imp)$]
\btab
$(\GG,\Omega)\emp\vd M \in \|E_{B}\ 
\pi(\GG^{u})\|$ \ba
$M\equiv t\ \pi(\GG^{u})$ and $\cdot\vd 
t\hastype B$\bv
$\GG\emp \vd S\hastype A$\` By Remark \ref{rmrk:gr}\\
 $\GG\emp\vd S\buda A$\` By  the canonical form Theorem  \\
$\GG;\Omega;\cdot\vd S\buda A$\` By Weakening$^0$\\
$\GG;\Omega;\cdot\vd S\hastype A$\` By soundness of canonicity\\
%$\GG;\Omega;\cdot\vd S\hastype A$.  Thus
\ignore{ $M\equiv t'\ \GG^{u} 
\Omega^{0}$ for $\cdot\vd t'\hastype B'$, \ie}
 $\GG\vd M\in \|F_{B'}\ \GG^{u} \Omega^{0}\|$\br and  Remark \ref{rmrk:gr}
\etab
\item[$(\If)$]
\btab
$\GG\vd M\in \|F_{B'}\ \GG^{u} \Omega^{0}\|$\ba
$M\equiv t'\ \GG^{u} \Omega^{0}$ for $\cdot\vd t'\hastype B'$\bv
$\GG;\O;\cdot \vd S\hastype A$\` By Remark \ref{rmrk:gr}\\
$\GG;\O;\cdot \vd S\buda A$\` By  the canonical form Theorem  \\
$\GG;\cdot;\cdot\vd S\buda A$\` By Lemma \ref{le:fat}\\ 
$\GG;\cdot;\cdot\vd S\hastype A$\` By soundness of canonicity\\
$\GG\emp\vd M \in \|E_{B}\ \pi(\GG^{u})\|$ \br  and  Remark \ref{rmrk:gr}
\etab
\itc
$\cD$ ends in Trn\_Lam or Trn\_App:
the result follows from a straightforward application of the inductive hypothesis.
\enit\end{proof}


From now on we tacitly assume that all simple terms are fully
applied.  We call a term $E\, x_1^{l_1}\ldots x_n^{l_n}$ a
\emph{generalized variable}.

\section{The Complement Algorithm}
\label{sec:compl}

The idea of complementation for applications and abstractions is quite
simple and similar to the first-order case.  For generalized variables
we consider each argument in turn.  If an argument variable is undetermined
it does not contribute to the negation.  If an argument variable is strict
then any term where this variable does not occur contributes to
the negation.  We therefore complement the corresponding label from $0$
to $1$ while all other arguments are undetermined.  For vacuous
argument variables we proceed dually.  
% In preparation for the rules
% we define.
% \beq 
% \mnot(1)  =  0\quad
% \mnot(0)  =  1\quad
% \eneq
If $\Gamma = x_1\oftp A_1,\ldots, x_n\oftp A_n$, we write $E\ \Gamma^u$ for
the application of $E\ {x_1}^u\ldots{x_n}^u$.  Such an application represents
the set of all terms without existential variables and free variables
from $\Gamma$.

% The idea of complementation of flexible simple patterns is to form 
% a set of terms under a  context according to the occurrence status of every 
% variable; if the former is determined (must or must not occur) a term 
% with the given variable annotated with the complement of the 
% annotation is built where the remaining variables are set to 
% undetermined, otherwise we do nothing, \ie we do not build a term.  

First, observe that the complement operation on terms behaves on 
labels like negation does on truth-values in Kleene's three-valued logic, in the 
sense of the following table: 
\beq 
\mnot(1)& = &0\\
\mnot(0)& = &1\\
\mnot(u) & = & u
\eneq
Note that these labels form a three-valued semi-lattice with 
the (reverse) partial 
information ordering $1\leq u,0 \leq u$. 

% Finally we present the system for pattern complement.  Since we 
% restrict to  simple terms, we need only one context, the 
% undetermined one.  Hence we abridge $\GG\vd\mnot(M)=N$ in 
% $\GG\vd\mnot(M)=N$. However, keep in mind that every token is in the 
% image of the $\_^{\pm}$ translation.


\begin{Definition}[Higher-Order Pattern Complement]
\label{def:compl}

Fix a signature $\Sigma$.  For a linear simple term  
$M$ such that $\GG \prv  M \hastype  A$ define $\GG\prv  \mnot(M) \blip  N\hastype A$
by the following rules.  Note that a given $M$ may be related to several
terms $N$ all of which belong to the complement of $M$.

\begin{small}
\[
\begin{array}{c}
\ianc{1\leq i\leq n\quad k\in\{1,0\}} {\GG\prv \mnot(E \ x_{1}^{l_{1}}\dots x_{i-1}^{l_{i-1}} \ 
x_{i}^{k}\ x_{i+1}^{l_{i+1}}\dots x_n^{l_{n}}) \blip  Z\ x_{1}^{u}\dots 
x_{i-1}^{u}\ x_{i}^{\mnot(k)}\ x_{i+1}^{u}\dots x_n^{u}\hastype P} {\mnot\_Flx}
\vsk
\mbox{\textrm{no rule for } $k=u$}
\vsk
\ianc{\GG,x\oftp A\prv  \mnot( M)  \blip   N\hastype B}
{\GG\prv  \mnot(\lxua M)  \blip  \lxua N\hastype A\Imp B}{\mnot\_Lam}
\vsk
\ianc{g\in\Sigma\cup\GG, g \hastype A_{1}\RImp\dots\RImp A_{m}\RImp 
P\quad m\geq 0,h \not\equiv g   } 
{\GG\prv  \mnot (h\ \Mn^1) \blip  
(\dots (g\ (Z_{1} \GG^{u}))^{1}\dots (Z_{m}\GG^{u}))^{1}\hastype P} {\mnot\_App^{1}}
\vsk
\ianc{  \GG\prv \mnot( M_i) \blip  N\hastype A_i\qquad 1\leq i\leq n } 
{\GG\prv  \mnot (h\ \Mn^1) \blip  
(\dots (h\ (Z_{1}\GG^{u} ))^{1}\dots (Z_{i-1}\GG^{u} )^{1} \ N^{1}\ 
(Z_{i+1}\GG^{u} )^{1}\dots (Z_{n}\GG^{u}))^{1}\hastype P} {\mnot\_App^{2}}
\end{array}
\]
\end{small}

\noindent where the $Z$'s are fresh logic variables and 
$h\in\Sigma\cup\GG$ and $\GG\prv h\hastype A_{1}\RImp\dots\RImp 
A_{n}\RImp P$. Finally we define $\GG\vd\mmnot(M)= \cN\hastype A$ if 
$\cN=\{N\mid\GG\prv \mnot(M)\blip N\hastype A\}$.
\end{Definition}

 We may drop the type
 %and signature 
information from the above judgment in examples and proofs.

Note that if $E_A$ is a generalized variable considered in the empty context,
 it has the canonical form $\l \ol{x_{n}^{u}}\,.\,E\ \ol{x_{n}^{u}}$. Hence
$\cdot\vd\mmnot(E_{A}) = \eset$ as expected.


\begin{example} If $\GG=x\oftp B,y\oftp C$:
\begin{eqnarray}
\GG\vd\mmnot( E\ x^{u} y^{1}) & = & \{ F\ x^{u} y^{0}\}\nonumber \\
\GG\vd\mmnot( E\ x^{0} y^{1}) & = & \{ F\ x^{1} y^{u}, G\ x^{u} y^{0}\} 
\label{eq:l}
\end{eqnarray}
\end{example}

It is worthwhile to observe that the members of a complement set  are not 
mutually disjoint, due to the indeterminacy of $u$. We can achieve 
an exclusive `or' if we resolve this indeterminacy, that is by 
considering for every $x^{u}$ the two possibilities $x^{1},x^{0}$. 
Thus, for example,  equation (\ref{eq:l}) may be made explicit into:
\[
\{F \ x^{1} y^{1},    G \ x^{1} y^{0},  H \ x^{0} y^{0}\}
\]
It is clear that in the worst case scenario the number of terms in a 
complement set is bound by $2^{n}$; hence the usefulness of this 
further step needs to be pragmatically determined.


% \renewcommand{\ng}{\GG\prv\mnot}

\begin{example} Take the signature of numerals:
\beq
\lefteqn{\mmnot(\l x^{u}\l y^{u}.\, s(M\ x^{1} y^{0})^{1}   =}\\
& \{ \l x^u\l y^u .\, x, \l x^u\l y^u .\, y, \l x^u\l y^u .\, 0, \l 
x^u\l y^u .\, s(N\ x^{0} y^{u})^{1}, \l x^u\l y^u .\, s(N'\ x^{u} 
y^{1})^{1} \} 
\eneq
\end{example}

We can now revisit\footnote{To avoid too many indices on existential variables,
we adopt a convention that the scope of existential variables is
limited to each member of a complement set.}
 Example \ref{ex:etardx}:
\beq
\lefteqn{\mmnot(lam(\lamb{x^{u}}{exp} app\ (E\ x^{0})\ x ))=}\\
& & \{ lam(\lamb{x^u}{exp} app\ (H\ x^1)\ (H'\ x^u)),\\
& & lam(\lamb{x^u}{exp} app\ (H\ x^u)\ (app\ (H'\ x^u) \ (H'' x^u)), \\
& &lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H'\ x^u\ y^u)),\\
& & lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H\ x^u\ y^u) ),\\
& & lam(\lamb{x^u}{exp}x),\\
& & app\ H\ H'\}
\eneq

% We can now revisit Example \ref{ex:etardx}:
% \beq
% \lefteqn{\mmnot(lam(\lamb{x^{u}}{exp} app\ (M\ x^{0}) x^{1} ))\blip }\\
% & & \{ lam(\lamb{x^u}{exp} app\ (H\ x^1)\ H,
% \{ lam(\lamb{x^u}{exp} app\ (H\ x^u)\ (app\ H_4\ H_5)), \\
% lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H_6\ x^u\ y^u)),
% & & app\ H_1\ H_2,\\
%  & &lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H_3\ x^u\ y^u) )\}
% \eneq
\smallskip

It is  possible to show that simple terms are closed under complementation.

\begin{Theorem}
If $M$ is a simple term and $\GG\vd\mnot(M)\blip  N\hastype A$, then  $N$ is simple.
\end{Theorem}
\begin{proof}
By induction on the structure of $\cD::\GG\vd\mnot(M)\blip  N\hastype A$.
\bit
\itc
 $\cD$ ends in $\mnot\_Flx$: immediate.
% $M\equiv E\ \ol{x_{n}^{l}}$. Then for $1\leq i\leq n$ and for 
% $k\in\{1,0\}$ 
% $\GG\prv \mnot(E \ x_{1}^{l_{1}}\dots x_{i-1}^{l_{i-1}} \ 
% x_{i}^{k}\ x_{i+1}^{l_{i+1}}\dots x_n^{l_{n}}) \blip  Z\ x_{1}^{u}\dots 
% x_{i-1}^{u}\ x_{i}^{\mnot(k)}\ x_{i+1}^{u}\dots x_n^{u}\hastype P$ by rule , where the latter is simple.
\itc
$$\cD=\ianc{\GG,x\oftp A\prv  \mnot( M)  \blip   N\hastype B}
{\GG\prv  \mnot(\lxua M)  \blip  \lxua N\hastype A\Imp B}{\mnot\_Lam}$$
By inversion $\GG,x\oftp A\prv  \mnot( M)  \blip   N\hastype B$, hence by IH $N$ 
is simple and so is $\lxua N$.
\itc
$$\cD=\ianc{g\in\Sigma\cup\GG, g \hastype A_{1}\RImp\dots\RImp A_{m}\RImp 
P\quad m\geq 0,h \not\equiv g   } 
{\GG\prv  \mnot (h\ \Mn^1) \blip  
(\dots (g\ (Z_{1} \GG^{u}))^{1}\dots (Z_{m}\GG^{u}))^{1}\hastype P} {\mnot\_App^{1}}
$$ 
Since every $(Z_{i}\GG^{u)}$ is simple, so is $(\dots (g\ (Z_{1} 
\GG^{u}))^{1}\dots (Z_{m}\GG^{u}))^{1}$.
\itc
$\cD=$
 \begin{small}
$$\ianc{ 
% h\in\Sigma\cup\GG,\GG\prv h\hastype A_{1}\RImp\dots\RImp 
% A_{n}\RImp P\qquad \mbox{\textrm{for some} $i$} \quad 
\GG\prv \mnot( M_i) \blip  N\hastype A_i \qquad 1\leq i\leq n} 
{\GG\prv  \mnot (h\ \Mn^1) \blip  
(\dots (h\ (Z_{1}\GG^{u} ))^{1}\dots (Z_{i-1}\GG^{u} )^{1} \ N^{1}\ 
(Z_{i+1}\GG^{u} )^{1}\dots (Z_{n}\GG^{u}))^{1}\hastype P} {\mnot\_App^{2}}
$$
 \end{small}
By inversion and IH $N$ is simple and as above so is every $(Z_{i}\GG^{u})$.
Thus $(\dots (h\ (Z_{1}\GG^{u} ))^{1}\dots (Z_{i-1}\GG^{u} ) \ 
N^{1}\ (Z_{i+1}\GG^{u} )^{1}\dots (Z_{n}\GG^{u}))^{1}$ is simple.
\enit\end{proof}

\begin{Corollary}
If $M$ is a simple term, so is $N$, for all $N\in\GG\vd\mmnot(M)\hastype A$.
\end{Corollary}

\medskip We address the soundness and completeness of the complement
algorithm \wrt the set-theoretic semantics: the proof obligation
consists in proving that the former does behave as a complement
operation on sets of patterns. Termination is obvious as the algorithm
is syntax-directed and only finitely branching.   
We abridge $\mnot(l)$ in $-l$. We start with soundness:

\begin{Theorem}
\label{thm:part1}
Let $\GG\vd N\hastype A$ be simple linear pattern and assume there is
a $Q$ such that $\GG\vd \mnot(N)\blip Q\hastype A$: it is not the case
that both $\GG\vd M \in \| N\|\hastype A$ and $\GG\vd M \in \|
Q\|\hastype A$.
\end{Theorem}

\begin{proof}
By induction on the structure of $\cD::\GG\vd \mnot(N)\blip Q$.
\bit
\itc $\cD$ ends in $\mnot\_Flx$.
First observe that $E\ \ol{x_{n}^{l}}$ can be seen as $E\ 
\Phi^{u}\Omega^{0}\Delta^{1}\ x^{d}$, where $x$ is determined; 
indeed if $x$ is undetermined, the result holds trivially.  Assume 
$\GG\vd M\in \|E\ \Phi^{u}\Omega ^{0}\Delta ^{1}\ x^{d}\|$ and 
$\GG \vd M\in\|F\ \Phi^{u}\Omega ^{u}\Delta ^{u}\ x^{-d}\|$ for 
some $d\in\{1,0\}$.  Then it holds that both $\Phi;\O;(\D,x\oftp 
A)\vd M\hastype C$ and $(\Phi,\O,\D);x\oftp A;\cdot\vd M\hastype 
C$ or $\GG;(\O,x\oftp A);\D\vd M\hastype C$ and 
$(\GG,\O,\D);\cdot;x\oftp A\vd M\hastype C$, depending on the 
polarity of $d$.  Both cases are impossible by Corollary 
\ref{co:disj}.
 
\itc  $\cD$ ends in $\mnot\_App^{1}$.
Suppose both $\GG\vd M\in \|h\ \ol{N_n^{1}}\|$ and 
$\GG \prv M\in \|g\ (Z_{1} \GG^{u})^{1}\dots (Z_{m}\GG^{u})^{1}\| $ 
for $h\not\equiv g$; but this is immediately impossible by rule 
$grApp$ as the root of $M$ should be both $h$ and $g$.  

\itc $\cD$ ends in $\mnot\_App^{2}$.
\btab
$\GG\prv  \mnot (h\ \Mn^1) \blip  
(\dots (h\ (Z_{1}\GG^{u} ))^{1}\dots (Z_{i-1}\GG^{u} )^{1} \ N^{1}\ 
(Z_{i+1}\GG^{u} )^{1}\dots (Z_{n}\GG^{u}))^{1}$\\ \bh
$\GG\vd\mnot(N_i)\blip  Q$,  for $1\leq i\leq n$ \`    By inversion  \\
$\GG\vd h\ \ol{M_n^{1}}\in \|h\ \ol{N_n^{1}}\|$  \` By assumption\\
$\GG \prv h\ \ol{M_n^{1}}\in \| h\ (Z_{1}\GG^{u} )^{1}\dots 
(Z_{i-1}\GG^{u} )^{1}\ Q^{1}\ (Z_{i+1}\GG^{u} )^{1}\dots (Z_{n}\GG^{u} 
)^{1} \|$\\ \` By assumption\\
$\GG \prv M_{i}\in\|N_{i} \|$\`    By inversion \\
$\GG \prv M_{i}\in\|Q \|$\bv
$\perp$\` By IH\\
$\perp$\` By rule
\etab
\itc $\cD$ ends in $\mnot\_Lam$:
\btab
$\GG\vd \mnot( \lxua N) \blip  \lxua Q$\bh
 $\GG,x\oftp A\vd \mnot( N) \blip  Q$\bv
$\GG \prv \lxua M\in \| \lxua N\|$ 
\` By hypothesis\\
 $\GG \prv \lxua M\in \| \lxua Q\|$
\` By assumption\\
$\GG,x\oftp A \vd M\in \| N\|$\`  By inversion \\
$\GG,x\oftp A \prv M\in \| Q\|$,\`  By inversion \\
$\perp$\` By IH\\
$\perp$\` By rule
\etab
\end{itemize}
\end{proof}

Note that soundness is based on Corollary \ref{co:disj}, which holds 
for \emph{any} strict term: thus disjointness does not require simple 
terms.

We are now ready to prove exhaustivity of complementation.

\begin{Theorem}
\label{thm:part2}
Assume $\GG\vd N\hastype A$ is  simple linear pattern and there is a $Q$ 
such that $\GG\vd \mnot(N)\blip Q\hastype A$: then,  either $\GG \prv M\in 
\| N \| \hastype A$ or  $ \GG \prv M\in \| Q\| \hastype A$.
\end{Theorem}
\begin{proof}
By induction on the structure of $\cD::\GG\vd \mnot(N)\blip Q\hastype A$ 
\bit

\itc 

$\cD$ ends in $\mnot\_Flx$.  Again observe that $E\ \ol{x_{n}^{l}}$ can 
be seen as $E\ \Phi^{u}\Omega^{0}\Delta^{1}\ x^{d}$, where 
$x$ is determined; indeed if $x$ is undetermined, the result holds 
trivially; by Corollary \ref{co:exh} either $GG;(\O,x\oftp C);\D\vd M\hastype A$ 
or $(\GG,\O,\D);\cdot;x\oftp C;\vd M\hastype A$ and either 
$\GG;\O;(\D,x\oftp C\vd M\hastype A$ 
or $(\GG,\O,\D);\cdot;x\oftp C \vd M\hastype A$, depending on the 
polarity of $d$.  Thus 
$\GG\vd M\in \|E\ \Phi^{u}\Omega ^{0}\Delta ^{1}\ x^{d}\|$ or $\GG 
\vd M\in\|F\ \Phi^{u}\Omega ^{u}\Delta ^{u}\ x^{-d}\|$ for some 
$d\in\{1,0\}$.
\itc $\cD$ ends in $\mnot\_App^{1}$.
let $M$ be a ground term $g\ \Mm$ where 
$g\in\Sigma\cup\GG, g\not\equiv h$.  Then clearly $\GG\vd g\ \Mm\in \|g\ (Z_{1} 
\GG^{u})^{1}\dots (Z_{m}\GG^{u})^{1}\| $,
%  where $\GG \prv \mnot(h\ 
% \ol{N_n^{1}}) = g\ (Z_{1} \GG^{u})^{1}\dots (Z_{m}\GG^{u})^{1}\| $,
 hence the thesis by weakening.
\itc$\cD$ ends in $\mnot\_App^{2}$.
\btab
$\GG\vd\mnot(N_{i}) \blip  Q$ for $1\leq i\leq n$ \bv
$\GG\vd h\ \ol{N_n^{1}}\hastype P$ \` By assumption\\
$\GG\vd N_{i}\hastype A_{i}$\`  By inversion \\
$\GG \prv M_{i}\in \| N_{i} \| \hastype A_{i}$\`  By the left horn of IH \\
$\GG \prv h\ \ol{M_n^1}\in \| h\ 
\ol{N_n^1} \| \hastype P$\`  by rule $grApp$ \\
%$\GG \prv h\ \ol{M_n^1}\in \| h\ \ol{N_n^1} \| \hastype P$ or \\
% $\GG \prv h\ \ol{M_n^1}\in \| h\ 
% (Z_{1}\GG^{u} )^{1}\dots (Z_{i-1}\GG^{u} )^{1}\ Q^{1}\ 
% (Z_{i+1}\GG^{u} )^{1}\dots (Z_{n}\GG^{u} )^{1} \| \hastype P$\\
% \`  by 
hence the thesis by weakening \\ $ \GG \prv M_{i}\in \| Q\| \hastype
 A$ \` By the right horn of IH\\ $\GG\vd M_{j}\in\|(Z_{j}\GG^{u}
 )^{1}\|$ for $j\neq i, 1\leq j\leq n$\` By rule $grFlx$\\ $\GG \prv
 h\ \ol{M_n^1}\in \| h\ (Z_{1}\GG^{u} )^{1}\dots (Z_{i-1}\GG^{u}
 )^{1}\ N^{1}\ (Z_{i+1}\GG^{u} )^{1}\dots (Z_{m}\GG^{u} )^{1} \|
 \hastype P$\\ \` by rule $grApp$ \\ hence, by weakening the result.
 \etab

\itc $\cD$ ends in $\mnot\_Lam$.  \btab
% $\GG\vd\lxua N\hastype A\TImp B$\` By assumption\\
%  $\GG, x\oftp A\prv N\hastype B$\`  by inversion\\
$\GG,x\oftp A\vd\mnot(N)\blip Q$\bv $\GG,x\oftp A \prv M\in \| N \|
\hastype B$\` By the left horn of IH\\ $\GG \prv \lxua M\in \|\lxua N
\| \hastype A\TImp B$ \` by rule $grLam$ \\
%  $\GG \prv \lxua M\in \|\lxua N \| \hastype 
% A\TImp B$ or there is a $\lxua Q$ such that $\GG\vd\mnot(\lxua N) \blip  
% \lxua Q$ and $ \GG \prv \lxua M\in \|\lxua Q\| \hastype A\TImp B$\` 
hence the thesis by weakening\\ $ \GG \prv M\in \| Q\| \hastype B$\`
By right horn of IH\\ $ \GG \prv \lxua M\in \| \lxua Q\| \hastype
A\TImp B$\` by rule\\
%  $\GG \prv \lxua M\in \|\lxua N 
% \| \hastype A\TImp B$ or there is a $\lxua Q$ such that 
% $\GG\vd\mnot(\lxua N) \blip  \lxua Q$ and $ \GG \prv \lxua M\in \|\lxua 
% Q\| \hastype A\TImp B$\` 
hence the thesis by weakening.  \etab \enit
\end{proof}

\begin{Corollary}[Partition Lemma] For a fixed signature $\Sigma$ let 
$\GG\vd N \hastype A$ be a linear simple term:
\label{lemma:part}
\ben
\item (Disjointness) It is not the case that $\GG\prv M\in \| N
\|\hastype A$ and $\GG\prv M\in \| \mmnot(N) \|\hastype A$.
\item (Exhaustivity) $\GG\prv M\in \| N \| \hastype A$ or $\GG\prv
M\in \| \mmnot(N) \|\hastype A$.  \enen
\end{Corollary}
\begin{proof}
Disjointness is entailed by Theorem \ref{thm:part1},
% and the canonical form Theorem (Theorem \ref{thm:canonical}),
exhaustivity by Theorem \ref{thm:part2}.
\end{proof}


\section{Unification of Simple Terms 
% in the Strict $\lambda$-Calculus
}
\label{sec:sunif}

We now address the issue of unification, \ie intersection of simple
linear \ho patterns.  We start by determining when two labeling are
compatible: \beq 1 \cap 1 = u \cap 1 = 1\cap u = 1\\ 0 \cap 0 = u \cap
0 = 0\cap u = 0\\ u\cap u = u \eneq
%  we define an intersection operator on occurrence labels as 
% the symmetric and idempotent extension of the following partial 
% operation: 

% \beq
% 1\cap u = 1\\ 0\cap u = 0\\ u\cap u = u
% \eneq

We use $\Phi$ for (contexts) of labeled bound variables, \ie what we
call $\xnl$ and if $x^k\in\Phi$, we say that $\Phi(x)= k$.  We then
extend the intersection operations to these contexts; remember that
full application entails that we only intersect context that are the
same modulo different labeling: \beq \cdot\mcap \cdot & = & \cdot\\
(x^k\ \Phi)\mcap (x^{k'}\ \Phi') & = & x^{k\mcap k'}\ (\Phi\mcap
\Phi') \quad\mbox{\textrm{if $k\mcap k'$ is defined.}}  \eneq

 \newcommand{\godf}{\GG_{1};\Omega_{1};\Delta_{1}}
\newcommand{\gods}{\GG_{2};\Omega_{2};\Delta_{2}}
\newcommand{\godt}{(\GG_{1}\cap\GG_{2});(\Omega_{1},\Omega_{2});(\Delta_{1},\Delta_{2})}

Thus if $\Phi_{1}\cap\Phi_{2}$ is defined and $\Phi_{1} = \godf$ and
$\Phi_{2} = \gods$, we call the latter type assignments
\emph{compatible}.

\begin{Remark}
\label{rmrk:compa}
 $\Psi\vd M\in \|E_{A}\ \Phi_{1}\cap\Phi_{2}\|$ iff $M\equiv \l
\Phi_{1}\cap\Phi_{2}\,.\,S$ such that $\god\vd S\hastype A$, where
\beq \GG & = & (\GG_{1}\cap\GG_{2})\\ \O &= &(\O_{1},\O_{2})\\ \D & =
& (\D_{1},\D_{2}) \eneq Indeed, $x\in\GG$ iff $x\in\GG_{1}$ and $x\in
\GG_2$; moreover $x\in\O$ iff either $x\in\O_1\cup\GG_{2}$ or
$x\in\O_2\cup\GG_{1}$.  Analogously for $x\in\D$.
\end{Remark}

\begin{Lemma}
\label{le:compat}
Let $\GG_1\cup\D_1=\GG_2\cup\D_2$. Then
$(\GG_1\cup\D_1)\cap(\GG_2\cup\D_2)= (\GG_1\cap\GG_2)\cup\D_1\cup\D_2 $.
\end{Lemma}
\begin{proof}
\begin{metanote} A miracle \end{metanote}
\end{proof}

\medskip
Following standard terminology with call atomic terms whose head is a
free or bound variable \emph{rigid}, while terms whose head is an
existential variable is called \emph{flexible}.


\begin{Definition}[Higher-Order Pattern Intersection]
Fix a signature $\Sigma$. For simple linear terms $M$ and $N$ without
 shared variables such that $\GG \prv M \hastype A$ and $\GG \prv N
 \hastype A$, define $\GG\prv M \mcap N \blip Q \hastype A$ by the
 following rules:


\begin{small}
\[
\begin{array}{c}
\ianc{
% \Phi_1\mcap \Phi_2 = \Phi%\quad \Phi\not = nil
 }
{\GG\prv  E \ \Phi_1\mcap   F\ \Phi_2\blip  H\ (\Phi_{1}\mcap \Phi_{2}) \hastype  P} 
{\mcap\_FlxFlx}
\vsk
\mbox{\textrm{no rule for flex-flex same}}
\vsk
\ianc{c\in\Sigma\quad \GG\prv  H_1 \ \Phi_{1}\mcap 
M_{1}\blip N_{1}\hastype A_{1}\cdots \GG\prv  H_n \ \Phi_{n}\mcap 
M_{n}\blip N_{n}\hastype A_{n}  } 
{ \GG\prv  E \ \Phi \mcap c\ \Mns\blip  c\ \Nns\hastype  P} {\mcap\_FlxRgd^c }
\vsk
\ianc{y\in\GG\quad  \quad \GG\prv  H_1 \ \Phi_{1}\mcap 
M_{1}\blip N_{1}\hastype A_{1}\cdots \GG\prv  H_n \ \Phi_{n}\mcap 
M_{n}\blip N_{n}\hastype A_{n} } 
{\GG\prv E\ \Phi \mcap y\ \Mns\blip  y\ \Nns \hastype  P} {\mcap\_FlxRgd^y }
\vsk
\ianc{ h\in\GG\cup\Sigma\quad \GG\prv  M_1 \mcap N_{1} \blip  Q_1\hastype  A_1 \cdots \GG\prv  M_n \mcap 
N_{n}\blip  Q_n \hastype  A_n} 
{\GG\prv   h\ \Mns\mcap h\ \Nns \blip  h\ \ol{Q_{n}^{1}} \hastype  P} {\mcap\_App}
\vsk
\ianc{\GG,x\oftp A\prv   M  \mcap  N \blip  Q\hastype  B}
{\GG\prv   \lxua M  \mcap \lxua N \blip \lxua Q \hastype  A\Imp B}{\mcap\_Lam}
\end{array}
\]
\end{small}
where  the $H$'s are fresh 
variables of correct typing and $n\geq 0$. 
 % The rule 
% $\mcap\_FlxRgd^c $ has the following proviso: for all $x\in \Phi$ and
% $1\leq i\leq n$
% \beq
% \forall x. \Phi(x) = 0 & \Imp & \forall i\,.\, \Phi_{i}(x) = 0\\ 
% \forall x. \Phi(x) = u & \Imp & \forall i\,.\, \Phi_{i}(x) = u\\ 
% \forall x. \Phi(x) = 1 & \Imp & \exists i\,.\, \Phi_{i}(x) = 1
% %\And \forall j, j\not = i. \Phi_{j}(x)\not = u
% \eneq
% The rule 
% $\mcap\_FlxRgd^y $ has the additional proviso: 
% \beq
% \Phi(y) \not = 0\And ( \Phi(y)=1& \Imp & \forall i. \Phi_{i}(y) = u)\ignore{\\
% \forall x. \Phi(x) = 0 & \Imp & \forall i. \Phi_{i}(x) = 0\\ 
% \forall x. \Phi(x) = u & \Imp & \forall i. \Phi_{i}(x) = u\\ 
% \forall x. \Phi(x) = 1 & \Imp & \exists i. \Phi_{i}(x) = 0
% \And \forall j, j\not = i. \Phi_{j}(x)\not = u
% }\eneq
% Finally define 
% \beq
% M\mbigcap N \hastype A & =& \{Q\mid\cdot\prv  M\mcap N = Q \hastype  A\}
% \eneq
The rules
$\mcap\_FlxRgd^c$ and $\mcap\_RgdFlx^c$ have the following proviso: for all
$x\in \Phi$ and $1\leq i\leq n$:
\beq
\forall x. \Phi(x) = 0  \Imp  \forall i\,.\, \Phi_{i}(x) = 0\\ 
\forall x. \Phi(x) = u  \Imp  \forall i\,.\, \Phi_{i}(x) = u\\ 
\forall x. \Phi(x) = 1  \Imp  \exists i\,.\, \Phi_{i}(x) = 1
\And \forall j, j\not = i. \Phi_{j}(x) = u
\eneq
The rules $\mcap\_FlxRgd^y$ and $\mcap\_RgdFlx^y$ are subject to the
proviso
\beq
\forall x. \Phi(x) = 0  \Imp  \forall i\,.\, \Phi_{i}(x) = 0\\ 
\forall x. \Phi(x) = u  \Imp  \forall i\,.\, \Phi_{i}(x) = u\\ 
\forall x. x \not= y \And \Phi(x) = 1  \Imp  \exists i\,.\, \Phi_{i}(x) = 1
\And \forall j, j\not = i. \Phi_{j}(x) = u \\
\Phi(y) = u \Or
(\Phi(y)=1 \And  \forall i. \Phi_{i}(y) = u)
\eneq
Finally define $\GG\vd M\mbigcap N \hastype A = {\cal Q}$ if ${\cal Q}=
 \{Q\mid\GG\prv  M\mcap N \blip  Q \hastype  A\}$.
\end{Definition} 

Some remarks are in order:
\bit
\item
In rule $\mcap\_FlxFlx$ we can assume that the same list 
of variables, though with different labeling, is the argument of $E,F$ 
and $H$, since simple terms are fully-applied and due to linearity we 
can always reorder the context to the same list.  
\item
 Since patterns are linear and $M$ and
$N$ share no pattern variables, the flex-flex case arises only with distinct
variables.  This also means we do not have to apply substitutions or perform
the customary occurs-check.
\item 
In the flex/rigid and rigid/flex rules, the proviso enforces the typing
discipline since each strict variable $x$ must be strict in some premise.
% The modified condition on $y$ takes into account that the head of an
% application constitutes a strict occurrence.
% In  rule $\mcap\_FlxRgd$ the proviso enforces the typing discipline, 
% for which $x$ must be strict in some premise.
% %  is compelled by the typing 
% % rules not to leave the status of $x$ undetermined in the antecedent, 
% % when $c$ is a constant.  
% \item
If instead $y$ is the projected variable, it 
\textbf{does} occur in the RHS: hence it \emph{ought to} occur in the 
LHS: moreover, since it did occur, it is set to $u$ in the rest of the 
computation, as there are no more requirements on that variable, therefore
the modified condition on $y$ takes into account that the head of an
application constitutes a strict occurrence.
\item
We also need an  exchange rule:
$$
\ianc{ h\in\GG\cup\Sigma\quad  \GG\prv N\mcap h\ \Mns \blip  Q\hastype  P} 
{\GG\prv   h\ \Mns\mcap N \blip  Q \hastype  P} 
{\mcap\_Excng}$$
As usual,  this kind of rule is problematic \wrt termination. We can
 avoid it if we agree to implicitly add the symmetric rules  $\mcap\_
RgdFlex^c$ and  $\mcap\_RgdFlex^y$.
\enit

The following example illustrates how the Flex-Rigid rules, in this 
case $\mcap\_FlxRgd^c$, make unification on simple terms finitary.

\begin{example}
Consider the unification problem $x\oftp A\prv E\ x^{1}\mbigcap\ 
c\ (F\ x^{u})^{1} \ (F'\ x^{u})^{1}$.  Since $x$ is strict in 
the LHS, there are two ways in which $\Phi$ can be `split' leading 
to the following sub-problems:
\[
\begin{array}{lrr}
x\oftp A\prv E' \ x^{1}\mcap\  F\  x^{u} \blip  H\  x^{1}
& & x\oftp A\prv E''\ x^{u}\mcap\  F'\  x^{u} \blip  H'\  x^{u}
\\
x\oftp A\prv E' \ x^{u}\mcap\  F\  x^{u} \blip  H\  x^{u}
& & x\oftp A\prv E''\ x^{1}\mcap\  F'\  x^{u} \blip  H'\  x^{1}
\end{array}
\]
Hence the result:
\begin{eqnarray*}
%\label{eq:int}
x\oftp A\prv E\ x^{1}\mbigcap\  c\ (F\  x^{u})^{1} \ (F'\  
x^{u})^{1}& = &  \{c\ (H\  x^{1})^{1} \ (H'\  x^{u})^1,c\ (H\  x^{u})^1 \ (H'\  
x^{1})^1\}
\end{eqnarray*}
\end{example}

Note that, similarly to complementation, intersection return a 
solution with some `overlapping' possible; again it is possible, in a 
post-processing phase to make the result exclusive:
for example the above problem \ignore{(\ref{eq:int})} can be explicited in:
\beq
\lefteqn{x\oftp A\prv E\ x^{1}\mbigcap\  c\ (F\  x^{u})^{1} \ (F'\  
x^{u})^{1} = }\\
& & \{c\ (H\ x^{1})^{1} \ (H'\ x^{0})^1,c\ (H\ x^{0})^1 \ 
(H'\ x^{1})^1,c\ (H\ x^{1})^1 \ (H'\ x^{1})^1\}
 \eneq 

However, it must be noted that the latter is not the most general 
solution \wrt the subsumption ordering on terms based on  the 
(reverse) partial information ordering on labels.  Indeed, say, $c\ 
(H\ x^{1})^{1} \ (H'\ x^{0})^1 \leq E\ x^{1}$ and $c\ (H\ 
x^{})^{1} \ (H'\ x^{0})^1\leq c\ (H\ x^{u})^{1} \ (H'\ 
x^{u})^1$, but $c\ (H\ x^{1})^{1} \ (H'\ x^{0})^1\leq c\ 
(H\ x^{1})^{1} \ (H'\ x^{u})^1$.

\smallskip The following example illustrates the 
additional proviso on $\mcap\_FlxRgd_{y}$:

\begin{example}
The unification problem $y\oftp A\vd E\ y^{0} \mbigcap y\ (F\ y^{u})^{1} 
\ (F'\ y^{u})^{1}$ has no solution, whereas $y\oftp A\vd E\ y^{1} 
\mbigcap y\ (F\ y^{1})^{1} \ (F'\ y^{0})^{1}= \{y \ (H\ y^{1})^1 \ 
(H'\ y^{0})^1\} $.
\end{example}

\begin{Lemma}
\label{le:flexunif}
Let $\godf\vd M\hastype A$ and $\godf\vd M\hastype A$ be \emph{compatible} 
type assignments; then $\godf\vd M\hastype A$ and 
$\gods\vd M\hastype A$ iff $\godt \vd M\hastype A$.
\end{Lemma}
\begin{proof}
($\Imp$). By induction on the structure of $\cD_1::\godf\vd M\hastype A$ and 
$\cD_2::\gods\vd M\hastype A$.  
\bit
\itc 
$$\cD_1=\ianc{c\oftp A\in \Sigma}{\GG_{1};\O_{1}\cdot\vd c\hastype 
C}{Con}\qquad
\cD_2=\ianc{c\oftp A\in \Sigma}{\GG_{2};\O_{2}\cdot\vd c\hastype 
A}{Con}$$
Then
$$\cE=\ianc{c\oftp A\in \Sigma}{(\GG_{1}\cap\GG_{2});(\O_{1},\O_{2});\cdot\vd c\hastype 
A}{Con}$$
\itc 
$$\cD_1=\ianc{}{(\GG_{1},x \oftp A);\O_{1}\cdot\vd x\hastype 
A}{Id^u}\qquad
\cD_2=\ianc{}{(\GG_{2},x \oftp A);\O_{2}\cdot\vd x\hastype 
A}{Id^u}$$
Then
$$\cE=\ianc{}{(\GG_{1}\cap\GG_{2},x\oftp A);(\O_{1},\O_{2});\cdot\vd x\hastype 
A}{Id^u}$$
\itc 
$$\cD_1=\ianc{}{\GG_{1};\O_{1};x\oftp A\vd x\hastype 
A}{Id^1}\qquad
\cD_2=\ianc{}{\GG_{2};\O_{2};x\oftp A\vd x\hastype 
A}{Id^1}$$
Then
$$\cE=\ianc{}{(\GG_{1}\cap\GG_{2});(\O_{1},\O_{2});x\oftp A\vd x\hastype 
A}{Id^1}$$
\[
\cD_1 =  \ianc{(\Gamma_1, x\oftp A); \Omega_{1}; \Delta_{1}\vd M \hastype B}{\Gamma_1;
\Omega_1; \Delta \vd \lamb{ x^u }{A} M \hastype A \GImp{u}
B}{\GImp{u}I}
\quad
\cD_2 =  \ianc{(\Gamma_2, x\oftp A); \Omega_2; \Delta_{2}\vd M \hastype B}{\Gamma_1;
\Omega_2; \Delta_{2} \vd \lamb{ x^u }{A} M \hastype A \GImp{u}
B}{\GImp{u}I}
\]
\btab
$(\Gamma_1, x\oftp A); \Omega_{1}; \Delta_{1}\vd M \hastype B$\bv
$(\Gamma_2, x\oftp A); \Omega_2; \Delta_{2}\vd M \hastype 
B$\bv
$(\Gamma_1, x\oftp A)\cap (\Gamma_2, x\oftp A); (\Omega_{1},\O_{2}); 
(\Delta_{1},\D_{2})\vd M \hastype B$\bi\\
$(\Gamma_1\cap \GG_{2}, x\oftp A); (\Omega_{1},\O_{2}); 
(\Delta_{1},\D_{2)}\vd M \hastype B$\` By De Morgan\\
$\godt \vd \lamb{ x^u }{A} M \hastype A \GImp{u}
B$\br
\etab
\itc
$$\cD_{1}= \ibnc{(\Gamma_{1}, \Delta_N^{1}); \Omega_{1}; \Delta_M^{1} \vd M \hastype A \RImp 
B}{(\Gamma_{1}, \Delta_M^{1}); \Omega_{1}; \Delta_N^{1} \vd N \hastype 
A}{\Gamma_{1}; 
\Omega_{1}; (\Delta_M^{1}, \Delta_N^{1}) \vd M\ N^1 \hastype B}{\GImp{1}E}
$$
and
$$\cD_{2}= \ibnc{(\Gamma_{2}, \Delta_N^{2}); \Omega_{2}; \Delta_M^{2} \vd M \hastype A \RImp 
B}{(\Gamma_{2}, \Delta_M^{2}); \Omega_{2}; \Delta_N^{2} \vd N \hastype 
A}{\Gamma_{2}; 
\Omega_{2}; (\Delta_M^{2}, \Delta_N^{2}) \vd M\ N^1 \hastype B}{\GImp{1}E}
$$
\btab
$(\Gamma_{1}, \Delta_N^{1}); \Omega_{1}; \Delta_M^{1} \vd M \hastype A \RImp 
B$\bv
$(\Gamma_{2}, \Delta_N^{2}); \Omega_{2}; \Delta_M^{2} \vd M \hastype A \RImp 
B$\bv
$(\Gamma_{1}, \Delta_N^{1})\cap(\Gamma_{2}, \Delta_N^{2}); 
( \Omega_{1},\Omega_{2});(\D_{M}^{1}, \Delta_M^{2}) \vd M \hastype A \RImp 
B$\bi\\
$(\Gamma_{1}, \Delta_M^{1})\cap(\Gamma_{2}, \Delta_M^{2}); 
( \Omega_{1},\Omega_{2});(\D_{N}^{1}, \Delta_N^{2} )\vd N \hastype A$\bi\\
$(\Gamma_{1}\cap \Gamma_{2},  \Delta_N^{1}, \Delta_N^{2}); 
( \Omega_{1},\Omega_{2});(\D_{M}^{1}, \Delta_M^{2}) \vd M \hastype A \RImp 
B$\` By Lemma \ref{le:compat}\\
$(\Gamma_{1}\cap \Gamma_{2}); ( \Omega_{1},\Omega_{2});( \Delta_M^{1},\Delta_M^{2},\D_{N}^{1}, 
\Delta_N^{2}) \vd N \hastype A$
\` By rule
\etab
\enit
($\If$). Similarly by induction on the structure of the derivation of\\
$\godt \vd M\hastype A$.
\end{proof}

%\include{deriv}
{\newcommand{\gm}{(\Gamma,\Delta_i^u);\Omega; }

We introduce two $n$-ary strict application rules, one which 
correspond to the imitation step and the other to projection, which 
will be needed in the proof of Theorem \ref{thm:unif1} and 
\ref{thm:unif2}.

\beq 
\ianc{(\GG,\D^{u}_{i});\O;\D_i^{1} \vd M_{i}\hastype A_{i}\quad 
1\leq i\leq n}{\Gamma;\Omega; \D\vd c\ M_{1}^{1}\dots M_{n}^{1}\hastype 
B}{\RImp E_{n}^{c}} 
\eneq 
where $\GG;\O;\cdot\vd c\ \hastype A_{1}\RImp\dots\RImp A_{n}\RImp B$ and 

\ben
\item 
$\forall x\in\D\,.\,\exists i
:1\leq i\leq n
\,.\,x\in\D_{i}^{1}$.
\item
$\forall i:1\leq i\leq n
\,.\,\D_{i}^{u}\cup\D_{i}^{1}=\D$.
\enen


%proj rule
\beq 
\ianc{(\GG,\D^{u}_{i});\O;\D_i^{1} \vd M_{i}\hastype A_{i}\quad 
1\leq i\leq n}{\Gamma;\Omega; \D\vd y\ M_{1}^{1}\dots M_{n}^{1}\hastype 
B}{\RImp E_{n}^{y}} 
\eneq 
where $\GG';\O;\D'\vd y\ \hastype A_{1}\RImp\dots\RImp A_{n}\RImp B$
such that  $\D'=\{y\}$ or $\D'=\cdot \And y\in\GG'$, 
$\GG'\cup\D'=\GG\cup\D$ and
\ben
\item 
$\forall x\in\D\,.\,\exists i:1\leq i\leq n
\,.\,x\in\D_{i}^{1}$.
\item
$\forall i:1\leq i\leq n
\,.\,\D_{i}^{u}\cup\D_{i}^{1}=\D$.
\enen

We proceed to show that both are invertible and derivable rules. 
%We drop the $\_^{1}$ annotations in the following lemmata:

\begin{Lemma}
\label{le:derivec}
Let $(\GG,\D^u);\O;\cdot\vd c \hastype A_{1}\RImp\dots\RImp 
A_{n}\RImp B$: if $\gm\D_i^1 \vd M_{i}\hastype A_{i}$ for $1\leq 
i\leq j$, then $(\GG,\D^u);\O;\D^1\vd c\ M^{1}_{1}\dots 
M_{j}^{1}\hastype A_{j+1}\RImp\dots\RImp A_{n}\RImp B$, where
\bit
\item[1.] 
$\forall x\in\D^{1}.\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{1}$.
\item[1'.]
$\forall x\in\D^{1}.\neg\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{u}$.
\item[2.]
$\forall i:1\leq i\leq j\,.\,\D_{i}^{u}\cup\D_{i}^{1}=\D^u\cup\D^1$.
\enit
\end{Lemma}
\begin{proof}
By induction on $j$.
\bit
\item[$\mathbf{ j=0}$]
\btab
$(\GG,\D^u);\O;\cdot\vd c \hastype A_{1}\RImp\dots\RImp 
A_{n}\RImp B$ \` By hypothesis
\etab
\item[$\mathbf{j+1}$]
\btab
$\gm\D_i^1\vd M_i\hastype A_i, 1\leq i\leq j$\` By assumption\\
 $(\GG,\D^u);\O;\D^1\vd c\ M^{1}_{1}\dots 
M_{j}^{1}\hastype A_{j+1}\RImp\dots\RImp A_{n}\RImp B$\bi\\     
$(\GG,\D^u_{j+1});\O;\D^1_{j+1}\vd M_{j+1}\hastype A_{j+1}$\bh
%$(\GG,\D^u_{j+1});\O;\D^1_{j+1}\vd M_i\hastype A_i$\` By assumption\\
 $(\GG,\D^u_+);\O;\D^1_+\vd c\ M^{1}_{1}\dots 
M_{j+1}^{1}\hastype A_{j+2}\RImp\dots\RImp A_{n}\RImp B$ and \\
$x\in\D^1_+ \Bimp x\in \D^1_{j+1}\cup\D^1\And
x\in\D^u_+\Bimp x\in\D^u\cap\D^u_{j+1}$ \br \ $\RImp E$
\etab
We now show that the last step satisfy the condition on  rule $\RImp E$:
\bit
\item[1.]
\btab
$x\in\D^1_+$\ba
$ x\in \D^1_{j+1}\cup\D^1$\` As $x\in\D^1_+ \Bimp x\in \D^1_{j+1}\cup\D^1$\\
$ x\in \D^1_{j+1}$\` Case\\
$x\in\D^1_+ \Imp \exists i\oftp 1\leq i\leq j+1\,.\, x\in\D^1_i$\\
$x\in\D^1       $\` Case\\
$x\in\D^1_i$, for some $1\leq i\leq j$\bi\\
$x\in\D^1_+ \Imp \exists i\oftp 1\leq i\leq j\,.\, x\in\D^1_i$
\etab
\item[1'.]
\btab
$x\in\D^u_+$\ba
$x\in\D^u$\` As $x\in\D^u_+\Bimp x\in\D^u\cap\D^u_{j+1}$\\
$x\in\D^u_+\Imp \neg \exists i\oftp 1\leq i\leq j\,.\, x\in\D^1_i$\bi
\etab
\item[2.]
\btab
$\D^1_+\cup\D^u_+= \D^1\cup\D^u$ \br \\
$\forall i\oftp 1\leq i\leq j\,.\, \D^1_i\cup\D^u_i= \D^1\cup\D^u$\bi\\
$\forall i\oftp 1\leq i\leq j\,.\, \D^1_i\cup\D^u_i= \D^1_+\cup\D^u_+$
\` By replacement
\etab
\enit
\enit
\end{proof}

\begin{Lemma}
\label{le:invertec}
Let $(\GG,\D^u);\O;\cdot\vd c \hastype A_{1}\RImp\dots\RImp 
A_{n}\RImp B$: if $(\GG,\D^u);\O;\D^1\vd c\ M^{1}_{1}\dots 
M_{j}^{1}\hastype A_{j+1}\RImp\dots\RImp A_{n}\RImp B$, then 
 $\gm\D_i^1 \vd M_{i}\hastype A_{i}$ for $1\leq 
i\leq j$.
\bit
\item[1.] 
$\forall x\in\D^{1}.\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{1}$.
\item[1'.]
$\forall x\in\D^{1}.\neg\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{u}$.
\item[2.]
$\forall i:1\leq i\leq j\,.\,\D_{i}^{u}\cup\D_{i}^{1}=\D^u\cup\D^1$, where
\enit
\end{Lemma}
\begin{proof}
By induction on $j$.
\bit
\item[$\mathbf{ j=0}$]
\btab
$(\GG,\D^u);\O;\cdot\vd c \hastype A_{1}\RImp\dots\RImp 
A_{n}\RImp B$\` By hypothesis\etab
\item[$\mathbf{ j+1}$]
\btab
$(\GG,\D^u);\O;\D^1\vd c\ M^{1}_{1}\dots 
M_{j+1}^{1}\hastype A_{j+1}\RImp\dots\RImp A_{n}\RImp B$\ba
$(\GG,\D^u_+);\O;\D^1_+\vd c\ M^{1}_{1}\dots 
M_{j}^{1}\hastype A_{j}\RImp\dots\RImp A_{n}\RImp B$\\
$(\GG,\D^u_{j+1});\O;\D^1_{j+1}\vd M_{j+1}\hastype A_{j+1}$ and\\
$x\in\D^1_+ \Bimp x\in \D^1_{j+1}\cup\D^1\And
x\in\D^u_+\Bimp x\in\D^u\cap\D^u_{j+1}$\` By inversion on rule $\RImp E$\\
$\gm\D_i^1 \vd M_{i}\hastype A_{i}$ for $1\leq 
i\leq j$\bi
\etab
since the conditions on the rule are satisfied 
as in the above Lemma \ref{le:derivec}.
\enit
\end{proof}

\begin{Corollary}
\label{co:derivec}
Rule $\RImp E_{n}^c$ is derivable and invertible.
\end{Corollary}
\begin{proof}
For derivability, use Lemma \ref{le:derivec} with $j=n$, $\D^{u}=\cdot,\D^{1}=
\D$; conditions $1.$ and $2.$ are immediately satisfied. Ditto \wrt 
invertibility, using Lemma  \ref{le:invertec}.
\end{proof}

\begin{Lemma}
\label{le:derivey}
Let $(\GG,\D^u)';\O;\D'\vd y\hastype A_{1}\RImp\dots\RImp A_{n}\RImp
B$,
where $\D'=\{y\}$ or $\D'=\cdot \And y\in(\GG,\D^u)'$ and
$(\GG,\D^u)'\cup D'=\GG\cup\D^u\cup \D^1 $.
If $\gm\D_i^1 \vd M_{i}\hastype A_{i}$ for $1\leq 
i\leq j$, then $(\GG,\D^u);\O;\D^1\vd y\ M^{1}_{1}\dots 
M_{j}^{1}\hastype A_{j+1}\RImp\dots\RImp A_{n}\RImp B$  and 
\bit
\item[1.] 
$\forall x\in\D^{1}.\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{1}$.
\item[1'.]
$\forall x\in\D^{1}.\neg\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{u}$.
\item[2.]
$\forall i:1\leq i\leq j\,.\,\D_{i}^{u}\cup\D_{i}^{1}=\D^u\cup\D^1$.
\enit
\end{Lemma}
\begin{proof}
By induction on $j$.
\bit
\item[$\mathbf{ j=0}$]
\btab
$(\GG,\D^u)';\O;\D'\vd y \hastype A_{1}\RImp\dots\RImp 
A_{n}\RImp B$ \` By hypothesis\\
$(\GG,\D^u);\O;\D^1\vd y \hastype A_{1}\RImp\dots\RImp 
A_{n}\RImp B$ \` By the condition
\etab
\item[$\mathbf{j+1}$] Similar to the same case in Lemma \ref{le:derivec}.
\enit
\end{proof}
\begin{Lemma}

\label{le:invertey}
Let $(\GG,\D^u)';\O;\D'\vd y\hastype A_{1}\RImp\dots\RImp A_{n}\RImp
B$,
where $\D'=\{y\}$ or $\D'=\cdot \And y\in(\GG,\D^u)'$ and
$(GG,\D^u)'\cup D'=\GG\cup\D^u\cup \D^1 $. If $(\GG,\D^u);\O;\D^1\vd y\ M^{1}_{1}\dots 
M_{j}^{1}\hastype A_{j+1}\RImp\dots\RImp A_{n}\RImp B$, then 
 $\gm\D_i^1 \vd M_{i}\hastype A_{i}$ for $1\leq 
i\leq j$  and 
\bit
\item[1.] 
$\forall x\in\D^{1}.\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{1}$.
\item[1'.]
$\forall x\in\D^{1}.\neg\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{u}$.
\item[2.]
$\forall i:1\leq i\leq j\,.\,\D_{i}^{u}\cup\D_{i}^{1}=\D^u\cup\D^1$.
\enit
\end{Lemma}
\begin{proof}
By induction on $j$ similarly to Lemma \ref{le:invertec}.
\end{proof}

\begin{Corollary}
\label{co:derivey}
Rule $\RImp E_{n}^y$ is derivable and invertible.
\end{Corollary}
\begin{proof}
As in Corollary \ref{co:derivec}.
\end{proof}


Note how the side conditions in the $n$-ary rules mirrors the proviso 
on the intersection rules.  Firstly note that if $\Phi(x) = 0$ then 
$x\in\O$ which is unchanged in the premises; thus $\forall i:1\leq 
i\leq n.  \Phi_{i}(x) = 0$.  Similarly for $\Phi(x) = u$.  Finally, if 
$\Phi(x) = 1$, the first condition is equal to  $\exists i:1\leq i\leq n.  
\Phi_{i}(x) = 1$, while the requirement $\forall j:1\leq i\leq n, j\neq
i.  \Phi_{i}(x) = u$ is met by Loosening$^1$.
As far as the $FlxRgd^{y}$ rule is concerned the assumption on
$\GG',\D'$ is equivalent to  the additional proviso.
\begin{metanote}
Shall I make it more formal?
\end{metanote}

\begin{Theorem}
\label{thm:unif1}
Let $\GG\vd N_{1}\mcap N_{2}\blip  N\hastype A$.  If $\GG\prv M\in\|N_{1}\|:A$ and 
$\GG\prv M\in\|N_{2}\|:A$, then $\GG\prv M\in\|N\|:A$.
\end{Theorem}
\begin{proof}
% By simultaneous induction on $\cD_{1}::\GG\prv M\in\|N_{1}\|:A$ and 
% $\cD_{2}::\GG\prv M\in\|N_{2}\|:A$.
By induction on the structure of $\cD::\GG\prv N_{1}\mcap N_{2}\blip  N\hastype A$.
\bit
\itc $\cD$ ends in  $\mcap\_FlxFlx$; by Remark \ref{rmrk:compa} and 
the left-to-right direction of Lemma \ref{le:flexunif}.
\itc $\cD$ ends in  $\mcap\_FlxRgd^{c}$:
\btab
$\cD::\GG\vd E\ \Phi\mcap c\ \ol{Q_{n}^{1}} \blip  c\ \Nns$\bh
$\cD_i::\GG\vd E_{i}\ \Phi_i\mcap Q_i \blip  N_i$ for $1\leq i\leq n$
with proviso \bv
$\GG\vd M \in\|c\ \ol{Q_{n}^{1}}\|$\bh
$M\equiv c\ \Mns$ and  $\cD^2_i::\GG\vd M_{i}\in\|Q_{i}\|$ for $1\leq i\leq n$ 
\bv
$\GG\vd c\ \Mns\in\|E\ \Phi\|$\bh
$c\ \Mns\equiv t\ \Phi$, where $t\hastype A$ and $t\equiv \l\Phi\,.\,c\ \tn$ 
for  $\Phi\vd c\ \tn^{1}\hastype P$\bv
$\Phi_{i}\vd t_{i}\hastype A_{i}$\` By inversion on rule $\RImp 
E^{n}_{c}$ (Lemma \ref{le:invertec})\\
$\cD^1_i::\GG\vd M_{i}\in\|E_{i}\ \Phi_{i}\|$ \br\, $grFlx$\\
$\GG\vd M_{i}\in\|N_{i}\|$\bi on $\cD_1,\cD_i^1,\cD_i^2$\\
$\GG\vd c\ \Mns\in\|c\ \Nns\|$\br
\etab
\itc $\cD$ ends in  $\mcap\_FlxRgd^y$. Proceed as above, but using 
Lemma \ref{le:derivey}.

\itc $\cD$ ends in  $\mcap\_Lam$:
\btab
$\GG\vd \lxua N_1\mcap \lxua N_2 \blip  \lxua N$\bh
$\cD::\GG,x\oftp A\prv N_{1}\mcap N_{2}\blip N$\bv
$\GG\prv \lxua M\in\|\lxua N_{1}\|$ \bh
$\cD_1:: \GG,x\oftp A\vd M\in\| N_{1}\|$\bv
$\GG\prv \lxua M\in\|\lxua N_{2}\|$\bh
$\cD_2::\GG,x\oftp A\prv M\in\| N_{2}\|$\bv
$\GG,x\oftp A\prv M\in\| N\|$\bi on $\cD,\cD_1,\cD_2$\\
$\GG\prv \lxua M\in\|\lxua N\|$\br
\etab
\itc $\cD$ ends in  $\mcap\_App$; by a straightforward appeal to the inductive hypothesis 
as in the above case.
\enit
\end{proof}

% start other direction
 
\begin{Theorem}
\label{thm:unif2}
If $\GG\vd N_{1}\mcap N_{2}\blip  N$ and $\GG\prv M\in\|N\|:A$, then $ \GG\prv 
M\in\|N_{1}\|:A$ and $\GG\prv M\in\|N_{2}\|:A$ .
\end{Theorem}
\begin{proof}
By induction on the structure of $\cD::\GG\vd N_{1}\mcap N_{2}\blip  N$.
\bit
\itc $\cD$ ends in $\mcap\_FlxFlx$; by Remark \ref{rmrk:compa} and the 
right-to-left direction of Lemma \ref{le:flexunif}.

\itc $\cD$ ends in  $\mcap\_FlxRgd $.
\btab
$\cD::\GG\vd E\ \Phi\mcap c\ \ol{Q_{n}^{1}} \blip  c\ \Nns$\bh
$\cD_i::\GG\vd E\ \Phi_i\mcap Q_i \blip N_i, 1\leq i\leq n$\bv
$\GG\vd c\ \Mns\in\|c\ \Nns\|$\bh
$\GG\vd M_{i}\in\|Q_{i}\|$ and $\GG\vd M_{i}\in\|E_{i}\ \Phi_{i}\|$
\bi on $\cD_i$\\
$M_{i}\equiv t\ \Phi$, where $t\hastype A$ and $t\equiv \l\Phi\,.\,t_{i}$ 
for  $\Phi_{i}\vd t_{i}\hastype A_{i}$\br $grFlx$\\
$\Phi\vd c\ \ol{t^{1}_{n}}\hastype P$\` By  rule $\RImp 
E^{n}_{c}$ (Lemma \ref{le:derivec})\\
$\GG\vd c\ \Mns\in\|E\ \Phi\|$\br\\
$\GG\vd c\ \Mns\in\|c\ \ol{Q^{1}_{n}}\|$\br
\etab
\itc $\cD$ ends in  $\mcap\_FlxRgd^y$. Proceed as above, but using 
Lemma \ref{le:derivey}.
\itc $\cD$ ends in  $\mcap\_Lam$; by IH as in Theorem \ref{thm:unif1}
\itc $\cD$ ends in  $\mcap\_App$; ditto.
\enit
\end{proof}

\begin{Corollary}[Adequacy of Pattern Intersection]
\label{co:unif}
Fix a signature $\Sigma$.  For simple linear terms $N_1$ and $N_2$ 
 without shared variables such that $\GG \prv N_1 \hastype A$ and $\GG
\prv N_2 \hastype A$,
$\GG\prv 
M\in\|N_{1}\|\hastype A$ and $\GG\prv M\in\|N_{2}\|\hastype A$  iff $\GG\prv 
M\in\|N_1\mbigcap N_2\|\hastype A$.
\end{Corollary}
\begin{proof}
from Theorem \ref{thm:unif1} and \ref{thm:unif2}.
\end{proof}

\smallskip
We now list some basic properties of intersection, which follows from 
Corollary \ref{co:unif} and will be useful in the next Section.

\begin{Corollary}
\label{co:unifpr}
Let $M,N$ be simple linear terms of type $A$:
\bit
\item
$ M\mbigcap M = \{M\} $.
\item
$ M\mbigcap N = N\mbigcap M$.
\enit
\end{Corollary}
% We will overload our notation in the definition of families, indexed 
% by types of complementation and intersection operations between 
% \emph{sets} of terms:
% 
% \beq
% \mmnot_{A}\{M_{1}\mdots M_{m}\} & = & \{N\mid\forall i\in[1,m]  N\in 
% \mnot(M_{i}:A)\}\\
% \{M_{1}\mdots M_{m}\} \mbigcap_{A} \{N_{1}\mdots N_{n}\} & = & 
% \{P\mid \forall  i\in[1,m], \forall  j\in[1,n]\hastype A M\in M_{i}, 
% N\in N_{j}, P \in M\mbigcap N\hastype A\}
% \eneq

\section{The Algebra of Strict Terms}
\label{sec:algebra}
We now extend the intersection and complement operations to \emph{sets} 
of terms, as required by their  finitary nature. 

\begin{Definition}
\label{def:setop} If 
$\cM$ and $\cN$ are sets of \emph{simple} terms of type $A$, define:
\beq      
\cM \mbc \cN & \eqdef & \{Q\mid Q\in
M\mbigcap N\hastype A, M\in \cM, N\in \cN\} 
\vsk
\mna \cM & \eqdef & \bigcap_{M\in\cM} \mmnot(M\hastype A)
\eneq
\end{Definition}

Those operations on set of terms satisfy the same properties that 
`singleton' intersection and complementation do.


\begin{Corollary} [Adequacy of Set Pattern Intersection]
\label{co:setunif}
If $\cN_{1},\cN_{2}$ are sets of simple terms of type $ A$, then 
$\GG\prv M\in\|\cN_{1}\|\hastype A$ and $\GG\prv 
M\in\|\cN_{2}\|\hastype A$ iff $\GG\prv M\in\|\cN_{1}\mbc 
\cN_{2}\|\hastype A$.
\end{Corollary}
\begin{proof}
$\GG\prv M\in\|\cN_{1}\|\hastype A$ and $\GG\prv 
M\in\|\cN_{2}\|\hastype A$ iff there is $N_{1}\in\cN_{1}$ and 
$N_{2}\in\cN_{2}$ such that $\GG\prv M\in\|N_{1}\|\hastype A$ and 
$\GG\prv M\in\|N_{2}\|\hastype A$ iff, by Corollary \ref{co:unif}, 
$\GG\prv M\in\|N_{1}\mbigcap N_{2}\|\hastype A$ iff, by definition 
$\GG\prv M\in\|\cN_{1}\mbc \cN_{2}\|\hastype A$.
\end{proof}

\begin{Corollary}[Set Partition Lemma] 
% For a fixed signature $\Sigma$ let 
Let $ \cN $ be a linear simple term of type $A$:
\label{co:setpart}
\ben
\item (Exhaustivity) $\GG\prv  M\in \| \cN \| \hastype A$ or $\GG\prv  M\in \| 
\mna(\cN) \|\hastype A$.
\item (Disjointness) It is not the case that $\GG\prv  M\in \| N \|\hastype A$ and $\GG\prv  M\in \| \mna(N) \|\hastype A$.
\enen
\end{Corollary}
\begin{proof}\mbox{}
\ben
\item 
By the Partition Lemma,  $\GG\prv  M\in \| \cN \| \hastype A$ 
or $\GG\prv  M\in \| \mmnot(\cN) \|\hastype A$, for every $N\in \cN$. 
Assume $\GG\prv  M\in \| 
N \| \hastype A$; then $\GG\prv  M\in \| \cN \| \hastype A$ and 
finally  $\GG\prv  M\in \| \cN \| \hastype A$ or $\GG\prv  M\in \| 
\mna(\cN) \|\hastype A$. Otherwise assume $\GG\prv  M\in \| 
\mmnot(N) \|\hastype A$, for every $N\in \cN$. Then by Corollary \ref{co:unif}
$\GG\prv  M\in \| 
\mbc_{N\in\cN}\mmnot(N) \|\hastype A$, so by definition $\GG\prv  M\in \| 
\mna(\cN) \|\hastype A$ and finally $\GG\prv  M\in \| \cN \| \hastype A$ or $\GG\prv  M\in \| 
\mna(\cN) \|\hastype A$.
\item
Similarly to the above.
\enen
\end{proof}



%That will allows use to solve `multiple' complement problems, as the 
%ones typically required by clause complementation, see Section \ref{}, 
%\ie:
%$$\|Z\|-\|M_{1}\mdots M_{n}\|$$
%as
%$$ \mna \{M_{1}\mdots M_{n}\}$$
%
%\beq
%\mna\{ \lamb{x}{exp} x, \lamb{x}{exp}lam \ (\lamb 
%{y}{exp} (E\ x)\ y)\} = \\ 
% \mna(\lamb{x}{exp} 
%x)\mbc\mna(\lamb{x}{exp}lam \ (\lamb {y}{exp} (E\ x)\ y)=\\ 
%\{\lamb{x}{exp}lam \ (\lamb {y}{exp} (E\ x)\ y),\lamb{x} {exp} app \ 
%(E_{1}\ x) (E_{2}\ x))\} \mbc\mbox{}\\
%\{\lamb{x}{exp} x,\lamb{x} {exp} app \ 
%(E_{1}\ x) (E_{2}\ x))\}=\\ 
% \{\lamb{x} {exp} app \ (E_{1}\ x) (E_{2}\ 
%x))\}
%\eneq

\begin{metanote} An involution example ? \end{metanote}

This suggests that complementation is involutive.  This should come as 
no surprise, as the Partition Lemma tell us that complementation is 
essentially boolean.  It is in fact possible to organize the set of 
finite sets of simple terms over a given signature say $\mathbf{\cal 
T}_{\Sigma}$ in a boolean algebra $\la \mathbf{\cal 
T}_{\Sigma},\emptyset,\cup,\mbc,\mna\ra$ under set union, patterns 
intersection and complementation.

\begin{Theorem}
\label{thm:algebra}
Consider the algebra  $\la \mathbf{\cal 
T}_{\Sigma},\emptyset,\cup,\mbc,\mna\ra$ under set union, patterns 
intersection and complementation. Then the following holds:
\ben
\item
$\cM\mbc\cM = \cM$.
\item
$\cM\mbc\cN = \cM\mbc\cN$.
\item\label{it:DM}
$\cM\mbc(\cN\cup\cP)= (\cM\mbc\cN)\cup(\cM\mbc\cP)$.
\item
$\cM\mbc(\cN\mbc\cP) = (\cM\mbc\cN)\mbc\cP$.
\item
$\mna\mna \cM=\cM$.
\item
$\mna \mathbf{\cal 
T}_{\Sigma}= \emptyset$.
\item
$\mna \emptyset=\mathbf{\cal 
T}_{\Sigma}$.
\enen
\end{Theorem}
\begin{proof}\mbox{}
\ben
\item
From idempotency of $\mcap$, Corollary \ref{co:unifpr}.
\item
From commutativity of $\mcap$, Corollary \ref{co:unifpr}.  
\item 
Immediate from Corollary \ref{co:setunif} and properties of 
set-theoretic union.
\item 
By induction on $\cP$.  If the latter is empty, the result is 
immediate.  Otherwise
\btab
 $\cM\mbc(\cN\mbc \{M\}\cup\cP)=$\` LHS\\
$\cM\mbc((\cN\mbc\{M\})\cup(\cN\mbc\cP)) =$ \` By $\ref{it:DM}.$\\
$(\cM\mbc(\cN\mbc\{M\}))\cup\cM\mbc(\cN\mbc\cP))=$ \` By $\ref{it:DM}.$\\
$((\cM\mbc\cN)\mbc\{M\})\cup (\cM\mbc\cN)\mbc\cP))=$\bi\\ 
$(\cM\mbc\cN)\mbc ( \{M\}\cup\cP)$  \` By $\ref{it:DM}.$
\etab
\item
$\GG\vd M\in \|\mna\mna \cM\|$ iff by Corollary \ref{co:setpart} 
$\GG\vd M\not\in\|\mna \cM\|$ iff, again by Corollary \ref{co:setpart} 
$\GG\vd M\in \|\cM\|$.
\item
Immediate from Corollary \ref{co:setpart}.
\item
Immediate from Corollary \ref{co:setpart}.
\enen
\end{proof}


\begin{Corollary}
\label{co:boolean}
The algebra $\la \mathbf{\cal T}_{\Sigma},\emptyset,\cup,\mbc,\mna\ra$ 
of simple linear terms is boolean.
\end{Corollary}
\begin{proof}
Theorem \ref{thm:algebra} confirms that the above operators satisfy 
the boolean algebra axioms.
\end{proof}

Corollary \ref{co:boolean} guarantees that any other boolean operation 
is definable: indeed complementation and intersection alone allows to 
define the \emph{relative} complement operation:

\begin{Definition}
\label{def:relcompl}
Given $\cM$ and $\cN$ sets of terms of type $A$:
\beq
\cM - \cN & \eqdef & \cM\mbc (\mna \cN)
\eneq
\end{Definition}

The adequacy of this encoding follows immediately from the Partition 
Lemma and soundness and completeness of intersection.

\begin{Corollary}
$\GG\vd M\in\|\cM\| - |\cN\|$ iff $\GG\vd M\in\|\cM-\cN\|$ .
\end{Corollary}
\begin{proof}
$\GG\vd M\in\|\cM\| - |\cN\|$ iff $\GG\vd M\in \|\cM\|$ and $\GG\vd 
M\not\in\|N\|$ for every $N\in\cN$ iff (Corollary \ref{lemma:part}) 
$\GG\vd M\in \|\cM\|$ and $\GG\vd M\in\|\mmnot(N)\|$ for every 
$N\in\cN$ iff (Corollary \ref{co:unif}) iff $\GG\vd M\in \| \cM\mbc 
(\mna \cN)\|$ iff by definition $\GG\vd M\in\|\cM-\cN\|$.
\end{proof}

% Compare with the way in which 
% \emph{disunification} approaches the relative complement problems: 
% here algebraic operations on sets of terms are translated into 
% conjunctions or disjunctions of (dis)equations whose quantification 
% status is also kept explicit.  Non-deterministic application of a few 
% dozens rules, some addressing identity on finite trees, other 
% (dis)equality in general, eventually turns the given problem into a 
% solved form.  Though a reduction to a significant subset of the 
% disunification rules is likely to be attainable for complement 
% problems, it maybe argued that disunification is not necessarily the 
% master road to the former.  Moreover the \ho case brings in 
% additional complications, as dependencies, which are orthogonal to the 
% hyper-logical structuring that disunification requires.

\begin{metanote} 
Insert a remark (and counter-example) on why $\cup$ must be 
set-theoretic union rather than anti-unification?
\end{metanote}

%\section{Applications}
%\label{sec:appl}
\begin{example}
\label{ex:combi}
We can therefore combine Example \ref{ex:lam} and \ref{ex:etardx}:
\[
\begin{array}{lll}
\mmnot\{(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ 
F),lam(\lamb{x^u}{exp} app\ (E\ x^o) \ x\}
=\\
\quad \mmnot(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ 
F)\mbc \mbox{}\\
\quad \mmnot(lam(\lamb{x^{u}}{exp} app\ (E\ x^{0})\ x ))=\\

\qquad \{ lam\ (\lamb{x^u}{exp} (H\ x^u)),\\
 app\ (app\ H_{1}\ H_{2})\ H_{3}\} \mbc \mbox{}\\

\qquad\{ lam(\lamb{x^u}{exp} app\ (H\ x^1)\ (H'\ x^u)),\\
\qquad lam(\lamb{x^u}{exp} app\ (H\ x^u)\ (app\ (H'\ x^u) \ (H'' x^u)), \\
\qquad lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H'\ x^u\ y^u)),\\
\qquad lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H\ x^u\ y^u) ),\\
\qquad lam(\lamb{x^u}{exp}x),\\
\qquad app\ H\ H'\}=\\

% \qquad \{ lam(\lamb{x^u}{exp} app\ (H\ x^1)\ (H\ x^u),\\
% \quad\qquad\lam(\lamb{x^u}{exp} app\ (H\ x^u)\ (app\ (H_4 x^u) \ (H_5 x^u))), \\
% \quad\qquad lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H_6\ x^u\ y^u)),\\
% \quad\qquad app\ H_1\ H_2,\\
%  \quad\qquad lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H_3\ x^u\ y^u) )\}=\\

\qquad\qquad \{ lam(\lamb{x^u}{exp} app\ (H\ x^1)\ H'\ x^{u}), \\ 
\qquad\qquad  lam(\lamb{x^u}{exp} app\ (H\ x^u)\ (app\ H'\ x^{u} H''\ x^{u})),\\
\qquad\qquad lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H'\ x^u\ y^u))\\
\qquad\qquad  lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H'\ x^u\ y^u)),\\
\qquad \qquad lam(\lamb{x^u}{exp}x),\\
\qquad\qquad app\ ( app\ H\ H') H''\}
\end{array}
\]
\end{example}

\smallskip
Solving relative complement problems is not only a question of
intellectual
curiosity, but it is crucial for our intended application, 
the transformational approach to negation in \lp . This idea aims to by-pass most 
of the problems intrinsic to the negation-as-failure rule by replacing 
negative occurrence of predicates in goals
 by equivalent positive predicated whose definition 
has been mechanically synthesized. This entails
two major steps
\ben
\item
Compute complement of heads of clauses in the predicate definition.
\item 
Bring definition in negation normal form the respecting operational 
semantics.
\enen

While this approach has been investigated for \fo Horn clauses 
\cite{Sato84,Bar90} and CLP programs \cite{Bruscoli94}, the field has
not been explored, at the best of our knowledge, 
\wrt \ho logics and logical frameworks.  For the latter 
this notion of intensional negation is the most adequate, see 
\cite{Momigliano99phd} for a discussion.  

We cannot discuss item $2.$ here. We can suggest its usage via this
 example; consider the 
following facts:
\[
\begin{array}{lll}
betarx & : & isredx(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ F )\\
etarx & : & isredx(lam(\lamb{x^u}{exp} app\ (E\ x^0) \ x)
\end{array}\]

Computing the relative complement as in Example \ref{ex:combi} yields
 the
complementary  facts: 
\[
\begin{array}{lll}
nb1 & : & non\_isredx(lam(\lamb{x^u}{exp} app\ (H\ x^1)\ H'\ x^{u}))\\
nb2 & : & non\_isredx( lam(\lamb{x^u}{exp} app\ (H\ x^u)\
 (app\ H_4\ x^{u} H_5\ x^{u})))\\
nb3 & : & non\_isredx(lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H_6\ x^u\ y^u))))\\
nb4 & : & non\_isredx(lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H_3\ x^u\ 
y^u) ))\\
nbr & : & non\_isredx(lam(\lamb{x^u}{exp}x))\\ 
nb6 & : & non\_isredx( app\ (app\ H_{1}\ H_{2})\ H_{3}\ )
\end{array}\]


% \section{Conclusion}
% \label{sec:concl}
% We have shown that the complement of linear pattern is a finite set 
% of simple terms in the strict $\lambda$-calculus.  Moreover, 
% unification of simple terms is decidable and leads to a finite set of 
% most general unifiers.  We will consider two orthogonal follow-up to 
% this work.  First, an extension to the dependent types case, so as to 
% endow languages as Twelf \cite{Schurmann98cade} of a logically founded notion of 
% negation in the sense of \cite{Bar90}.  Second we will address the 
% general case of complementation and unification in the strict 
% $\lambda$-calculus; this is likely to be useful in linear logical 
% frameworks as \em{LLF} \cite{Cervesato96lics}.
