\section{The Clause Complement Algorithm}
\label{sec:cc}
\renewcommand{\vdf}{}
\newcommand{\vda}{\vd}

\renewcommand{\ex}{e_x}

We restrict to programs with:
\bit
\item \emph{Complementable} clauses of the form $Q\If G$ such that the
  head of every term  in $Q$ is rigid.
\item 
Parameters  of base type and  occurring only in \emph{head} position,
called \emph{Shallow Parameter Expressions}:
\[ \begin{array}{rrcl}
\mbox{\textit{SPE}}& e_x &  \bnfas & x\hastype a\bnfalt\lx e_x
\end{array}
\]
\enit

We do not formalize here the former assumptions on terms; note that
the rigidity restriction applies only to non-Horn predicate
definitions and can be relaxed significantly---see the comment and the
end of the proof of Theorem~\ref{thm:exclu}. We do give a definition
of complementable clause in Figure~\ref{fig:compl}.

\newcommand{\compg}[1]{\ga\vd #1 \mbox{ compl}}
\newcommand{\compd}[1]{ #1 \mbox{ compl}}
\begin{figure}
\bca
  \ianc{X\in\{\top,\perp\}\mbox{ or (dis)eq}}{ \compg{ X}}{G\ X}%\qquad 
%\ianc{}{\emp\vd Q\mbox{ compl}}{\atm\emp}
\vsk
\ianc{}{\GG;\top\vd Q \mbox{ compl}}{\atm}\vsk
\ianc{\mbox{\textrm{for all }}D\in\cD: \,\dom(\GG)\cap par(D)\not=\eset}{\compg{Q}}{\atm\cap}\vsk
\ibnc{ \GG;(\cD\And D)\vd G \mbox{ compl}}{\compd{D}}{  \compg{D\Imp G}}{ \Imp}\vsk
\ianc{(\GG,y\oftp a);\cD\vd[y/x] G  \mbox{ compl}}{\ga\vd \PI{x}{a}G\mbox{ compl}}{ \Pi^y}\vsk 
\ibnc{   \compg{G_1}}{  \compg{G_2}} {  \compg{G_1\And G_2}}{ \And}\vsk 
\ibnc{ \compg{G_1}}{ \compg{G_2}} { \compg{G_1\Or G_2}}{
  \Or}\vsk
 
\ianc{X\in\{\top,\perp\} }{\compd{X}}{D\ X} \vsk
  \ianc{\cdot;\top\vd G \mbox{ compl}} {\compd{Q\If D}}{ \If}\vsk
  \ianc{ \compd{[u/x]D}}{ \compd{\PIXA D}}{ \Pi^u}\vsk 
\ibnc{ \compd{D_1}}{\compd{D_2}} {  \compd{D_1\And D_2}}{ \And}\vsk
\ibnc{\compd{D_1}}{ \compd{D_2}} {  \compd{D_1\tensor D_2}}{ \tensor}
\eca
  \caption{Complementable clause and goal: $\compd{D}$ and $\compg{G}$}
  \label{fig:compl}
\end{figure}


\begin{Example}
The clause encoding the introduction rule for implication in
natural deduction from Example \ref{ex:nd} is \emph{not} complementable:
\beq
impi & : & nd(A\ imp\ B)\If (nd(A) \Imp nd(B)).
\eneq
On the other hand, the following  is allowed by rule $\atm$:
\beq
oplam^{\top}&:&  \PI{ E}{ exp\Imp exp} open\ (lam\ E)  \\
& & \qquad\If( \PI {x } {exp} \top_{open} \Imp open\ (E\ x)).
\eneq
The same rule  promotes the following:
\beq
isdall & : & \PI{D}{term\Imp form} isd\ (all\ D)\If \\
& & \qquad \PI{x}{term}  isd\ (D\ x).
\eneq
\end{Example}



% \[ \begin{array}{rrcl}
% \mbox{\textit{Shallow Parameter Expression}}& \ex & \bnfas &x \bnfalt \lamb{y}{A}\ex
% \end{array}\]
\renewcommand{\PIXA}{\PI{x}{a}} %base type parameters
The restriction on goal and clause yields this revised grammar:
\[ \begin{array}{rrcl}
\mbox{\textit{Clauses}}& D & \bnfas & \top\bnfalt\perp\bnfalt Q \If
G\bnfalt D_{1}\And D_{2}\bnfalt D_{1}\tensor D_{2}\bnfalt\PIXA D\\
\mbox{\textit{Goals}}& G & \bnfas & Q \bnfalt \top\bnfalt \perp\bnfalt
\vM \eqd \vN\bnfalt \vM \neqd \vN\bnfalt\\
& & & G_{1}\And G_{2}\bnfalt
G_{1}\Or G_{2}\bnfalt D\Imp G\bnfalt\PIXA G
\end{array}\]

Note that `facts' are represented, in a standardized way, by $ Q\If
\top$, although in examples we will omit to mention the body.  We
accordingly specialize the immediate implication and denial rules as
follows:

\[\begin{array}{c}
\ibnc{\ga\sp\vN\eqd\vM}{\ga\sp G}{ \ga\sp ( q\  \vN\If G) \imm q\
  \vM}{\imm\Imp}
\vsk
\ibnc{\ga\fp \vN\neqd\vM}{\fp G} {\ga\fp (q\ \vN\If G) \nimm q\ \vM}{\not\imm{\Imp_2}}
\vsk
\ianc{\ga\fp \vN\eqd\vM}{\ga\fp (q\ \vN\If G) \nimm q\ \vM}{\not\imm{\Imp_1}}
\end{array}\]

We remark that the `guards' in the immediate denial rules are
constructed so as to make the positive and negative judgment mutually
independent. Thus $\not\imm\Imp_1$ says that a clause $q\ \vN\If G$
denies a goal $q\ \vM$ if $\vN$ and $\vM$ clashes. Rule
$\not\imm\Imp_2$ instead attributes denial with the same conclusion
due to `failure' in the body. If we use $\Pi(D)$ to denote the
universal closure of (all) the free variables in $D$, then following
is a derived rule of inference:
% \begin{Lemma}
% \label{le:derivs}

$$
%\ianc{\mbox{for some $\GG\vd t\hastype A$}}{ \ga\sp  [t/x]D \imm
 % Q}{\ga\sp \PIXA D \imm Q}{\imm\Pi}
\ibnc{\GG\vd\s}{\ga\sp\s\vN\eqd\vM}{\ga\sp\Pi(q\
  \vN\If \top)\imm  q\ \vM}{\Pi\s\imm}
$$
% \end{Lemma}
% \begin{proof}
This can be proven by a straightforward induction on the number of
free variables in $\vN$.
%\end{proof}

\begin{figure}
    \[
    \begin{array}{c}
    %  \ianc{\gf \mnota(\top_{Q})=\neg D}{\vdf\mnotd (\top_q)  = \neg 
     % D}{\mnota\top}\vsk
%       \ianc{}{\cdot;\top\vdf\mnotd (\top)  = 
           \ianc{}{\vdf\mnotd (\top)  =       \perp}{\mnotd\top}\vsk
        \ianc{}{\vdf\mnotd (\perp)  =  \top}{\mnotd\perp}\vsk
    %( q\ \vM\If G)\in\cP
    \ianc{\vdf\mnotg(G) =  G'}{\vdf\mnotd( q\ \vM\If G) =
\BAnd_{\vN\in\mnot(\vM)}\Pi( \neg (q\ \vN)\If\top) \And ( \neg q\ \vM\If G')}{\mnotd\If}\vsk\vsk
         \ianc{\vdf\mnotd( D)=D'}{\vdf\mnotd (\PI{x}{A}D)  =  \PI{x}{A}D'}{\mnotd\Pi}\vsk
        \ibnc{\vdf\mnotd (D_{1})= D_1'}{\vdf\mnotd (D_{2})= D_2'}{\vdf\mnotd
        ( D_{1}\And D_{2})=D_1'\tensor D_2'}{\mnot\And}\vsk
       \ibnc{\vdf\mnotd (D_{1})= D_1'}{\vdf\mnotd (D_{2})= D_2'}{\vdf\mnotd
        ( D_{1}\tensor D_{2})=D_1'\And D_2'}{\mnot\tensor}
     %  \ibnc{
% %( q\ \vM\If G)\in\cD
% }{\gf\mnota( q\ \vM)=\neg D\quad\vdf\mnotg(G) = G'}{\vdf\mnotd( 
%       q\ \vM\If G) =\neg D\And ( \neg q\ \vM\If G')}{\mnota\If}\vsk
      \end{array}\]
    \caption{Clause Complementation: $\vdf\mnotd(D)=D'$}
  \label{fig:notclause}
\end{figure}


\begin{figure}
%\renewcommand{\ga}{\GG}
    \[
    \begin{array}{c}
       \ianc{}{\GG\vda\mnota (\perp)  =  \top}{\mnota\perp}\vsk
 \ianc{}{\GG\vd\mnota (\top_q)  = \BAnd_{x\in
 dom(\GG)}\BAnd_{xR^{i}q}\mnotxi(\top_q)}{\mnota\top}\vsk\\ 
%       \ianc{}{\GG\vda\mnota (\top_q)  = \BAnd_{x\in dom(\GG)}^{x\in
%          Q_{\mid_i}}\mnotxi(\top_q)}{\mnota\top}\vsk\vsk
%           \ianc{\vdf\mnotg(G) = G'}{\GG\vda\mnota( Q\If G) =\BAnd_{x\in dom(\GG)}^{x\in
%          Q_{\mid_i}}\mnotxi(Q) \And ( \neg Q\If
% G')}{\mnota\If}\vsk\vsk
           \ianc{\mnotg(G) = G'}{\GG\vd\mnota( Q\If G) =(\BAnd_{x\in
           dom(\GG)}\BAnd_{xR^{i}q}\mnotxi(Q)) \And ( \neg Q\If
           G')}{\mnota\If}\vsk\vsk
         \ianc{\GG\vda\mnota( D)=D'}{\GG\vda\mnota (\PI{x}{A}D)  =  \PI{x}{A}D'}{\mnota\Pi}\vsk
        \ibnc{\GG\vda\mnota (D_{1})= D_1'}{\GG\vda\mnota (D_{2})= D_2'}{\GG\vda\mnota
        ( D_{1}\And D_{2})=D_1'\tensor D_2'}{\mnot\And}\vsk
       \ibnc{\GG\vda\mnota (D_{1})= D_1'}{\GG\vda\mnota (D_{2})= D_2'}{\GG\vda\mnota
        ( D_{1}\tensor D_{2})=D_1'\And D_2'}{\mnot\tensor}
\vsk\vsk
\ibnc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\cdot\vd sh(x,A_i)=\ex}
{\gfq\mnotxi(\top_q)  =
      \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\  \ol{Z^i_{\ex}}\If \top}{\mnotxi\top}\vsk

    \ibnc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop\qquad M_i\equiv\ex}
%{\cdot\vd       sh(x,A_i)=\ex}
{\gfq\mnotxi  (q\ \Mn)=
    \BAnd_{1\leq j\leq n}^{j\not = i}(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}
     \neg q\ \ol{Z^i_{\ex}}\If M_j\neqd Z_j)}{\mnotxi\atm}
\vsk\vsk
\ianc{}{\gvd sh(x,a)=x}{\ex\atm}
\qquad
\ianc{\GG,y\oftp A\vd sh(x,B)=\ex}{\GG\vd sh(x,A\Imp B)=\lamb{y}{A}\ex}{\ex\Imp^y}
% \ianc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\gfq\mnotxi(\top_q)  =
%       \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ Z_1\dots Z_{i-1}\ x\
%       Z_{i+1}\dots Z_n}{\mnotxi\top}\vsk
%     \ianc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\gfq\mnotxi  (q\ \Mn)=
%     \BAnd_{1\leq j\leq n}^{j\not = i}(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}
%      \neg q\ \ol{Z^i_x}\If M_j\neqd Z_j)}{\mnotxi\atm}
 \end{array}\]
    \caption{Assumption Complementation: $\GG\vda\mnota(D)=D'$}
  \label{fig:notass}
\end{figure}

\smallskip We now introduce in Figure \ref{fig:notclause} and Figure
\ref{fig:notass} the rules for static and dynamic clause
complementation.  Consider a rule $q\ \vM\If G\in \defp(q)$; its
complement must contain a `factual' part motivating failure due to
clash with the head; the remainder $\mnotg (G)$ expresses failure in
the body, if any.  Clause complementation must discriminate whether
this rule belongs to the static or dynamic definition of a predicate.
In the first case all the relevant information is already present in
the head of the clause and we can use the term complementation
algorithm described in Chapter \ref{ch:relcomp}. This is accomplished
by the rule $\mnotd\Imp$, where a set of negative facts is built via
term complementation $\mnot (\vM)$, namely
$\BAnd_{\vN\in\mnot(\vM)}\Pi( \neg (q\ \vN)\If\top)$, whose fresh free
variables are universally closed; moreover the negative counterpart of
the source clause is obtained via complementation of the body. The
original quantification is retained thanks to rule $\mnotd\Pi$.

Otherwise, we can think of complementation of assumptions, which are
by definition parametric in some $x$, as static clause complementation
\wrt $x$. Informally, for an atomic assumption, say $ q\ M_1\dots
M_{i-1}\ \ex\ M_{i+1}\dots M_n$, its complement can be taken as
$\mnotd( q_{\ex}\ M_1\dots M_{i-1}\ M_{i+1}\dots M_n)$. However, most of the
those arguments, which at compile time are 
variables, will be instantiated at run-time: therefore it would be
incorrect to compute their complement as empty. Since we cannot
foresee this instantiation, we achieve term complementation via
the introduction of disequations. This is achieved by the judgment
$\gf\mnota(D)$; note that the latter is type directed and can be seen
as a \emph{constraints}-based version of term complementation.
% \bmeta Note the restriction to flat parameters\emeta
% We abbreviate $q\ M_1\dots M_{i-1} \ x\ M_{1+1}\dots M_{n}$ in $q \ 
% \ol{M_{x}^{i}}$.  Whenever we use this notation we will always assume
% that the type of $x$ is relevant to $Q$.
% For every $x\hastype A\in\GG$ relevant to $Q$ and for every $i$
% such that $x\in Q_{\mid_i}$, define:
% \beq
% \gf\mnota(D)=\BAnd D'\mid \gfq\mnotxi(D)=D'\eneq
% and
% \[
% \begin{array}{c}
% \ianc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\gfq\mnotxi(\top_q)  =
%       \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ Z_1\dots Z_{i-1}\ x\
%       Z_{i+1}\dots Z_n}{\mnotxi\top}\vsk
%     \ianc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop
% %\ga\vd\mnotg(G)=G'
% }{\begin{array}{l}
% \gfq\mnotxi  (q\ \Mn)=
%     \BAnd_{1\leq j\leq n}^{j\not = i}(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}
%      \neg q\ \ol{Z^i_x}\If M_j\neqd Z_j)
% %    \mbox{}\And (\neg q\ \Mn\If G')
%    \end{array}}{\mnotxi\atm}
%     \end{array}
%     \]
We briefly comment on rules $\mnota\top$ and $\mnota\Imp$:    
\begin{itemize}
    \item Pivot on $x\oftp a\in\GG$.
    \item Locate a type $A_i$ such that $x$ is relevant to $Q$ at $i$.
    \item Complement $D$ \wrt $x$ and $i$, by introducing the
      appropriate disequation(s).
    \item Repeat for every relevant $x$ and  $i$.
    \item Special case: if no $x$ is relevant, the trivial program is
      returned.
