 \section{Complementing Patterns}

In this section we introduce a generalization of the \emph{Not} 
algorithm to the case of \ho patterns.  As before, complement problems 
are treated as special equational problems and solved via a subset of 
the disunification rules lifted to the \ho case \cite{Lug95}.  
Differently for the the \fo case, the treatment is different depending 
on whether the term to be complemented is rigid or flexible.  In the 
latter case the complement has to take into account the status of free 
and bound variables: the crux 
lies in the presence of \emph{dependency constraints}, \ie when some 
of the variables mentioned in the binder does appear in the matrix.  
Differently from Lugiez who gives an ad hoc treatment, those 
constraints are directly dealt with by the type theory; indeed this is 
the aim to introduce \emph{relevant} types: for an $x$ in the binder 
relevant application $E \cdot x$ denotes an expression that 
\emph{must} use $x$, while intuitionistic application $E x$ denotes an 
expression that \emph{may or may not} use $x$.  Indeed if an 
expression depends on a subset of its argument, its complement is the 
set of terms that may depend on the former subset but must not appear 
in the (set-theoretic) complement of the former.  For rigid terms, 
instead, we proceed as in the \fo case by explosion, applied as often 
as the depth of the term to be complemented\footnote{This should 
follow from case-elimination: to understand : is the semantics of \ho 
E the DCA?}.  Some examples will make this clear.  We maintain the same 
notational convention of previous section for variables, with the 
difference that they are now capitalized.  Terms but inner 
meta-variables are in $\be$-long normal form.

\begin{figure}[h] 
\label{fig:ho-disunif}
\[
\begin{array} {lllllr}
% R :  \eqeb W M  \And P[W]  & \Lmap &  \eqeb W M \And [M/W]P & W \not \in 
% Var(M)\\
M1 &:& :   \eqeb W M \And \not\eqeb W N  & \Lmap &   \eqeb W M \And M \nebe  
 N  & W \not \in Var(M)\\
T1 & : & \eqeb   M M  & \Lmap &  \top \\
T1 & : &  \neqeb M M  & \Lmap &  \bot \\
 UE1  & : &  \forall \vec(Y) : P \And \l\xn .  Y(\ym)\nebe \l\xn. M  
 & \Lmap &  \bot  & Y\in\vec{Y} \\
 UE2  & : &  \forall \vY   : P \Or Y \nebe M  & \Lmap &  \forall \vY  : 
 [M/y] P \\
D1  & : &    \l\xn.a(\tm) \ebe\l\xn.a(\sm)  & \Lmap &  \ANd\limits^{n}_{i=1} 
  \l\xn.t_i \ebe \l\xn.s_i \\
D2  & : &  \l\xn.a(\tm) \nebe\l\xn.a(\sm)  & \Lmap &  \BOr\limits^{n}_{i=1} 
  \l\xn.t_i \nebe \l\xn.s_i \\
C1  & : &   \l\xn.a(\tm) \ebe \l\xn.b(\sm)  & \Lmap &  \bot \\
C2  & : &   \l\xn.a(\tm) \nebe\l\xn.b(\sm)  & \Lmap &  \top \\
& &\mbox{for $a,b$ distinct constants or loose bound variables or 
variables from $\xn$} \\
\\
E  & : &   \forall \vY : P  & \Lmap &       
(\exists \vec{W} \forall \vY : P \And \eqeb W  \l 
\xn.a(H_{1}(\xn)\mdots H_{k}(\xn))) \\
& & \mbox{For $W$ free or existential variable of type 
$\tau_{1}\Imp\mdots\tau_{n}\Imp\tau$, $x_{i}:\tau_{i}$\\
$a(H_{1}(\xn)\mdots H_{k}(\xn)) : \tau$ and $a \in 
\Sigma\cup\xn$}
\end{array}
\]
\caption{Complement Rules}
\end{figure}

