% Then its completion {\em comp(p)} is, for new $\Xn$
% \beq
% \forall \Xn .p(\Xn) \Imp \BOr\limits^m_{i=1}
% \exists \vY (\BAnd\limits^n_{j = 1} (x_j\ebe t_{i,j}[\vY]) \And G_{i}[\vY])\\
% \forall \Xn . Not(p(\Xn))\Imp \BAnd\limits^m_{i=1}
% \all \vY (\BOr\limits^n_{j = 1} (x_j\nebe t_{i,j}[\vY]) \And Not(aug(G_{i}[\vY])))
% \eneq
% which can be abbreviated in the definiens formula
% \beq
% dp & :& \forall \Xn. p(\Xn) \If D[\vx]\\
% not(dp) & :& Not(\forall \Xn. p(\Xn) \If Not(aug(D[\vx])))
% \eneq

\subsection{General case}

We start with a very basic example: identity of (untyped) lambda terms 
modulo $\alpha$-conversion: this is coded in the following:
\beq
eqapp &:& eq\ (app\ E_{1}E_{2}) (app\ F_{1}F_{2})\If  eq\ (E_{1}F_{1}) 
\If eq\ (E_{2}F_{2})\\
eqlam &:& eq\ (lam\ E) (lam\ F)\If \Pi xy : exp .\ eq\ (x\ y) \Imp eq\ (E\ x)(F\ y)
\eneq

To determine when two abstractions, say $lam\ ( \lx x)$ and $lam\ 
(\lx (app\ E_{1}x E_{2}x))$ are different, we must be able to tell, inside the 
meta-language, that a parameter is different from any other term. While 
this property holds for the meta-theory of the meta-language, it 
cannot be tested unless we introduce explicit \emph{disequations} 
(modulo $\beta\eta$). Hence the program

\[
\begin{array}{llll}
\neg eqappi &:& \neg eq\ (app\ E_{1}E_{2}) \ (app\ F_{1}F_{2})\If  
\neg eq\ (E_{1}F_{1}) \Or \neg eq\ (E_{2}F_{2})\\
\neg eqlam &:& \neg eq\ (lam\ E) (lam\ F)\If \Pi xy : exp \\
 & &(\Pi E^{'}F^{'}: exp.\ (\neg  eq E^{'} y \If x \nebe E^{'}) \And
 (\neg eq\ F^{'} y \If y  \nebe F^{'}))\\
  & &  \Imp  eq\ (x\ y) \Imp \neg eq\ (E\ x)(F\ y)
\end{array}
\]

To complement parametrical clauses we therefore need to extend the 
$Not$ algorithm to treat parameters: operationally, \fo parameters act 
like constants with the constraint that they must be new \wrt the 
current signature.  Since, by standard undecidability results, it is 
not possible to foresee how many parameters will be introduced for a 
given query, the complement of parametric assumptions cannot be 
computed at compile-time.  We thus introduce the notion of 
\emph{constrained complement} for parameters in \fo terms\footnote{can 
be introduced for term in general, without parameters}: remember, terms are 
linear.

\begin{Definition}[Constrained complement]
\beq
Not(\Pi \xn:\ol{A_{n}} . M[\xn]) = 
\Pi \xn : \ol{A_{n}}.\ \BAnd \limits^n_{i = 1} (\Pi E_{i}. \neg M[x_{1}\mdots x_{i-1}, 
E_{i},x_{i+1}\mdots x_n] \If E_{i}\nebe x_{i})
\eneq
where the $E_{i}$'s are fresh logical variables.
\end{Definition}

The simplest way to operationally interpret disequalities is probably not 
to  feed them to a separate disunification module but to incorporate them 
as additional constraints to the current unification problem in the 
now experimented constraint approach to \ho pre-unification \cite{SP9?,Pfe91}. 


Consider now the typing example, namely the case for functions and its 
complement: we may observe that typically it will be called with the 
first argument instantiated while the second is in `don't mind' mode. 
We then take the complement of $of\ x\ T_{1}$ according to its 
calling mode, that is, keeping $x$ fixed and constraining $T_{1}$:

\[
\begin{array}{lllll}
oflam &:& of (lam\ E) \ (T_{1} \supset T_{2}) \If \Pi x : exp .\ of\ x\ T_{1} \Imp of 
(E\ x) T_{2}\\
\\
\neg oflam &:& \neg of (lam\ E) \ (T_{1} \supset T_{2}) \If\\
& &  \Pi x : exp (\Pi : tp. \ \neg of\ x\ T \If T \nebe T_{1})\\
& &   \Imp  of\ x\ T_{1} \Imp \neg of (E\ x) T_{2}
\end{array}
\]

\begin{Definition}[Constrained  moded complement]
Let an atom $(p\ \Mm\  \Nn)$ have type $\Am\Imp\Bn \Imp type$ 
and mode $ p\ (+\Mm)\ (*\Nn)$: if $mode(p)=m$ we denote with 
$Not_{m}(p)$ the \emph{constrained moded complement} of  $p$ according 
to $m$.
\beq
Not_{m}(p\ (+\Mm)\ (*\Nn)) = 
\BAnd \limits^n_{i = 1} (\Pi E_i. \neg p\ \Mm \ N_{1}\mdots 
N_{i-1}, N_{i},N_{i+1}\mdots N_{n} \If E_{i}\nebe x_{i})
\eneq
\end{Definition}


\begin{Definition}[Moded Augmentation]
For a program $\cP$, let 
$m : p (\l \xn: \ol{A_{n}} . M[\Ep\ \xn]) \If  G \If (\Pi \zp :  
\ol{A'_{p}}. q\ (\l \xn: \ol{A_{n}}.  q\ ([\Ep\ \xn\ z])))$
 be s.t.\
\bit
\item
$mode(p)=m$
\item
$m$ is a second-order $\Pi$-allowed recursive clause thru $q$ in $\cP$:
\item
 $E_{i} : B_{i}$ and $\omicron(B_{i}) = 2$ for all $i\in 1..p$
\item
  $A'_{i}\leq B_{i}$.
\enit
Then define 
\beq
aug(m) &:& p(\l \xn: \ol{A_{n}} . M[\Ep\ \xn]) \If  G \\
& & \If Not_{m}(\Pi \zp :  
\ol{A'_{p}} q\ (\zp)) \Imp q\ (\l \xn: \ol{A_{n}}.\  q\ ([\Ep\ \xn\ z]))
\eneq
 Define $aug(\cP)$ as the augmentation of every clause in $\cP$.
\end{Definition}

\subsubsection{Example: normal natural deductions}

Fill in code