\slidetitle{Clause Complement}
\bit 
\item Then, the complement of {\tt
  linapp} does not problematic: 
application in not linear if either the first element or the second in
not linear.  
\beq
\neg linapp & : & \neg linear(app\ E_1\ E_2)\\
& & \qquad\If  \neg linear(E_1)\Or\neg linear(E_2).  
\eneq
% \item
% A lambda expression is not linear first it is not linear in its first argument:
%  \beq
% \neg linlam1& : & \neg linear(lam( \lx E\ x))\\
% & & \qquad\If \neg linx(\lx E\ x).  
% \eneq
% \item 
% Secondly, 
\item Complementing a hypothetical and parametric clause :
need a way to complement \emph{dynamic assumptions}.

\item By definition assumption are parametric in some eigenvariable

\item We can replicate clause complementation by pivoting on that parameter
\item We \emph{augment} a hypothetical clause with the negation of its
  possible assumption via a source-to-source transformation.
\item This additional structure in a predicate definition in order
to completely determine the provability and failure of goals which
mention \emph{parameters}

\item we first augment the clause \texttt{linxlm}: 
\beq
\ald(linxlm)& : &linx(\lx lam(\ly E\ x\ y))\\
& & \qquad\If (\PI{y}{exp} \neg linx(\lx y)\Imp linx (\lx E\ x\ y)).
\eneq so that, by complementation, we obtain \beq
\neg \ald(linxlm)& : &\neg linx(\lx lam(\ly E\ x\ y))\\
& & \qquad\If (\PI{y}{exp} \neg linx(\lx y)\Imp \neg linx (\lx E\ x\ 
y)).  \eneq
\enit
\mends
\begin{slide}
\bit
\item
This in turn 
entails that we have to make sure that during execution, whenever an
assumption is made, it remains in the fragment we have isolated.
Technically, we proceed as follows:2
\begin{itemize}
\item We extract from the static definition of a predicate the general
  `template' of a legal assumption.
\item We require dynamic assumptions to conform to this template.
\enit
\enit
\mends