\begin{Proposition}
The complement rules are correct and terminating
\end{Proposition}
\begin{proof} This proof is adapted from \cite{Lug95}. We use the 
restricted version of explosion with implicit merging\footnote{A 
similar proof goes thru for general disunification}.
\bit
\item
\item
We give the following control: all rules but explosion are tried 
non-deterministically: explosion is performed when
\bit
\item no other rule is applicable
\item $Z$ occurs in a disequation whose RHS head is not a variable 
and contains only universally quantified variables
\enit
We use as complexity measure on equational problems a triple $\la 
NUV,PUV,NSYM\ra$ where $NUV$ is the number of universal variables, 
$PUV({\cal E}) = \Sigma \mid p_{cal E}\mid$, \ie the sum of top 
positions of universal variables and $NSYM$ the number of non-logical 
symbol less lambda prefixes. The triple is lexicographically 
ordered. Now, $T_{1,2}, D_{1,2}C_{1,2}$ decrease $NSYM$ and $UE_{1,2}$ 
decrease  $NUV$. We cannot prove that explosion decrease complexity 
directly. What holds is that $E\l \nebe  \xn a(\tn)$ is followed by rules which decrease 
$PUV$: in fact exploding on $Z$ yields either clash (for a candidate $ \l 
\xn.b(H_{1}(\xn)\mdots H_{k}(\xn)))$ for $b\neq a$ or by decomposition 
otherwise. The first case leads to $\top$, the second to $n$ 
disequations of the form $\l x_m. H_{i}(\yn) \nebe \l x_{m}.t_{i}$ 
where universal variable occurs in $t_{i}$ at a smaller positions, 
thus reducing $PUV$.
\enit
\end{proof}
We now give the definition of complement of closed terms: we 
implicitly use an \ho-version of Corollary \ref{co: pt-equiv}, which 
states the equivalence of complement and disunification problems:

\begin{Definition}[Closed term complement]
$Not(\l \xn.c (N\xn)) = (\neqeb Z \l n.c(N\xn))$
\end{Definition}
 
\begin{Corollary}
\label{co: ho-pt-equiv}
$  Not(M) = M_1 \Or \cdots \Or M_n$ iff\ $\forall \vY : \neqeb Z M 
\Lmap^* \eqeb Z M_1 \Or \cdots \Or \eqeb Z M_n$.
\end{Corollary}
\begin{proof}

\end{proof}

\subsection{Examples}

Suppose we want to model predicates on the signature of the untyped 
$\l$-calculus. To distinguish between the former and the meta-language 
we introduce constants of well-known meaning and type (see \cite{Pfe9?}).
\[
\Sigma  ::= x \mid lam \ E \mid app \ E_{1} E_{2}
\]

As usual with \ho abstract syntax, we identify the name of (bound) 
variables in both languages. It is maybe worthwhile to stress that we 
have  three layers: the object language, the untyped 
$\l$-calculus, the meta-language, the type theory (whose variables are 
often called unification variables \cite{Nip93}) and the meta-meta 
language, the informal mathematical one used to describe the former. 
Given the adequacy of the encoding (proved for Mini-ML in 
\cite{Pfe9?}) we may think of living in the metalanguage.

\begin{Examplen} Imagine we want to negate the identity predicate:
\[
id(\l x.x)
\]
The intuitive answer is as follows:
\[
\begin{array}{l}
nid(\l x. app \ (E_{1} x) (E_{2} x))\\
nid(\l x. lam \ (E x))
\end{array}
\]

