\subsection{Covering}
Recall the relation of {\em subsumption} among (typed) first-order 
terms~\ref{} and related definitions. Note also the following trivial 
property: 
\[ s \leq t \, \mbox{entails } \|s\| \subseteq \|t\|
\]

From there we introduce the notion of {\em covering} of a term, \ie a 
set of terms such that every ground instance of the latter can be 
obtained as a ground instance of a term in the former. We assume a 
fixed signature with appropriate kind and type declarations. 
\begin{Def}
\label{def:cov}
Let $t: \tau$ and $\xi=\{t_1 \mdots t_n , \dots\}$ be a possibly 
infinite set of terms of the same type. $\xi$ is said to be a {\em 
covering for} $t$ (sometimes denoted $t_1\mdots t_n \mdots / t$) if 
$\|t\| \subseteq 
\bigcup_{i \in \omega} \|t_i\| $. It is  {\em exact} if $\|t\| = 
 \bigcup_{i \in \omega} \|t_i\| $. It is {\em tight} if no 
element is an instance of another, \ie it is an antichain under term 
subsumption. A 
{\em partition} of $t$ is a disjoint and exhaustive union of the
ground instances of  $t$. 
If $t:\tau$ is a variable, then a covering $\xi$ is called a {\em 
type covering {\rm or} $\tau$-covering}. A $\tau$-covering  is {\em 
canonical} if it consists of 
the type constructors, denoted $\delta(\tau)$. A covering $\xi$ for 
$t$ 
is {\em trivial}  if $\exists t_i \in \xi :  t \leq t_i$; in 
particular, a type covering is {\em trivial} if the variable belongs 
to the cover\footnote{In this discussion we are implicitly considering
terms modulo renaming.}. 
\end{Def}

 \begin{Examplen}
Consider the signature of numerals: $x \Or 0, 0\Or sx, \omega$ are 
resp.\ a trivial, 
the canonical and an infinite nat-covering. Consider the term  $t = sx$: $s0 \Or 
ssx, ssy\Or x, 0\Or s0 \Or ssy, s0 \Or sss0 \Or ssx$ are resp.\ an 
exact, a trivial, a non-exact, and an non-tight exact coverings.
\end{Examplen}

While it is clear how to generalize Definition~\ref{def:cov} to 
tuples 
of terms, we shall consider them as special single terms with a tuple 
prefix constructor.

\smallskip

We now list some basic properties of coverings:
\begin{Pty}
A  partition of $t$ is an exact and tight covering for $t$.
\end{Pty}
\begin{proof}
Tightness entails disjointness, exactness exhaustivity.
\end{proof}
We extend the definition of {\em canonical} covering to any term  in 
the obvious manner, \ie we consider $\delta(\tau)$ as a substitution 
acting on the free variables of the term.
\begin{Pty}
A canonical covering of $t$ is a partition of $t$.
\end{Pty}
We note the following:
\begin{Lemma}
\label{t_i<t}
If $\xi=\{t_1 \mdots t_n , \dots\}$ is a non-trivial exact covering 
for $t$, then for every $i\; , t_i < t$.
\end{Lemma}
\begin{proof}
Exactness  entails for all $i\,
, t_i \leq t$; by non-triviality  $t_i < t$.
\end{proof}

A term $t: \tau$ induces a set of coverings $\Xi_{t:\tau}$, which can 
be ordered by a variant of the clause subsumption ordering: 
%\cite{Lov8?}
Namely:

\begin{Def} For $\xi_1, \xi_2 \in \Xi_{t:\tau}$, we say that $\xi_1 
\leq\xi_2 $ iff there is a (well-typed) substitution $\q$ s.t.\ 
$\q\xi_1 \subseteq \xi_2$.
\end{Def}