\end{itemize}
     
The judgment is not optimized since if $M_j$ is
essentially existential, an unsatisfiable clause is built; moreover,
if it is a ground term, we add a disequation, rather then computing
the term complement. We can perform constraint simplification in a
separated phase, see Section \ref{sec:simplify}.


Notice the different treatment of the trivial clause $\top$ by rules
$\mnotd\top$ and $\mnota\top$: if no parameter has been assumed, then $\top$
truly stands for the empty predicate definition and its complement is
the universal definition $\perp$.
% Notice that in this case,
%by definition of allowed program, $\cD$ must be empty as well. 
If, on the other side $\GG$ is \emph{not} empty, it means that
$\top_q$ has been introduced during the $\top$-normalization
preprocessing phase and has been localized to the predicate $q$.  The
rule $\mnotxi\top$ allows to build a new negative assumption \wrt
$q,x,i$ in case $\top_q$ is the only dynamic definition of $q$. As
$\top_q$ carries no information at all concerning $q$, the most
general negative assumption is added. The $\GG\vd sh(x,A)$ judgment
builds a shallow parameter expression as required by the type of the
position in $q$ where it ought to occur; finally, the notation
$\ol{Z^i_{\ex}}$ abridges $ Z_1\dots Z_{i-1}\ \ex\ Z_{i+1}\dots Z_n$,
where the $Z$'s are fresh logic variables.