This follows from the computation of $Not(\l x.x)$, \ie (numbers 
indicate a disjunction):
\[
\begin{array}{l}
\neqeb Z \lx x \Lmap_{E}\\
1. \neqeb Z \lx x  \And  \eqeb Z  \l x.x \Lmap_{T2} \bot \\
2.  \neqeb Z \l x.x \And \exists E_{1},E_{2}.  \eqeb Z \l x.  app \
(E_{1} x) (E_{2}) x \Lmap_{C2}\\
  \eqeb Z  \l x. app \ (E_{1} x) (E_{2}) x\\
3.  \neqeb Z  \l x.x  \And \exists E.  \eqeb Z  \l x. lam \ (E x)  
\Lmap_{C2}\\
  \eqeb Z  \l x. lam \ (E x)
\end{array}
\]
\end{Examplen}

As remarked before, if the term to complement is nested, we need to 
explode several times, according to the nesting. This approach works 
also for loose bound variables that are dealt with as constants, with 
the difference that we have to exercise care in order to avoid 
capture-renaming substitutions. Let us see another related example 
that requires two explosions:

\begin{Examplen}
Consider the signature of numerals and the following problem $Not(\l 
x.x0)$. The first explosion lead three branches: the two imitation 
yields $  \eqeb Z\l x.0 \Or   \eqeb Z  \l x. s(N x)$. We trace the 
last case, projection: for the sake of brevity we leave the 
replacement implicit.
\[
\begin{array}{ll}
 \neqeb Z\l x.x0 \Lmap_{E}\\
\neqeb {\l x.x(N x)} \l x.x0 \And  \eqeb Z  \l x.x(N x) \Lmap_{D2}\\
 \neqeb{\l x.N x} \l x.0 \And  \eqeb Z  \l x.x(N x) \Lmap_{E(N)}\\
 1.\ \neqeb{\l x. 0} \l x.0 \And  \eqeb Z  \l x.x(N x) \Lmap \bot\\
 2.\  \neqeb {\l x.0} \lx .s(M) \And N \eqeb \l x .s(M) \And \eqeb Z \l 
 x.x(N x) \Lmap_{C2}\\
  \eqeb N \l x .s(M) \And  \eqeb Z  \l x.x(N x) \Lmap  \fbox{$\eqeb Z  \lx x(N 
  X)$}\\
3.\  \neqeb {\l x.0} \lx .x(s P) \And \eqeb N \l x. x(s P) \And  \eqeb Z  
\l x.x(N x) \Lmap_{C2}\\
   \eqeb N \l x.x(s P) \And  \eqeb Z  \l x.x(N x) \Lmap \fbox{$\eqeb Z  \lx x(x(N 
   x))$}
   \end{array}
   \] 

\end{Examplen}

Note that, as far as complement problems are concerned, the explosion 
rule has a specific format, where $P$ is constrained to be an 
unquantified disequation: more precisely $Z$ is an abbreviation for 
its $\be$-long normal form (for example as $\l x.N x$ in the example 
above).  

\beq E : \neqeb Z M_{1}\mdots \neqeb Z M_{l} \Lmap (\exists 
H_{n}: \neqeb Z M_{1}\mdots \neqeb Z M_{l} \And \\
\eqeb Z\l \xn.a(H_{1}(\xn)\mdots H_{k}(\xn)) \eneq


\section{Open Terms}

Consider a predicate true if a unary function does not depend on its argument
\beq
vacous(\lx E)
\eneq

Intuitively the complement is
\[
\begin{array}{l}
nvacous(\lx x)\\
nvacous(\lx app (E_{1} x) (E_{2} X)) 
   \If nvacous(\lx E_{1} x) ; nvacous(\lx E_{2} x)\\
nvacous(\lx lam (\l y. (E x y))) \If \Pi y. nvacous(\lx (E x y))
\end{array}
\]
Hence the complent of a fact would lead to possibly hypothetical and 
parametrical clauses. But we may internalize the (in)dependency 
costraints in the relevant type theory thus yielding
$ Not(\lx E) = \lx E\cdot x$, where the latter express the fact that 
a function is not vacous if its argument ought to occurr in its body. 
In this way we do not need clauses. More explicitely, by exploding in a 
relevant way $E$:
\[
Not(\lx E) = \lx x \Or \lx lam (E \cdot x) \Or \lx app (E_{1} \cdot 
x) (E_{2} x) \Or \lx app (E_{1} x) (E_{2}\cdot x)
\]
\[
\begin{array}{l}
nvacous(\lx x)\\
nvacous(\lx app (E_{1}\cdot  x) (E_{2} X)) \\
nvacous(\lx app (E_{1} x) (E_{2}\cdot X)) \\
nvacous(\lx lam (E\cdot x))
\end{array}
\]

More explosions refine the result in a way reminiscent of partial 
evaluation.

\[ Not(\l xy. E \cdot x \cdot y) = \l xy. E \Or \l xy.E\cdot x \Or \l 
xy. E x \cdot y\]


We have a relevant explosion rule that makes explicit relevant terms: 
note that, analougously to unification, projection and imitation 
produce each a conjunction of $k$ candidates, \ie for all $i\in 
[1..k]$:
\beq
E : \neqeb Z M_{1}\mdots \neqeb Z M_{l} \Lmap (\exists H_{k}: \neqeb 
Z M_{1}\mdots \neqeb Z M_{l} \And \\
\eqeb Z \l \xn.a(H_{1}(\xn) \mdots 
H_{i-1}, H_{i} \cdot \xn,H_{i+1}\mdots H_{k}(\xn))
\eneq

\textbf{A firts try} Let $\xn,\ol{y_{m}}$ be two list of variables 
such that for the underlying subsets $\ym\subseteq\xn$.  Let $\zp$ be 
the set-theoretic complent of $\xk$, is $\ym\cup\zp = \xn$.  We first 
treat the intuitionistic term case .The complement of $\l \xn.E(\ym)$ 
is the set of terms that \emph{may} depend on $\ym$ but has to depend 
on $\zp$, that is $\mid p\mid$ terms such that

\begin{Definition}[Open Intuitionistic Complement]
\[
Not(\l \xn.E(\ol{y_{m}})) = \BOr\limits_{j=1}^{p} \l \xn. 
E(\ym,z_{1}\mdots z_{j-1} \cdot z_{j},x_{z+1}\mdots z_{p}))
\]
\end{Definition}

\begin{Definition}[Open Relevant Complement]
\[
Not(\l \xn.E(\cdot\ol{y_{m}})) = \BOr\limits_{j=1}^{m} \l \xn. 
E(y_{1}\mdots y_{j-1}, y_{z+1}\mdots y_{m}))
\]
\end{Definition}
For example
\[
 \begin{array}{l}
 Not(\l xyzw.E(y,w))= \l xyzw.E(y,w\cdot x,z)\Or 
\l xyzw.E(y,w,x\cdot z)\\
Not(\l xy.E\cdot x\cdot y) = \l xy. E x \Or \l xy.E y
\end{array}
\]

Note that as far as dependencies are considered the order in which 
argument occurs in the matrix is irrelevant provieded that the term is 
linear (unrestricted), ie free variables occcurs only once. Since this 
can always be achieved by left-linearization (see \ref{dis}) we assume 
the former condition to be always satisfied in the following.