This `lattice'  notation stresses similarity with subsumption. 

\begin{Examplen}
\[
(0 \Or sx) \leq  (0\Or s0 \Or ss0 \Or sssy)
\]
\end{Examplen}

It is clear that this relation is a
partial ordering among coverings.  We may thusly introduce  
 posets for a given generator, that is the covered term. 
\smallskip

The following lemma allows us to restrict only to posets of type 
coverings: it easily follows from the definition of covering.

\begin{Lemma}
\label{lem:type-cov}
Let $\xi$ be a $\tau$-covering and $t$ so that $t= \q x$. Then there 
exists a covering $\xi^\q$ for $x$ so that $t_1\mdots t_n \mdots / t$ 
iff $t^\q_1\mdots t^\q_n \mdots / x$ and for all open $t_i$: $t_i =\q 
t_i^\q$.
\end{Lemma}

\begin{Pty}
A tight type covering is non-trivial and exact.
\end{Pty}
\begin{proof}
It is exact by definition of type-covering. If it were trivial, it 
would contain a variable. 
\end{proof}
\begin{Corollary}
A tight type-covering is a partition.
\end{Corollary}

%FALSE \begin{Lemma}A partition for $t$ is the {\em minimum} 
non-trivial %covering for $t$.
%\end{Lemma}

\begin{Corollary}
A canonical covering $\delta(\tau)$ is 
the {\em minimum} non-trivial $\tau$-covering.
\end{Corollary}
\begin{proof}
Note that a canonical covering is a partition. Furthermore,
 any smaller covering would be trivial.
\end{proof}
Since we will consider only  non-trivial tight coverings, when not 
partitions, we may form the {\em pointed} poset (ppo) $\la 
\Xi_{x:\tau},\delta(\tau),\leq\ra$, where $\delta(\tau)$ is the 
minimum element of the poset.

In particular the ppo $\la \Xi_{: \tau},\delta(\tau),\leq\ra$ of 
tight type coverings is, under this ordering, a chain; besides only 
one substitution, determined by $\delta(\tau)$ induces the comparison 
for every pair of terms. Therefore the ppo $\la \Xi_{: 
\tau},\delta(\tau),\leq\ra$ is trivially a 
 lattice, where the top is the type enumerated by $x$, glb and lub are 
predecessor and successor functions on chains---see~\ref{lattice} for 
a more general treatment.
For usage in the next section (\ref{mdca}), we thus introduce a 
decoration of the aforementioned ordering, namely the {\em numbered 
subsumption ordering}.
\begin{Def}
\label{cr}
Let $\la \Xi_{: \tau},\delta(\tau),\leq\ra$ be the chain of tight 
type coverings: then $\xi \leq_1 \xi\prime$ iff $\xi\prime = 
succ(\xi)$ 
iff $lub(\xi,\xi\prime)=\xi\prime$. Let $\leq_{n+1}$ be the $n$-th 
iteration of this relation. Define the {\em case-rank} of a covering 
$cr(\xi:\tau)= n : \delta(\tau) \leq_n \xi$.
\end{Def}
\medskip

We now address the model theoretic foundations for coverings and the 
$CASE$ rule for the Horn case, by referring to some results proved in 
~\cite{Man88} for the uni-sorted case, but holding for the 
mani-sorted one too.

First it is shown that finite type coverings do cover the domain of 
every model of $CET^*$.
\begin{Ppn}
\label{tcov1}
Let $M \models CET^*$ and $\xi$ be a finite type covering. Then for 
all $d\in\mid M\mid$ there is a $t \in\xi$ and a variable assignment 
$V$ s.t.\ $d = t^{M,V}$.
\end{Ppn}

From the latter we can prove the following: 
\begin{Corollary}[Soundness of CASE]
\label{tcov2}
Let $P$ be definite and $\phi[\xn]$  a wff in the same language. Let 
$\ol{\xi_n}$ be a finite covering of $\tn$. Then 
$P\cup CET^*  \models \forall\phi[\tn]$  if $P\cup CET^*  \models 
\forall\phi[t^i_{j_i}]$ for all $t^i_{j_i} \in \xi_i$.
\end{Corollary}

This justifies the $CASE$  inference rule: by using $DCA$, a finite 
covering for a term $t$ is representative of all instances of $t$. 
Hence proving a statement for a finite exhaustive set is enough for 
introducing the universal.

Finally, we formulate this  $CASE$ rule.
\begin{Def}
Let $\phi[\xn]$ with free variables $x_i : \tau_i$ and for $i \in 
[1..n]$ let $\{t^i_1 \mdots t^i_{m_i}\}$ be a covering for $t_i$ 
of the appropriate types: then
\[
\frac{\forall\phi[\ol{t^1_m}] \cdots \forall\phi[\ol{t^n_{m_n}}]}
{\forall\phi[\tn]}   {\, t^i_1 \mdots t^i_{m_i} /t_i}
\]
\end{Def}

Lemma~\ref{lem:type-cov} allows us to use the following simplified 
format of the $CASE$ rule:
\begin{Def}
Let $\phi[\xn]$ with free variables $x_i : \tau_i$ and for $i \in 
[1..n]$ let $\{t^i_1 \mdots t^i_{m_i}\}$ be a covering for $x_i$ 
of the appropriate types: then
\[
\frac{\forall\phi[\ol{t^1_m}] \cdots \forall\phi[\ol{t^n_{m_n}}]}
{\forall\phi[\xn]}  {\, t^i_1 \mdots t^i_{m_i} /x_i}
\]
\end{Def}

We will denote with $CASE^-$ the version of the rule restricted to 
goals (literals, for the time being).

\smallskip

Then we can state a completeness result for $CASE$: indeed the only 
logical atomic consequences of the form $\forall p(\tn)$ of $P\cup 
CET^*$ induced by the $DCA$ are those provable by case analysis.

\begin{Ppn}
\label{tcov3}
Let $P$ be definite and $p(\tn)$  a possibly open atom. Let 
$\ol{\xi_n}$ be a finite covering of
 $\tn$. Then 
$P\cup CET^*  \models \forall p(\tn)$ iff   $P\cup CET^*  \models 
\forall p(\tn^i)$ for each $\tn^i$
from the covering $\ol{\xi_n}$.
\end{Ppn}

Finally we sum up the relationship among $P, comp(P), CET$ and $ 
CET^*$. It should come as no surprise that:
\bit
\item
$P\cup CET$ and $P\cup CET^*$ are equivalent modulo positive ground 
atoms
\item
$comp(P)\cup CET$ and $comp(P)\cup CET^*$ are equivalent modulo 
negative ground atoms and universal negative queries
\item $P \cup CET^*$ is a conservative extension of $P \cup CET$ modulo 
positive universal queries.
\enit

We conclude this section with the following lifting property:
\begin{Ppn}
\label{flift}
Let $P$ be definite and $p(\tn)$  a possibly open atom. Let  
$\ol{\xi_n}$ be a finite covering of $\tn$. Then if $p(\tn^i)$ 
from the covering fails finitely, so does $p(\tn)$.
\end{Ppn}

The converse of this proposition is painstakingly proven in the 
appendix of \cite{Mom95}.

\subsection{CASE-Elimination}
\label{mdca}
While the model-theoretic results of the previous section may be 
satisfying for the Horn setting, they are not straightforwardly 
generalizable to the more expressive framework we are interested in. 
We thus turn to proof-theory and show what we may call, with a jazzy 
term, $CASE$-elimination.

This actually boils down to showing that the rule of proof by case 
analysis is {\em admissible} w.r.t.\ systems augmented with the 
$DCA$. Indeed, the latter is derivable from the former in minimal 
logic with 
predicate congruence. Roughly, we can eliminate a $CASE$ step by a 
sequence of applications of the $DCA$ corresponding to the ``depth" 
of the covering, which is formalized in Definition~\ref{cr} by the 
notion of case-rank. This is then iterated on the whole derivation as 
usual. The base case is given by Lemma~\ref{DCA->Case}. We need some 
additional terminology. 

\begin{Def}
We say that a covering $\xi$ is {\em relevant } to $\phi_{{\cal 
L}_\Sigma}$ if
\bit
\item
 $\phi$ is a formula in the language ${\cal L}_\Sigma$
of the form $\forall x : \tau .\psi$ for a type $\tau \in Type$
\item 
$\xi$ is a $\tau$-covering.
\enit
\end{Def}

 We use the notation $CASE_\xi^\phi$ for an application of $CASE$ to 
a formula $\phi$ according to a relevant covering $\xi$. In 
particular $CASE^\phi_{\delta(\tau)}$ is the 
{\em canonical} rule, \ie it uses the canonical covering 
$\delta(\tau)$. Finally, let $Cng(\phi)$ be the congruence axioms for 
the predicate symbols occurring in $\phi_{{\cal L}_\Sigma}$\footnote{In the \ho 
setting predicate symbols belong to the signature and $Cng(\phi)$ is 
just the $Cng$ axiom in $CET$, but we opt to keep it separate. In 
fact at \fo they are not related to the signature and thus do not 
concern the free equality theory; second we know that its weak 
versions are derivable from the completion and finally we prefer not 
to assume calculi with built-in equality.}. We will shorten the 
notation when it does not lead to ambiguity.

\begin{Lemma}
\label{DCA->Case}
 For a given $\phi$ in ${\cal L}_\Sigma$: 
$DCA,Cng(\phi)\prv_{M} CASE_{\delta(\tau)}^\phi$.
\end{Lemma}
\begin{proof}
A simple derivation in minimal logic.
\end{proof}
Trivially this holds for $CASE^-_{\delta(\tau)}$.

\begin{Lemma} [Admissibility of $CASE$] Let $\xi =  t_1 \mdots t_n / 
x:\tau$ be a relevant  covering for $\forall x: \tau. \phi$ $\in  
{\cal L}_\Sigma$. For $i \in [1,n]$, let ${\cal D}_i :: \forall_\tau 
[t_i/x] \phi$ be a CASE-free derivation in minimal logic with  $DCA$ 
and $Cng(\phi)$ Then there is a case-free derivation ${\cal E} :: 
\forall x: \tau. \phi$ in the same system.
\end{Lemma}
\begin{proof}
By induction on the case-rank.
\bit
\item
Let $cr(\xi) =0$. Then $\xi = \delta(\tau)$ and the result follows
from Lemma~\ref{DCA->Case}.
\item
Let $cr(\xi) =n+1$. By inductive hypothesis.
\enit
\end{proof}
%\begin{sloppypar}
\begin{Corollary}[CASE-Elimination] 
\\
\label{CASE-elim}
$P, CASE \prv_M \phi$ entails $P,DCA,Cng(\phi) \prv_M \phi$
\end{Corollary}
%\end{sloppypar}
\begin{proof}
By structural induction of the derivation. For each inference rule 
which is not $CASE$, we appeal to the inductive hypothesis applied to 
the premise(s). Otherwise it is a $CASE_\xi$ with $cr(\xi) =n$: apply 
IH to the premises and admissibility of $CASE$ to recover the 
case-free derivations.
\end{proof}
The converse of Lemma~\ref{DCA->Case} does not hold for the literal 
version of $CASE$: 
\begin{Lemma}
For a given $\phi$ in $\cal L$,
$CASE_{\delta(\tau)}^\phi, Cng(\phi)\prv_{M}   DCA$ 
\end{Lemma}
\begin{proof}
For the sake of simplicity consider the case of the signature of 
numerals: then let $\phi[0]$ be $0=0 \Or \exists y.0=s(y)$ and
$\phi[s(x)]$ be $\forall x. s(x)=0 \Or \exists y.s(x)=s(y)$ and 
conclude by $CASE$.
\end{proof}

\begin{Corollary}[Equivalence]
\label{DCA=CASE}
$P, CASE \prv_M \phi$ iff $P,DCA,Cng(\phi) \prv_M \phi$
\end{Corollary}

%\end{document}
\subsubsection{Refinements: More on $DCA$}
%\input{dca}
This part is skipped; it contains a different formalism which will be 
fixed soon.

\subsubsection{CASE and Induction}

Of course, proof by case analysis must not be confused with 
induction, as it is, after all, only a limp, stepless induction.
\begin{Examplen}
\[\begin{array} {l}
 p(0)\\
 \Pi x. p(s(x)) \If p(x)
\end{array} \]
the query $\If\forall x.p(x)$ fails, since an inductive step is 
required, 
although the query $\If p(N)$ succeeds for every numeral $n$.
\end{Examplen}

Actually it is an easy consequence of the $CASE/DCA$ equivalence
that in certain theories, the addition of $CASE$, either as an axiom 
or a rule, is immaterial \wrt provability. Let $PA-IND$ be the Peano 
axioms  minus induction.
\begin{Corollary}
$Th(PA-IND\cup CASE) = Th(PA-IND)$.
\end{Corollary}
\begin{proof}
$DCA_{NAT}$ is provably equivalent to the third Peano axiom as in 
Enderton's textbook axiomatization.
\end{proof}

Since the latter axiom ensures that every element in the domain of 
the model can be construed (even not effectively) out of the 
signature of the relevant axioms, this suggests the following 
generalization:

\begin{Conjecture}
Let $\cal K$ be the class of reachable models: if $\cal A$ is a set 
of axioms which hold in $M \in \cal K$, then $Th({\cal A} \cup CASE) 
= Th({\cal A)}$.
\end{Conjecture}

Yet, it may be thought that there is some connection with the 
$\omega$-rule in arithmetic and its usage for cut-elimination. After
all, the latter coincides with the $CASE$ rule with an infinite 
domain covering. Well, it can be shown that the results in 
\cite{Bro90} do not hold for infinite coverings. Indeed 
Proposition~\ref{tcov1} and therefore Corollary~\ref{tcov2} are 
falsified, e.g.\ by considering an infinite nat-covering: clearly it 
does not cover any domain of a model of $CET^*$ not isomorphic to the 
numerals. This is the case for Proposition~\ref{flift}, too.

\subsection{The $CASE$ algorithm}

The problem is now to integrate $CASE$ with \SLD. Actually it seems
we have made no progress, since we have substituted an extensional 
universal with more extensional universals. Yet Lemma~\ref{t_i<t} 
roughly suggests this is not a regressio ad infinitum.

The proposal in \cite{Bro90} is to use an {\em ad hoc} algorithm to 
solve universal queries stemming by inversion on the $CASE$ rule. 
This is actually achieved for $\Sigma2$-formulae.

\begin{Def} [Correct answer for  $\Sigma2$-formulae]
Let $\phi(x:\tau,y:\tau\prime)$ be a quantifiers free 
formula---usually a Horn goal---and $\q_1\mdots\q_n$ correct answers 
for
$\exists y\exists x\phi$ s.t.\ for all $i\in [1..n]$
\begin{enumerate}
\item
 $\q_i(x)$ is a $\tau$-covering
\item There is $\q$ s.t.\ $\q=mgu(\q_i(y))$.
\end{enumerate}
Then $\q(y)$ is a {\em correct answer} for $\exists y\forall x\phi$.
\end{Def}

The idea is thus to produce a possibly infinite sequence of correct
answers from the existential goals looking for a subsequence that 
satisfies the above conditions. The bindings for the universal 
variable are regarded as partial type-covering: the algorithm stops 
when the type is covered and there exists an mgu for the existential 
one.  The state on which we compute is a set of triples $\la \q, U, 
L\ra$, where $\q$ is the candidate mgu, $U$ records what it is still 
to be covered and $L$ contains the initial sequence of substitution.
Rather then giving more details, we trace the computation on the 
nonpath example~\ref{path} using $LPA Prolog^@$. Note that the 
program in the paper is wrong: the third clause is not {\tt 
nonpath(X,Y,[Z|ZS]):-nonpath(X,Y,ZS)}. Moreover, the clause {\tt 
nonedge(b,a)} is subsumed by {\tt nonedge(E,a)}.


\begin{verbatim}
nonpath(X,Y,[]):-nonedge(X,Y).
nonpath(X,Y,[Z|ZS]):-nonedge(X,Z).
nonpath(X,Y,[Z|ZS]):-nonpath(Z,Y,ZS).

/* nonedge(b,a). */
nonedge(b,b).
nonedge(c,Z).
nonedge(Z,a).
nonedge(a,c).
\end{verbatim}



Consider the query $\If \exists Y\forall Xs: nonpath(c, Y, Xs)$ which 
succeeds with computed answer $Y =a$, as the values for $X$ given by 
$\q_1,\q_2,\q_3$ are a covering for $list(el)$.

Note that the algorithm does not automatically backtrack and cannot 
find the other answers $Y=b, Y=c$. Again operationally it might be 
though that this is due to the impossibility of finding suitable mgus 
for $Y$. Actually, this could be fixed with a simple {\em restart} 
mechanism which would reinitialize $\q$ to $\epsilon$ and $U$ to 
$\tau$. 

It seems that there is something inherently fishy in the 
inter-relationship between the $CASE$ algorithm in \cite{Bro90} and 
\SLD.

\subsection{Extensional Uniform Proofs}
%Semi-intensional Universal quantification}

We formulate a system of uniform proofs with extensional quantifiers 
so that the result is still an abstract logic programming language 
which extends conservatively the given one---in this case the 
implication free fragment of hhf. We do this in two steps. First we 
describe a very high level non deterministic
system that we then refine to an actual interpreter (in a 
continuation-passing style).

Consider Horn clauses and its extension UPiHorn with the two
universal quantifiers:
\beq
& D ::= & A | G \supset D| D_1 \And D_2|\Pi xD   \\
& G::= & A  | G_1 \And G_2 | G_1 \lor G_2 | \exists xG | \forall xG | 
\Pi xG 
\eneq

Recall the operational semantics of uniform proofs for this fragment:
\[\begin{array}{lr}
   P \prv G_1 \And G_2   \ \mbox{iff }  P  \prv G_1   \ \mbox{and }P  
\prv 
G_2 	  & AND\\
  P  \prv  G_1 \Or G_2   \ \mbox{iff }   P  \prv G_1  \ \mbox{or } P  
\prv G_2   & OR\\
   P \prv  \exists xG   \ \mbox{iff  there is a closed term t s.t.\ 
}  P  \prv [t/x]G & INSTANCE \\
 P  \prv \Pi xG   \ \mbox{iff }  P  \prv [a/x]G  \ \mbox{for a 
eigenvariable 'a'} &  GENERIC
\end{array}
\]
To those search operations we add:
\[
\begin{array}{lr}
P \vdash \forall x: \tau . G \ \mbox{iff } P \vdash \Pi [t_i/x]G \ 
\mbox{for } t_1\dots t_n /x & CASE
\end{array}
\]
Call this extensional uniform proofs ($\vdash_{eu}$). 
The idea is to `guess` the correct covering for $x:\tau$ and them
proceed with the intensional interpretation. As a matter of fact, we 
are factoring out the guessing game, much in the same style the 
INSTANCE operation is treated. In the high-level version, the right 
term is guessed and substituted. This is later operationally refined 
by using unification to provide the instantiation.

\begin{Examplen}
Let $\Gamma$ be the following program:
\[
\begin{array}{ll}
\Pi X. r(X)   \If  p(X).\\
\Pi X. r(X)  \If  q(X).\\
p(0).\\
p(s(0)).\\
\Pi X. q(s(s(X))).
\end{array}
\]
We trace the evaluation of query $\Gamma \prv_{eu}\forall X.r(X)$ 
\[
\begin{array}{lcl}
 & & \Gamma \prv_{eu} q(ssa)\\
\Gamma \prv_{eu} p(0) & \Gamma \prv_{eu} p(s0) & \ol{\Gamma \prv_{eu} 
r(ssa)}\\
\underline{\ol{\Gamma \prv_{eu} r(0)}} & \ol{\Gamma \prv_{eu} r(s0)} 
& \underline{\ol{\Gamma \prv_{eu} \Pi y. r(ssy)}}\\
 &\ol{\Gamma \prv_{eu}\forall X.r(X)}^{case}
\end{array}
\]
\end{Examplen}


From Corollary~\ref{DCA=CASE} we get
\begin{Corollary}
$P, CASE \prv_M \forall x.G$ iff $P,DCA,Cng(G) \prv_M \Pi x.G$
\end{Corollary}

\begin{Claim}
$P\vdash_{eu} G$ iff $P,CET^*_c\vdash_M G$
\end{Claim}


To be completed

\subsection{An Interpreter}


We assume two sets of parameters, the usual ones $a,b,c$ and the 
splittable ones $\overline{a},\ol{b},\ol{c}$ etc.... Those are the 
ones introduced by $\Pi$ immediately after a $CASE$ application (in a 
bottom-up search).
The technique could be called a form of iterative deepening search, 
since, upon reports of clashes among splittable parameters and 
clauses, deeper coverings have to be tried.
It would seem plausible to push the choice of the covering, \ie the 
instantiation of the splittable parameter, to the atomic level and 
inserting there the backtracking point, thus avoiding a premature 
commitment. This would mean adding the following 
clause to the immediate implication final condition something like:

\[
\frac{P\vdash A >> [t_i/x]A}{P\vdash A >> [\overline{a}/x]A} 
{t_1\dots t_n /x }
\]


Yet this is at once incomplete as it is shown by the previous example.

\begin{Example}
\smallskip
\begin{verbatim}
r(X) :- p(X).
r(X) :- q(X).
p(0).
p(s(0)).
q(s(s(X)).
\end{verbatim}
\end{Example}

\smallskip

Given the query $\forall X.r(X)$ we need to split immediately at the 
root rather than propagating the parameter thru backchaining on the 
first clauses. Note that two splitting have to be tried. Upon 
failure, control must be given back to the initial query, that will 
submit the correct covering.

Some Elf  high level code for the interpreter\footnote{to be 
inserted}:
