\section{Refinements}
\label{sec:ref}

In the following sections we will move towards an operational
semantics for our language.


% \subsection{The Algebra of Clause Complementation}
% \label{ssec:ccalgebra}

% Similarly to what we did for term complementation, we show that we can
% organize  programs in a boolean algebra under $\la
% \And,\tensor,\mnotd,\top,\perp\ra$, generalizing the approach in \cite{MP90}.
% \bmeta fill in \emeta

\subsection{More on Termination}
\label{ssec:ccterm}

We prove that clause complementation preserve
termination, so that a negative program can be used as decision
procedure if so is its positive counterpart. First some
preliminaries: call $[R]$ the stable and transitive closure of the
subgoal ordering defined in Figure \ref{fig:termgraph}. Define
$\mnot(R)$ as follows:
\beq
\mnot(\cdot) & = & \cdot\\
\mnot(R,G_1\less G_2) & = & \mnot(R),\mnotg(G_1)\less\mnotg(G_2)
\eneq
Observe that, by the restriction to clauses of the form $Q\If G$, it
is sufficient to consider only goal complementation. It is clear that
negation is preserved under relation union, that is:
\beq
\mnot(R_1,R_2) & = & \mnot(R_1),\mnot(R_2)
\eneq
We will also need the following technical Lemma, stating that goal
complementation commutes with substitution:
\begin{Lemma}
\label{le:notgtheta}
For any substitution $\q$, $\mnotg([\q] G) = [\q] \mnotg(G)$.
\end{Lemma}
\begin{proof}
  By a simple induction on the structure of $\mnotg(G)$.
\end{proof}