Example of linearized non-linear term
\[
\l xy. c(E x y) (E y x) \Lmap \l xy. c(E x y) (E' y x) \Ift \eqeb  E E'
\]

For the sake of clarity we give an example analogous to \ref{ex:num} 
in Chapter \ref{dis}: since we have a binding operator we have an 
additional case for projection.

\begin{Examplen}
\label{ex:lnum}
\[ \begin{array}{lll}
\fbox{$\forall Y:  \neqeb Z  \lx 0 \And  \neqeb Z  \lx ss(Y x)$}\\
\Lmap_{E(Z)(1,2,3)}\\
& (1) \ \forall Y: \neqeb Z \lx 0 \And \neqeb Z \lx ss(Y x) \And \eqeb 
Z \lx 0\\ 
\Lmap_{M1(Z)}\\
& \forall Y: \neqeb\lx 0 \lx 0 \And \neqeb\lx 0  \lx ss(Y x) \And   \eqeb Z \lx 0\\
\Lmap ^*_{Clh(F)}  \fbox{$\bot$}\\
& (2) \ \exists W \forall Y:  \neqeb Z  \lx 0 \And  \neqeb Z  \lx ss(Y x) 
\And   \eqeb Z  \lx s(W x)\\
\Lmap_{M1(Z)}\\
& \exists W   \forall Y: \neqeb\lx s(W x)  \lx 0 \And \neqeb \lx s(W x)  \lx ss(Y x) \And   \eqeb Z  sW x\\
\Lmap^*_{Dec,Clh(T)}\\
& \exists W \forall Y: \neqeb W sY \And   \eqeb Z  \lx s(W x)\\
\Lmap_{E(W)(2.1,2.2,2.3)}\\
&(2.1) \ \exists  W \forall Y:  \neqeb W sY \And   \eqeb Z  \lx s(W x) 
\And \eqeb\lx (W x) \lx O\\
\Lmap_{M1(Z)}\\
&  \exists  W \forall Y: \neqeb\lx 0 sY \And   \eqeb Z  \lx s(W x) 
\And \eqeb\lx (W x) \lx O\\
\Lmap^*_{Clh(T)}  \fbox{$  \eqeb Z  \lx s(W x)$}\\
& (2.2)  \ \exists W_1 W \forall Y: \neqeb W  sY \And   \eqeb Z  \lx s(W x) \And W 
\eqeb \lx s(W_1 x) \\
\Lmap^*_{M1(W),Dec1,UE_1(Y)} \fbox{$\bot$}\\
&(2.3) \ \exists  W \forall Y: \neqeb W  sY \And   \eqeb Z  \lx s(W x) 
\And   \eqeb W x\\
\Lmap_{M1(Z)}\\
&  \exists  W \forall Y: \neqeb\lx x \lx sY \And   \eqeb Z  \lx s(W x) 
\And \eqeb W x\\
\Lmap^*_{Clh(T)} \fbox{$  \eqeb Z  \lx s(W x)$}\\
& (3) \ \forall Y: \neqeb Z \lx 0 \And \neqeb Z \lx ss(Y x) \And \eqeb 
Z \lx x\\
\Lmap_{M1(Z)}\\
& \forall Y: \neqeb \lx x \lx 0 \And \neqeb \lx 0 \lx ss(Y x) \And 
  \eqeb Z \lx x\\
\Lmap ^*_{Clh(F)}  \fbox{$Z = \lx x$}
\end{array} \]
\end{Examplen}

 \textbf{The general case}.  There is a certain asymmetry between 
 relevant and intuitionistic application: while the former completely 
 determines the occurrence status of a variable, the latter leaves the 
 status floating indeterminately between the possibility or not of 
 occurrence.  We therefore decorate bound variables in a matrix three 
 \emph{occurrence annotations} $1,0,\top$ with the intended meaning 
 of\footnote{An analogous approach can be used to deal with resource 
 management in linear logic \cite{Pfe98}.}: 
 \beq
 x^{1} & : & \mbox{$x$ must occurr}\\
  x^{0} & : & \mbox{$x$ must \emph{not} occurr}\\
   x^{\top} & : & \mbox{$x$ is undetermined}
\eneq

For example $\l xy. E\cdot y$ is written as $\l xy. E x^{0} y_{1}$.

These annotations form a three-valued lattice with the partial 
ordering $1\leq \top,0\leq \top$.

The occurance decoration is extended to tuples in an obvious manner. 
This can be formalized with this translation.

\[
\mid \l \xn\ym\zp.E \cdot \xn \ym\mid= \lr \xn\l \ym\l^{0} \zp.E \xn_{1} 
\ym_{\top} \zp_{0}
\]

or  in a more suggestive notation:

\[
\mid \l \xn\ym\zp. E \cdot \xn \ym\mid = 
\l_{1}\xn\l^{\top}\ym\l^{0}\zp. E \xn_{1} \ym_{\top} \zp_{0}
\]

This approach can be internalized in a relevant type theory by 
introducing  typing and computation rules: here $\l^{0} \zp$ is the 
abstraction that contrains its argument \emph{not} to occurr and 
$M_{\top} z$ is the `empty' application between $M$ and its 
non-occurring argument $z$.
\[
\frac{\Phi ; \GG \prvs M: B}{\Phi;\GG\prvs(\l^{\top} x :A.M) : 
A\TImp B}{\TImp-I}
\qquad\qquad
\frac{\Phi;\GG\prvs M : A \TImp B \quad\quad \Phi;\eset \prvs N  : A}
{\Phi;\GG  \prvs M^{\top} N :B}{\TImp-E}
\]

Reductions: $(\beta)$
\beq
N-I & (\lt x:A.M)  N \Lmap & M\\
    N-R & (\lt x:A.M) \circ N \Lmap & M\\
    N-N & (\lt x:A.M)^{\top}  N \Lmap & M\\
  R-N & (\lr x:A.M)^{\top} N \Lmap & M\\
    I-N & (\l x:A.M)^{\top}N \Lmap &  M
    \eneq
Observe that the complement operation on terms behaves on occurance 
annotation like negation does on truth-values in Kleene's logic, in 
the sense of the following table:
\beq
Not(1)=0\\
Not(0)=1\\
Not(\top) = \top
\eneq
 
\smallskip
The idea is to form a disjunction of terms according to the occurance 
status of every variable in the binder; if the former is definite 
(must or must not occurr)  a disjunct with the given variable 
annotated with  the complement of the 
annotation is added and the remaining variables are set to undefined,
 otherwise we do nothing, \ie we do not add a diusjunct.
 
\begin{Definition}[Open terms complement]
\[Not(\l \xn.E(\xn^{1,0,\top})) =  \BOr\limits_{j=1}^{m} \l \xn. 
E(x_{1}^{\top}\mdots x_{j-1^{\top}},x^{0,1}, x_{j+1}^{\top}\mdots\xn^{\top}))
\]
\end{Definition}

Examples:

\[
\begin{array}{l}
Not(\l xy. E x^{0} y_{1})= \l xy. E x^{1} y_{\top} \Or \l xy. E x^{\top} 
y_{0}\\
Not(\l xy. E x^{T} y_{1})=  \l xy. E x^{\top} y_{0}
\end{array}
\]
It is worthwile to observe that the members of the disjunction are not 
mutually disjoint, due to the indeterminacy of $\top$. We can achieve 
an exclusive `or' if we resolve this indeterminacy, that is by 
considering for every $x^{\top}$ the two possibilies $x^{1},x^{0}$. It is clear that in the 
worst case scenario the number of disjunct is bound by $2^{n}$.

We sum up the definition: let $M$ be a linear term in $\be$-normal form: the 
complement $Not(M)$ is defined by induction on $M$. We have three 
cases: if $M$ is a variable the complement is empty; if it is flexible 
we take into account occurance values, provided there at least an 
$x_{i}$ such that its annotation is not $\top$ (not to overlap with 
variable case); otherwise it is the solved form of its correspondent 
disunification problem.

\begin{Definition} [$Not(M)$]
\[
\begin{array}{l}
Not(\l\xn.E \xn) = \eset\\
Not(\l \xn.E(\xn^{1,0,\top}) =  \BOr\limits_{j=1}^{m} \l \xn. 
E(x_{1}^{\top}\mdots x_{j-1^{\top}},x^{0,1}, 
x_{j+1}^{\top}\mdots\xn^{\top}))\\
Not(\l \xn.c (N\xn) = ( \neqeb Z \l \xn.c(N\xn))
\end{array}
\]
\end{Definition}



The proof obligation is proving the correctness of the algorithm \wrt 
the set-theoretic semantics, \ie a term is in $Not(N)$ iff it is not 
in $N$.
\begin{Proposition}[Partition Lemma]
\label{lemma:part}
 For any term $N:\tau, M \in \| Not(N)\|$ iff $  M  \not\in \| N \|$
\end{Proposition}
\begin{proof}
By induction on $N$. We prove only the if-direction, the converse 
being analogous.
\begin{itemize}
\item Basis: $M\in Not(E:\tau) \Bimp M \in \eset$ which trivially 
entails the conclusion
\item Step
\end{itemize}
\end{proof}
% \begin{Corollary}
%  $M \in Not(N)$ iff $ \| M \| \not\subseteq \| N \|$ (?? <- )
% \end{Corollary}

\subsection{Complenting \ho Horn programs}

Consider an \ho version of our favorite program:

\[
\begin{tt}
\begin{tabular}{l}
ho-even([y].0).\\
ho-even([y].s(s(N y))) :- ho-even([y].N y)
\end{tabular}
\end{tt}
\]

Form the completion of the program {\em comp(ho-even)} and massage it so 
as to derive its complement {\tt ho-odd} as in Figure~\ref{comp-ho-even}:
\begin{figure}
\label{comp-ho-even}
\[
\begin{array}{lll}
\forall Y. ho-even(Y) \Bimp \eqeb Y  \lx 0 \Or \exists W. \eqeb Y \lx 
ss(W x) \And ho-even(W)\\
 \quad \lead_{cp}\\
  \forall Y. \neg ho-even(Y) \Bimp \neg ( \eqeb Y  \lx 0 \Or 
\exists W. \eqeb Y \lx ss(W x) \And ho-even(W))\\
\quad \lead_{nnf}\\
   \forall Y. \neg ho-even(Y) \Bimp Y \neq \lx 0 \And (\forall 
W. Y \neq \lx ss(W x) \Or \neg ho-even(W))\\
\quad\lead_{lift}\\
  \forall Y. \neg ho-even(Y) \Bimp Y \neq \lx 0 \And \forall W 
.  Y \neq \lx ss(W x) \Or (\exists W. \eqeb Y \lx ss(W x) \And \neg 
ho-even(W))\\
\quad\lead_{dnf}\\
  \forall Y. \neg ho-even(Y) \Bimp (Y \neq \lx 0 \And \forall 
W. Y \neq \lx ss(W x)) \Or (Y \neq \lx 0 \And \exists W. \eqeb Y \lx 
ss(W x) \And \neg ho-even(W))\\
\quad\lead_{disunify(Y \neq \lx 0 \And \forall W : Y \neq \lx ss(W 
x))}\\
  \forall Y. \neg ho-even(Y) \Bimp \eqeb Y  \lx s(0)\Or \eqeb Y  
\lx x \Or (Y \neq \lx 0 \And \exists W. \eqeb Y \lx ss(W x) \And \neg 
ho-even(W))\\
\quad\lead_{disunify(Y \neq \lx 0 \And \exists W : \eqeb Y  \lx ss(W 
x))}\footnote{M1,Cls(T)}\\
  \forall Y. \neg ho-even(Y) \Bimp \eqeb Y  \lx s(0)\Or \eqeb Y  \lx x \Or (\exists W.  Y 
\eqeb\lx ss(W x)  \And \neg ho-even(W))\\

\quad\lead_{prettyp}\\
\end{array}
\]
\[
\begin{tt}
\begin{tabular}{l}
ho-odd([y].y).\\
ho-odd([y].s(0)).\\
ho-odd([y].s(s(y))) :- ho-odd([y].y).
\end{tabular}
\end{tt}
\]
\caption{{\tt ho-odd} example}
\end{figure}

`