\smallskip The other rules for static and dynamic clause
complementation simply recur on the program respecting the duality of
conjunction and disjunction \wrt negation.  This a somewhat delicate
point and therefore we discuss it in details.  Intuitively, negative
clauses stemming from the complement of a clause in the definition of
a predicate need to be considered simultaneously.  In fact, if an goal
is unprovable from its definition, then its negation must be provable
from the complement of each clause of its definition; symmetrically if
it is provable then its negation must be unprovable from the
complement of at least one.  What we have described coincides the
operational semantics of
%This is abstractly accomplished by the 
an operator, which works exactly as disjunction.  This is arguably at
odd with the commonly held goal-oriented interpretation of the sequent
calculus as uniform proofs, since case analysis makes the latter
incomplete \wrt minimal logic (but see \cite{Nadathur95lics} for ways
to incorporate the former in the framework of uniform proofs). First,
we remark that the $\tensor$ is available uniquely as a program
constructor and can therefore be used only in the focusing phase of
deductions;in (Section \ref{ssec:tensor}), we will show how to
`compile away' all occurrences of $\tensor$ in clauses. This is an \ho
equivalent of the intersection operator `@' described in \cite{Bar90}.
This will restore completeness of uniform proofs

\newcommand{\gavd}{}
\begin{figure}
\renewcommand{\ga}{\GG;\cD}
    \[
    \begin{array}{c}
      \ianc{}{\gavd\mnotg (\top)  =  \perp}{\mnotg\top}\vsk
        \ianc{}{\gavd\mnotg (\perp)  =  \top}{\mnotg\perp}\vsk
      \ianc{}{\gavd\mnotg(\vM \eqd \vN)= (\vM \neqd \vN)}{\mnot\eqd}\vsk
      \ianc{}{\gavd\mnotg(\vM \neqd \vN)= (\vM \eqd \vN)}{\mnot\neqd}\vsk
        \ianc{}{\gavd\mnotg (Q) =  \neg Q}{\mnotg At}\vsk
        %   \ianc{(\GG,y\oftp A);\cD\vd\mnotg([y/x]G)=[y/x]G'}{\gavd\mnotg
        %(\PI{x}{A}G)  =  \PI{x}{A}G'}{\mnotg\Pi^*}\vsk
      \ianc{\gavd\mnotg(G)=G'}{\gavd\mnotg
        (\PI{x}{A}G)  =  \PI{x}{A}G'}{\mnotg\Pi}\vsk
        \ibnc{\gavd\mnotg (G_{1})= G_1'}{\gavd\mnotg (G_{2})= G_2'}{\gavd\mnotg
        ( G_{1}\And G_{2})=G_1'\Or G_2'}{\mnot\And}\vsk
       \ibnc{\gavd\mnotg (G_{1})= G_1'}{\gavd\mnotg (G_{2})= G_2'}{\gavd\mnotg
        ( G_{1}\Or G_{2})= G_1'\And G_2'}{\mnot\Or}\vsk
      \ianc{\gavd\mnotg(G) = G'}{\gavd\mnotg( D \Imp G) = D\Imp   G'}{\mnotg\Imp}
    \end{array}\]
    \caption{Goal Complementation: $\gavd\mnotg(G)=G'$}
  \label{fig:notgoal}
\end{figure}

Goal complemenation, that is the judgment $ \mnotg(G)$ depicted in
Figure \ref{fig:notgoal}, only brings the body into a normalized
format; namely, in what we may call \emph{parametric negation normal
  form}, to stress the distinction from classical negation normal form
or even from negation normal form in constructive logics as extension
of intuitionism with strong negation \cite{Nelson49}.  This
re-iterates the problem with strong negation we have hinted in Section
\ref{sec:completion}; negation is pushed inward but jumps over
parametric-hypothetical judgments to respect the operational
interpretation of unprovability.

%This is why we need the \emph{augmentation} procedure described in the
%next Section (\ref{sec:aug}).

\smallskip
As a final remark, we note that we must take the  complementation of a
program, seen as a conjunction,
\emph{predicate definition-wise} rather that \emph{clause-wise}. In
fact, it would be incorrect to simply negate a program as it would
introduce disjunctions rather than conjunction among predicate
definitions. The same remark applies to the `dynamic' program $\cD$. Formally,
fixed a signature $\Sigma_{\cP}$ and given a program $\cP$:
\beq
\mnotd(\cP) & = &  \BAnd_{q\in\Sigma_{\cP}} \mnotd (\defp(q,\cP))
\eneq
Similarly for a conjunction of dynamic assumptions $\cD$:
\beq
\mnota(\cD) & = &  \BAnd_{q\in\Sigma_{\cP}} \mnota (\defp(q,\cD))
\eneq
We abbreviate $\mnotd(\defp(q))$ in $\defp(\neg q)$.   
If $\PP$ is the source program, we use $\PM$ for $\mnotd (\PP)$.


The following example is somehow a special case of the general
procedure, as assumption complementation is trivial, 
but it is useful to clarify in isolation the  rules 
for clause and goal complementation. We refer to the next Section
(\ref{sec:aug}) for more complex examples.

\begin{Example}
\label{ex:closed}
A $\l$-expression is \emph{closed} if it has no occurrence of free
variables; let $z\hastype exp$ be a constant:
\beq
cloz & : & closed\ z.\\
clolam &: & \PI{E}{exp}closed\ (lam\ E) \If (\PI {x } {exp}\ (closed\ x 
\Imp closed\ (E\ x).)\\
cloapp &: & \PI{ E_{1}}{exp}\PI{E_{2}}{exp} closed\ (app\ E_{1} \ E_{2}) \If 
closed\ E_1 \And closed\ E_{2}.\\
\eneq

Now, $\defp(closed)= cloz\And clolam\And cloapp$. Therefore:
 $$\defp(\neg
closed) = \mnotd (cloz) \otimes \mnotd (clolam) \otimes \mnotd
(cloapp)$$
\beq
\mnotd (cloz) 
%& = &\mnotd (closed\ z)\\
            & = &\Pi(\BAnd_{ N\in\mnot(z)}\neg closed\ N)\\
            & = & \PI{F}{exp}\neg closed\ (lam\ F)\And
            \PI{F_1,F_2}{exp} \neg closed\ (app\ F_{1} \ F_{2}).
\vsk
\mnotd (clolam) 
%& = &\mnotd (closed\ lam\ E) \And
%\neg closed\ (lam\ E) \If \mnotg (\PI {x } {exp}\ (closed\ x \Imp closed\ 
%(E\ x))\\
              & = &\Pi(\BAnd_{N\in\mnot (lam\ E)}\neg closed\ N)\And\\
&&
\PI{E}{exp}\neg closed\ (lam\ E) \If \mnotg (\PI {x } {exp}\ (closed\ x \Imp closed\ 
(E\ x))\\
              & = &\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)).
\vsk
\mnotd (cloapp) 
%& = & \mnotd (closed\ (app\ E_1\ E_{2}))\And\\
%& & \PI{ E_{1}}{exp}\PI{E_{2}}{exp} 
%\neg  closed\ (app\ E_{1} E_{2}) \If \mnotg(closed\ E_1 \And closed\ 
%E_{2})\\
              & = & \Pi(\BAnd_{N\in\mnot  (app\ E_1 E_2))} \neg
              closed\ N)\And\\
& & \PI{E_1,E_2}{exp} \neg closed\ (app\ E_{1} E_{2}) \If \mnotg(closed\ E_1 \And 
closed\ E_{2})\\
              & = & \neg closed\ z\And \PI{F}{exp}\neg closed (lam\
              F)\And\\
&& \PI{E_1,E_2}{exp}  \neg closed\ (app\ E_{1} E_{2}) \If
\neg closed\ E_1 \Or \neg closed\ E_{2}.
\eneq
\end{Example}

If you want to see the definition simplified, please skip to Example
\ref{ex:closedatensor} and the final result in Example  \ref{ex:closedfinal}.


