YES
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Frameset//EN"
"http:/www.w3.org/TR/html4/frameset.dtd">
<html>
<head>
<title>Left Termination proof of ../tpdb/LP/terminweb/combination/der.pl</title>
</head>
<body>
<BR><B>Left Termination</B> of the query pattern
der_in_4(g, g, a, a)
w.r.t. the given <I>Prolog program</I> could successfully be <font color=#00ff00>proven</font>:<BR><BR><BR><BR><pre>&#8627 <B>Prolog</B></pre><pre>  &#8627 PrologToPiTRSProof</pre><BR>Clauses:<BR><BR>der(d(e(t)), const(1)).<BR>der(d(e(const(A))), const(0)).<BR>der(d(e(+(X, Y))), +(DX, DY))&#160;:-&#160;','(der(d(e(X)), DX), der(d(e(Y)), DY)).<BR>der(d(e(*(X, Y))), +(*(X, DY), *(Y, DX)))&#160;:-&#160;','(der(d(e(X)), DX), der(d(e(Y)), DY)).<BR>der(d(d(X)), DDX)&#160;:-&#160;','(der(d(X), DX), der(d(e(DX)), DDX)).<BR><BR>Queries:<BR><BR>der(g,g,a,a).<BR><BR>We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
<BR>Transforming <I>Prolog</I> into the following <B>Term Rewriting System</B>:
<BR>Pi-finite rewrite system:<BR>R is empty.<BR>Pi is empty.<BR>
<P><B>Infinitary Constructor Rewriting Termination</B> of PiTRS implies <B>Termination</B> of Prolog<P>
<BR><BR><pre>&#8627 Prolog</pre><pre>  &#8627 PrologToPiTRSProof</pre><pre>    &#8627 <B>PiTRS</B></pre><pre>      &#8627 RisEmptyProof</pre><BR>Pi-finite rewrite system:<BR>R is empty.<BR>Pi is empty.<BR><BR>The TRS R is empty. Hence, termination is trivially proven.<BR><BR></body>