\newcommand{\qq}{[\theta]}
%Next we show that
\begin{Lemma}
\label{le:notwf}
If $[R]$ is well-founded, so is $[\mnot(R)]$.
\end{Lemma}
\begin{proof}
  Suppose $[\mnot(R])$ is not well-founded. Then there is an infinite
  descending chain $\dots\less\qq G_i\less\dots\less\qq G_2\less\qq
  G_1$. By definition of $\mnot(R)$ there are $G'_i$ such that
  $\mnotg(G'_i)=G_i$ and that $G'_i\less G'_i-1\in R$ for
  $i\in\omega$. Since by Lemma \ref{le:notgtheta} $\mnotg([\q] G_i) =
  [\q] \mnotg(G_i)$, then $[R]$ allows an infinite descending chain
  $\dots\less\qq G'_i\less\dots\less\qq G'_2\less\qq G'_1$,
  impossible.
\end{proof}

The final piece is to show that the relation induced by the complement
of a program is the complement of the relation induced by the program
itself:
\begin{Lemma}
\label{le:ccterm}
\mbox{}
\ben
\item If $\pi::D\yd R$ then $\mnotd(D)\yd\mnot(R)$.
\item If $\gamma::\GG\vd G\yg R$ then $\GG\vd\mnotg(G)\yg\mnot(R)$.
\enen
\end{Lemma}
\begin{proof}
By induction on the structure of the given derivations. We prove some
selected cases:
\bit
\itc $\pi::\top\yd \cdot$; $\mnotd(\top)=\perp\yd\cdot=\mnot(\cdot)$.
\itc $\pi$ ends in $(q\ \vM\If G)\yd R,G\less q\ \vM$:
\btab
$\cdot\vd G\yg R$\bs
$\cdot\vd\mnotg(G)\yg\mnot(R)$\bi $2$\\
$\BAnd_{\vN\in\mnot(\vM)}\Pi( \neg (q\ \vN)) \And  \neg q\ \vM\If\mnotg(
G)\yd\mnot(R),\mnot(G)\less\neg q\ \vM$\\
\br\\
$\mnotd( q\ \vM\If G) \yd\mnot(R,G\less q\ \vM)$\br
\etab
\itc $\gamma::Q\yg \cdot$; $\mnotd(Q)=\neg Q\yd\cdot=\mnot(\cdot)$.
\itc $\gamma$ ends in $\GG\vd G_1\And G_2\yg R_1, R_2,G_1\less G_1\And G_2,G_2\less G_1\And G_2$:
\btab
$\GG\vd G_1 \yg R_1$ and $\GG\vd G_2\yg R_2$\bs
$\GG\vd \mnotg(G_1) \yg \mnot(R_1)$ and $\GG\vd \mnotg(G_2)\yg \mnotg(R_2)$\bi
$2$\\
$\GG\vd \mnot(G_1)\Or \mnotg(G_2)\yg \mnot( R_1), \mnot(R_2)$,\\
$\qquad\mnotg(G_1)\less \mnotg(G_1)\Or
\mnotg(G_2),\mnotg(G_2)\less \mnotg(G_1)\Or \mnotg(G_2)$\br\\
$\GG\vd\mnot(G_1\And G_2)\yg \mnot( R_1), \mnot(R_2),$\\
$\qquad\mnotg(G_1)\less \mnotg(G_1\And
G_2),\mnotg(G_2)\less \mnot(G_1\And G_2)$\br\\
$\GG\vd\mnot(G_1\And G_2)\yg \mnot( R_1, R_2,G_1\less G_1\And
G_2,G_2\less G_1\And G_2)$\br
\etab
\enit
\end{proof}

\begin{Corollary}
  If $\cP$ is terminating, so is $\mnotd(\cP)$.
\end{Corollary}
\begin{proof}
  By definition, $\cP$ is terminating if $\cP\yd R$ and $[R]$ is
  well-founded: by Lemma \ref{le:ccterm} $\mnotd(\cP)\yd\mnot(R)$ and
  by Lemma \ref{le:notwf} $[\mnot(R)]$ is well-founded. Thus
  $\mnotd(\cP)$ is terminating.
\end{proof}


\subsection{Elimination of $\tensor$}
\renewcommand{\vN}{\vec{N}}
\label{ssec:tensor}

We now show how to eliminate the $\tensor$ operator preserving 
provability; this will recover uniformity in proof-search.  
We generalize the approach in 
\cite{Bar90}, where the operation was defined as follows:
for $m1: Q_{1}\If G_{1}$ and  $m2: Q_{2}\If G_{2}$:
\beq
m1 \tensor m2 & = &  \q(Q_{1}\If G_1\And G_2) \quad\mbox{{\rm where }} 
\q = mgu(Q_{1},Q_{2}) 
\eneq
As we remarked earlier, the $\tensor$ operator was introduced to
preserve the duality between conjunction and disjunction in clauses.
Its use is limited to clauses in the same predicate definition and
therefore it can be eliminated simulating unification in the
definition.  Yet, the strict \ho unification problem is quite complex
and even more so complicated by the mixed quantifier structure of HHF.
Moreover, we have already in our language parameter (dis)equations
introduced by the augmentation procedure, as well as variable-variable
(dis)equations stemming from left-linearization.  We thus choose to
compile our source into an intermediate language which makes
unification problems explicit as simple equational problems in the
style of the unification logic introduced in \cite{Pfenning91lf}.  We
can then perform constraint simplification
as used in \emph{Elf} \cite{Pfenning89lics} and \emph{Twelf}
\cite{Schurmann98cade}.

% \newcommand{\eprv}{\stackrel{\prv}{\sim}}
% \newcommand{\enprv}{\stackrel{\nprv}{\sim}}
% \smallskip

% We introduce a notion of \emph{operational equivalence} \wrt 
% provability.

% \begin{Definition}[Operational Equivalence]
% \label{def:opeq}
% We say that $\cP_{1}$ and $\cP_{2}$ are \emph{operationally equivalent \wrt 
% provability}, denoted $\cP_{1}\eprv \cP_{2}$, iff, for any goal $G$ we 
% have $\ga\prv_{\cP_{1}} G$ iff $\ga\prv_{\cP_{2}} G$.

% \end{Definition}

We adapt the \emph{residuation} technique used in \cite{Pfenning94un}
to compile immediate implication into resolution.  We define the
judgment $D_{1}\tensor D_{2} \setminus D$ in Figure \ref{fig:otimes}
by induction on (normalized) $D_{1}$, with the intended meaning of
`$D_{1}\tensor D_{2}$ compiles to $D$': As usual, we add the rules
symmetric to $\tensor\top,\tensor\Pi,\tensor\And$.  Note that
residuation is undefined for clauses with different heads; yet we
could make the judgment total by agreeing to compile them to $\top$.

% \begin{Lemma}
% \label{le:imm-eq}
% The following are valid rules of inference:
% $$\ianc{\ga\sp q\ \vN_{1}\imm Q\quad \vN_{1}\eqd \vN_{2}}{\ga\sp q\ \vN_{2}\imm Q}{\imm\eqd}
% \qquad
% \ianc{\gna\fp q\ \vN_{1}\nimm Q\quad \vN_{1}\neqd \vN_{2}}{\ga\fp q\ \vN_{2}\nimm Q}{\imm\neqd}
% $$
% \end{Lemma}
% \begin{proof}
% It will be trivial once we specify the equality rules.
% \end{proof}

\begin{figure}
\[
\begin{array}{c}
\ianc{}{\top\tensor D \setminus \top}{\tensor\top}
\vsk
\ianc{}{(q\ \vN_{1}\If G_{1})\tensor  (q\ \vN_{2}\If G_{2}) \setminus
q\ \vN_{1}\If (\vN_{1}\eqd \vN_{2}) \And G_{1}\And G_{2}}{\tensor{\rm 
atm}}\vsk
\qquad
\ianc{([u/x] D_{1})\tensor D_{2}\setminus[u/x]D}{(\PIXA D_{1})\tensor 
D_{2}\setminus \PIXA  D}{\tensor\Pi}\vsk
\ianc{D_{1}\tensor D_{2}\setminus D\quad D'_{1}\tensor D_{2}\setminus D'}
{(D_{1}\And D'_{1})\tensor D_{2}\setminus D\And D'}{\tensor\And}
\end{array}
\]
\caption{$\tensor$-Elimination: $D_{1}\tensor D_{2}\setminus D$}
\label{fig:otimes}
\end{figure}

\begin{Example}
\label{ex:closedatensor}
Continuing Example \ref{ex:closed},
recall that:
\beq
\lefteqn{\mnotd(cloz)=}\\
& & \PI{F}{exp}\neg closed\ (lam\ F)\And \PI{F_1,F_2}{exp}
\neg closed\ (app\ F_{1} \ F_{2}).\\
\lefteqn{\mnotd(clolam)=}\\
&& \neg closed\ z\And  \PI{F_1,F_2}{exp}\neg closed\
               (app\ F_{1} \ F_{2})\And  \\ 
&& \PI{E}{exp} \neg closed\ (lam\ E) \If \PI {x } {exp}\ (closed\ x \Imp \neg closed\ 
 (E\ x)).
\eneq
Let us compute $\mnotd (cloz) \otimes \mnotd (clolam)\setminus D$:
\[\begin{array}{l}
 \PI{F}{exp}\neg closed\ (lam\ F)\If (lam\ F)\eqd z\And\mbox{}\\
 \PI{F,F_1,F_2}{exp}\neg closed\ (lam\ F)\If (lam\ F)\eqd (app\ F_1\
 F_2)\And\mbox{}\\
\PI{E}{exp}\neg closed\ (lam\ E) \If (\PI {x } {exp}\ closed\ x \Imp
 \neg closed\ (E\ x))\And\mbox{}\\
 \PI{F_1,F_2}{exp} \neg closed\ (app\ F_{1} \ F_{2})\If (app\ F_{1} \
 F_{2})\eqd z\And\mbox{}\\
 \PI{F,F_1,F_2}{exp} \neg closed\ (app\ F_{1} \ F_{2})\If (app\ F_{1} \
 F_{2})\eqd (lam\ F)\And\mbox{}\\
 \PI{F_1,F_2}{exp} \neg closed\ (app\ F_{1} \ F_{2}).
\end{array}\]

Note that only the third and last clause are satisfiable.
\end{Example}

The following lemma guarantees that compilation preserves immediate 
entailment:

\begin{Lemma}
\label{le:te-tim}
Let $ D_{1}\tensor D_{2}\setminus D$:  $\ga\vd D_1\tensor D_{2}
\imm Q$ iff $\ga\vd D\imm Q$.
\end{Lemma}
\begin{proof}
($\Imp$). By induction on the structure of $\pi:: D_{1}\tensor D_{2}\setminus D$.
\bit
\itc $\pi$ ends in $\setminus\top$. Trivially true.
\itc
$$\pi=\ianc{}{(q\ \vN_{1}\If G_{1})\tensor  (q\ \vN_{2}\If G_{2}) \setminus
q\ \vN_{1}\If (\vN_{1}\eqd \vN_{2}) \And G_{1}\And G_{2}}{\tensor{\rm 
atm}}$$
\btab
$\ga\sp (q\ \vN_{1}\If 
G_{1})\tensor (q\ \vN_{2}\If G_{2})\imm q\ \vN$\bh
$\ga\sp q\ \vN_{1}\If 
G_{1}\imm q\ \vN$ and $ q\ \vN_{2}\If G_{2}\imm q\ \vN$\bv
$\ga\sp\vN_1\eqd \vN$ and $\ga\sp G_1$\bv
 $\ga\sp\vN_2\eqd\vN$ and $\ga\sp G_2$\bv
$\ga\sp \vN_1\eqd\vN_2$\`By replacement\\
 $\ga\sp q\ \vN_{1}\If (\vN_{1}\eqd \vN_{2}) \And G_{1}\And 
G_{2}\imm q\ \vN$\br(s)
\etab
\itc $\pi$ ends in $\tensor\And,\tensor\Pi$: by an immediate
appeal to the IH.
% Case: 
% $$\ianc{([t/x] D_{1})\tensor D_{2}\setminus [t/x]D}{(\PIXA D_{1})\tensor 
% D_{2}\setminus \PIXA  D}\tensor\Pi}$$
% By inversion $([t/x] D_{1})\tensor D_{2} \setminus[t/x]D$ and $\ga\sp 
% [t/x]D\imm Q$ which is equivalent by IH to $\ga\sp [t/x]D_{1}\tensor 
% D_{2}\imm Q$ iff $\ga\sp [t/x]D_{1}\imm Q$ and $\ga\sp D_{2}\imm Q$ 
% iff $\ga\sp (\PIXA D_{1})\tensor D_{2}\imm Q$.
\enit
($\If$): completely analogous.
\end{proof}
We remark that, using again terminating programs, the above Lemma
covers immediate denial as well.
% The following guarantees that compilation preserves 
% Note that we have to take into account the meta-level universal 
% quantification on terms brought in by the $I^{\nprv}_{\Pi}$ rule.

% \begin{Lemma}
% \label{le:te-nimm}
% For all $\q, \ \q D_{1}\tensor D_{2}\setminus D$ and $\q D\nimm Q$ iff 
% $\q D_{1}\tensor D_{2} \nimm Q$.  
% \end{Lemma}
% \begin{proof}
% By induction on $D_{1}$.  We avoid mentioning substitutions when they 
% are immaterial and show only some significant cases in the $\Imp$ 
% direction, the converse following the same lines.
% \bit
% \item
% Case:
% $$\ianc{}{\top\tensor D \setminus \top}\tensor\top}$$
% $\ga\sp\top\nimm Q$ obviously entails   $\ga\sp\top\tensor D\nimm Q$.
% \item
% Case:
% $$\ianc{}{(q\ \vN_{1}\If G_{1})\tensor  (q\ \vN_{2}\If G_{2}) \setminus
% q\ \vN_{1}\If \vN_{1}\eqd \vN_{2} \And G_{1}\And G_{2}}\tensor{\rm 
% atm}}$$
% Assume $\ga\fp q\ \vN_{1}\If \vN_{1}\eqd \vN_{2} \And G_{1}\And 
% G_{2}\nimm Q$.  Then either $\ga\fp q\ \vN_{1}\nimm Q$ or $\ga\fp 
% \vN_{1}\eqd \vN_{2} \And G_{1}\And G_{2}$. The first case entails
% $\ga\fp q\ \vN_{1}\nimm Q$ or $\ga\fp G_{1}$ which implies 
% $\ga\fp q\ \vN_{1}\If G_{1}\nimm Q$ and finally 
% $\ga\fp q\ \vN_{1}\If G_{1}\tensor q\ \vN_{2}\If G_{2}\nimm Q$. The 
% second horn splits into three subcases:
% \ben
% \item
% $\vN_{1}\neqd \vN_{2}$. By Lemma \ref{le:imm-eq} $\ga\fp q\ 
% \vN_{2}\nimm Q$ which implies $\ga\fp q\ \vN_{2}\If G_{2}\nimm Q$ and finally 
% $\ga\fp q\ \vN_{1}\If G_{1}\tensor q\ \vN_{2}\If G_{2}\nimm Q$. 
% \item
% $\ga\fp G_{2}$ implies $\ga\fp q\ \vN_{2}\If G_{2}\nimm Q$ and finally 
% $\ga\fp q\ \vN_{1}\If G_{1}\tensor q\ \vN_{2}\If G_{2}\nimm Q$. 
% \item
% $\ga\fp G_{1}$ implies $\ga\fp q\ \vN_{1}\If G_{1}\nimm Q$ and finally 
% $\ga\fp q\ \vN_{1}\If G_{1}\tensor q\ \vN_{2}\If G_{2}\nimm Q$. 
% \enen
% \item
% Case:
% $$\ianc{([t/x] D_{1})\tensor D_{2}\setminus [t/x] D}{(\PIXA D_{1})\tensor 
% D_{2}\setminus \PIXA  D}\tensor\Pi}$$
% From $([t/x] D_{1})\tensor D_{2}\setminus [t/x] D$ and $\ga\sp \q 
% D\nimm Q$ by IH we infer $\ga\sp \q D\tensor D_{2}\nimm Q$, 
% equivalent to $\ga\sp \q D\nimm Q$ or $ D_{2}\nimm Q$ which implies 
% $(\PIXA D_{1})\tensor D_{2}\nimm Q$. 
% \enit
% \end{proof}
\newcommand{\ted}[1]{ (#1)^{\tensor_D} }
\newcommand{\teg}[1]{ (#1)^{\tensor_G} }
\newcommand{\PT}{\tensor\cP}

We now extend the effect of the above compilation on a program:
\begin{Definition}
\label{def:tensorpro}
\[\begin{array}{rcll}
 \ted{\top} & = & \top\\
\ted{\perp} & = & \perp\\
\ted{Q\If G} & = & Q\If \teg{G}\\
\ted{ D_{1}\And D_{2} } & = & \ted{D_{1}}\And \ted{D_{2}} \\
\ted{\PI{x}{A} D} & = & \PIXA  \ted{D} \\
\ted{D_{1}\tensor D_{2}} & = &  D  
& \mbox{\textrm{where }} \ted{D_{1}}\tensor \ted{D_{2}} \setminus D\\
\teg{X} & = & X & X\in\{\top,\perp,Q,\mbox{(dis)eq}\}\\
\teg{G_1\And G_2} & = & \teg{G_1}\And \teg{G_2}\\
\teg{G_1\Or G_2} & = & \teg{G_1}\Or \teg{G_2}\\
\teg{D\Imp G} & = & \ted{D}\Imp\teg{G}\\
\teg{\PIXA G} & = & \PIXA\teg{G}\\
\teg{\exa G} & = & \exa\teg{G}
\end{array}\]
\end{Definition}


\begin{Theorem}[Elimination of $\tensor$]
\label{thm:te-imm}
\mbox{} 
\ben
\item
 $\cS :: \ga\sp G$ iff $\tensor \cS :: \GG;\ted{\cD}\sp\teg{ G}$;
\item
 ${\cal I} :: \ga\sp D \imm Q$ iff $\tensor {\cal I} :: \GG;\ted{\cD}\sp
\ted{D} \imm Q$.
\enen
\end{Theorem}
\begin{proof}
($\Imp$). By a straightforward mutual induction on the structure of the given
derivations: we show the crucial case.
\bit
\itc $\cal I$ ends in $\imm\tensor$:
\btab
$\ga\sp D_1\imm Q$ and $\ga\sp D_2\imm Q$\bs
$\GG;\ted{\cD}\sp \ted{D_1}\imm Q$ and $\GG;\ted{\cD}\sp \ted{D_2}\imm
Q$\bi $2$\\
$\GG;\ted{\cD}\sp\ted{D_1}\tensor \ted{D_2}\imm Q$\br $\imm\tensor$\\
$\GG;\ted{\cD}\sp\ted{D_1\tensor D_2}\imm Q$\` By Lemma \ref{le:te-tim}
\etab
\enit
($\If$). Similarly.
\end{proof}
The same remark \wrt termination applies.
%\begin{Proposition}
% \label{ppn:te-nimm}
% $\cP \enprv \PT$.
% \end{Proposition}
% \begin{proof}
% We need to show $\ga\nprv_{\cP} G$ iff $\ga\nprv_{\PT} G$. We 
% generalize this to:
% \ben
% \item
% $\SM :: \ga\fp G$ iff $\tensor \SM :: \ga\nprv_{\PT} G$;
% \item
% For every $\q$, $\IM :: \ga\fp \q(def(Q)) \nimm Q$ iff $\tensor \IM :: \ga\nprv_{\PT} 
% \q(def(Q)) \nimm Q$.
% \enen
% The proof is a straightforward mutual induction on the structure of the 
% derivation using Lemma \ref{le:te-nimm}.
% \end{proof}

% From the above propositions, we have the soundness and completeness 
% of the compilation:

% \begin{Corollary}
% \label{co:te-ti}
% $\cP \sim \PT$.
% \end{Corollary}

\subsection{Constraint Simplification}
\label{sec:simplify}

In this section we hint on how to bring clauses stemming from
complementation into their final format by simplifying, whenever
possible, the disequation introduced by the $\mnota\Imp$ rule. In our
language, two forms of disequations cannot be immediately solved and
must be postponed as constraints:
\begin{enumerate}
\item Shallow parameter expression/existential variable disequations.
\item Rigid term/existential variable disequations, stemming from
  left-linearization.
\end{enumerate}

What can be solved instead is:
\begin{itemize}
\item The rest of existential variable-rigid term disequations by
  computing the complement of the latter.
\item Unsatisfiable variable-variable disequations, by removal.
%\item Removing useless augmentation clauses brought in by subordination.
\end{itemize}

In a final pass we may also:
\begin{itemize}
\item Remove irrelevant occurrences of $\top$.
%\item Remove failing clauses, \ie with $\perp$ in the body.
\item Hide the irrelevant augmentation in the final negative clause.
\item If so desired and when possible, bring clauses to the `core'
  languages syntax, as in LF.
\end{itemize}



\begin{Example}
\label{ex:closedfinal} 
Continuing Example \ref{ex:closed} and \ref{ex:closedatensor} the final
definition of $\neg$\texttt{closed} is:
\beq
oplam &: & \PI{ E}{exp} open\ (lam\ E)  \If \PI {x } {exp}\ open\ (E\ x).\\
opap1 &: & \PI{ E_{1},E_{2}}{exp} open\ (app\ E_{1} \ E_{2}) \If open\
E_1.\\
opap2 &: & \PI{ E_{1},E_{2}}{exp} open\ (app\ E_{1} \ E_{2}) \If open\ E_{2}.
\eneq
where we have solved all disequations, which are in this case trivial
ground-ground checks,  hidden the irrelevant assumption $closed\ x$ and
renamed `$\neg$\texttt{closed}' into \texttt{open}.
\end{Example}

\begin{Example}
\label{ex:linearfinal} 
The final definition of \texttt{$\neg$linear} and in turn \texttt{$\neg$linx} is:
\beq
\neg linapp1 & : & \neg linear(app\ E_1\ E_2)\If \neg linear(E_1).\\
\neg linapp2 & : & \neg linear(app\ E_1\ E_2)\If  \neg linear(E_2).\\
\neg linlam1& : & \neg linear(lam\ \lx E\ x)\If \neg linx( \lx E\ x)\\.
\neg linlam2& : & \neg linear(lam\ \lx E\ x)\If (\PI{y}{exp} (\neg linx(\lx y)\And linear(y))\Imp\neg  linear(E\ y)).\\
% \neg linx1& :& \neg linx(\lx app\ (E_1\ x) \ (E_2\ x))\If strict(E_2\ x).\\
% \neg linx2& :& \neg linx(\lx app\ (E_1\ x) \ (E_2\ x))\If
% strict(E_1\ x).\\
\neg linxap0& :& \neg linx(\lx app\ (E_1\ x^1) \ (E_2\ x^1)).\\
\neg linxap1& : & \neg linx(\lx app\ (E_1\ x) \ (E_2\ x^1))\If \neg linx(\lx
 E_1\ x).\\ 
 \neg linxap2& : & \neg linx(\lx app\ (E_1\ x^1) \ (E_2\ x))\If \neg linx(\lx E_2\ x).\\ 
\neg linxap3& : & \neg linx(\lx app\ (E_1\ x) \ (E_2\ x))\If \neg \neg
linx(\lx E_1)\And \neg linx(\lx  E_2\ x).\\
\neg linxlm& : &\neg linx(\lx lam(\ly E\ x\ y))\If\\
& & \qquad(\PI{y}{exp} \neg linx(\lx y)\Imp \neg linx (\lx E\ x\ y)).
\eneq
\end{Example}
