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/talp/maria/deriv.pl</title>
</head>
<body>
<BR><B>Left Termination</B> of the query pattern
deriv_in_3(g, g, 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 PredefinedPredicateTransformerProof</pre><BR>Clauses:<BR><BR>d(+(U, V), X, +(DU, DV))&#160;:-&#160;','(!, ','(d(U, X, DU), d(V, X, DV))).<BR>d(-(U, V), X, -(DU, DV))&#160;:-&#160;','(!, ','(d(U, X, DU), d(V, X, DV))).<BR>d(*(U, V), X, +(*(DU, V), *(U, DV)))&#160;:-&#160;','(!, ','(d(U, X, DU), d(V, X, DV))).<BR>d(/(U, V), X, /(-(*(DU, V), *(U, DV)), ^(V, 2)))&#160;:-&#160;','(!, ','(d(U, X, DU), d(V, X, DV))).<BR>d(^(U, N), X, *(DU, *(N, ^(U, N1))))&#160;:-&#160;','(!, ','(integer(N), ','(is(N1, -(N, 1)), d(U, X, DU)))).<BR>d(-(U), X, -(DU))&#160;:-&#160;','(!, d(U, X, DU)).<BR>d(exp(U), X, *(exp(U), DU))&#160;:-&#160;','(!, d(U, X, DU)).<BR>d(log(U), X, /(DU, U))&#160;:-&#160;','(!, d(U, X, DU)).<BR>d(X, X, 1)&#160;:-&#160;!.<BR>d(C, X, 0).<BR>main&#160;:-&#160;','(expression(X), ','(d(X, x, Y), write(Y))).<BR>expression(+(Exp, -(Exp, *(Exp, /(Exp, *(Exp, /(Exp, Exp)))))))&#160;:-&#160;value(Exp).<BR>value(/(+(*(3, x), -(*(4, *(exp(^(x, 3)), log(^(x, 2)))), 2)), +(-(*(3, x)), /(5, +(exp(^(x, 4)), 2))))).<BR><BR>Queries:<BR><BR>deriv(g,g,a).<BR><BR>Added definitions of predefined predicates.<BR><BR><pre>&#8627 Prolog</pre><pre>  &#8627 PredefinedPredicateTransformerProof</pre><pre>    &#8627 <B>Prolog</B></pre><pre>      &#8627 CutEliminatorProof</pre><BR>Clauses:<BR><BR>d(+(U, V), X, +(DU, DV))&#160;:-&#160;','(!, ','(d(U, X, DU), d(V, X, DV))).<BR>d(-(U, V), X, -(DU, DV))&#160;:-&#160;','(!, ','(d(U, X, DU), d(V, X, DV))).<BR>d(*(U, V), X, +(*(DU, V), *(U, DV)))&#160;:-&#160;','(!, ','(d(U, X, DU), d(V, X, DV))).<BR>d(/(U, V), X, /(-(*(DU, V), *(U, DV)), ^(V, succ(succ(zero)))))&#160;:-&#160;','(!, ','(d(U, X, DU), d(V, X, DV))).<BR>d(^(U, N), X, *(DU, *(N, ^(U, N1))))&#160;:-&#160;','(!, ','(integer(N), ','(','(isMinus(N, succ(zero), U), =(N1, U)), d(U, X, DU)))).<BR>d(-(U), X, -(DU))&#160;:-&#160;','(!, d(U, X, DU)).<BR>d(exp(U), X, *(exp(U), DU))&#160;:-&#160;','(!, d(U, X, DU)).<BR>d(log(U), X, /(DU, U))&#160;:-&#160;','(!, d(U, X, DU)).<BR>d(X, X, succ(zero))&#160;:-&#160;!.<BR>d(C, X, zero).<BR>main&#160;:-&#160;','(expression(X), ','(d(X, x, Y), write(Y))).<BR>expression(+(Exp, -(Exp, *(Exp, /(Exp, *(Exp, /(Exp, Exp)))))))&#160;:-&#160;value(Exp).<BR>value(/(+(*(succ(succ(succ(zero))), x), -(*(succ(succ(succ(succ(zero)))), *(exp(^(x, succ(succ(succ(zero))))), log(^(x, succ(succ(zero)))))), succ(succ(zero)))), +(-(*(succ(succ(succ(zero))), x)), /(succ(succ(succ(succ(succ(zero))))), +(exp(^(x, succ(succ(succ(succ(zero)))))), succ(succ(zero))))))).<BR>isPlus(zero, X, X).<BR>isPlus(succ(X), zero, succ(X)).<BR>isPlus(succ(X), succ(Y), succ(succ(Z)))&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(succ(X), pred(Y), Z)&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(pred(X), zero, pred(X)).<BR>isPlus(pred(X), succ(Y), Z)&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(pred(X), pred(Y), pred(pred(Z)))&#160;:-&#160;isPlus(X, Y, Z).<BR>isMinus(X, zero, X).<BR>isMinus(zero, succ(Y), pred(Z))&#160;:-&#160;isMinus(zero, Y, Z).<BR>isMinus(zero, pred(Y), succ(Z))&#160;:-&#160;isMinus(zero, Y, Z).<BR>isMinus(succ(X), succ(Y), Z)&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(succ(X), pred(Y), succ(succ(Z)))&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(pred(X), succ(Y), pred(pred(Z)))&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(pred(X), pred(Y), Z)&#160;:-&#160;isMinus(X, Y, Z).<BR>isTimes(X, zero, zero).<BR>isTimes(zero, succ(Y), zero).<BR>isTimes(zero, pred(Y), zero).<BR>isTimes(succ(X), succ(Y), Z)&#160;:-&#160;','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).<BR>isTimes(succ(X), pred(Y), Z)&#160;:-&#160;','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).<BR>isTimes(pred(X), succ(Y), Z)&#160;:-&#160;','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).<BR>isTimes(pred(X), pred(Y), Z)&#160;:-&#160;','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).<BR>isDiv(zero, succ(Y), zero).<BR>isDiv(zero, pred(Y), zero).<BR>isDiv(succ(X), succ(Y), zero)&#160;:-&#160;isMinus(succ(X), succ(Y), pred(Z)).<BR>isDiv(succ(X), succ(Y), succ(Z))&#160;:-&#160;','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).<BR>isDiv(succ(X), pred(Y), Z)&#160;:-&#160;','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).<BR>isDiv(pred(X), pred(Y), zero)&#160;:-&#160;isMinus(pred(X), pred(Y), succ(Z)).<BR>isDiv(pred(X), pred(Y), succ(Z))&#160;:-&#160;','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).<BR>isDiv(pred(X), succ(Y), Z)&#160;:-&#160;','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).<BR>isModulo(X, Y, Z)&#160;:-&#160;','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).<BR>=(X, X).<BR><BR>Queries:<BR><BR>deriv(g,g,a).<BR><BR>Eliminated all cuts by simply ignoring them.<BR><BR><pre>&#8627 Prolog</pre><pre>  &#8627 PredefinedPredicateTransformerProof</pre><pre>    &#8627 Prolog</pre><pre>      &#8627 CutEliminatorProof</pre><pre>        &#8627 <B>Prolog</B></pre><pre>          &#8627 UndefinedPredicateHandlerProof</pre><BR>Clauses:<BR><BR>d(+(U, V), X, +(DU, DV))&#160;:-&#160;','(d(U, X, DU), d(V, X, DV)).<BR>d(-(U, V), X, -(DU, DV))&#160;:-&#160;','(d(U, X, DU), d(V, X, DV)).<BR>d(*(U, V), X, +(*(DU, V), *(U, DV)))&#160;:-&#160;','(d(U, X, DU), d(V, X, DV)).<BR>d(/(U, V), X, /(-(*(DU, V), *(U, DV)), ^(V, succ(succ(zero)))))&#160;:-&#160;','(d(U, X, DU), d(V, X, DV)).<BR>d(^(U, N), X, *(DU, *(N, ^(U, N1))))&#160;:-&#160;','(integer(N), ','(','(isMinus(N, succ(zero), U), =(N1, U)), d(U, X, DU))).<BR>d(-(U), X, -(DU))&#160;:-&#160;d(U, X, DU).<BR>d(exp(U), X, *(exp(U), DU))&#160;:-&#160;d(U, X, DU).<BR>d(log(U), X, /(DU, U))&#160;:-&#160;d(U, X, DU).<BR>d(X, X, succ(zero))&#160;:-&#160;true.<BR>d(C, X, zero).<BR>main&#160;:-&#160;','(expression(X), ','(d(X, x, Y), write(Y))).<BR>expression(+(Exp, -(Exp, *(Exp, /(Exp, *(Exp, /(Exp, Exp)))))))&#160;:-&#160;value(Exp).<BR>value(/(+(*(succ(succ(succ(zero))), x), -(*(succ(succ(succ(succ(zero)))), *(exp(^(x, succ(succ(succ(zero))))), log(^(x, succ(succ(zero)))))), succ(succ(zero)))), +(-(*(succ(succ(succ(zero))), x)), /(succ(succ(succ(succ(succ(zero))))), +(exp(^(x, succ(succ(succ(succ(zero)))))), succ(succ(zero))))))).<BR>isPlus(zero, X, X).<BR>isPlus(succ(X), zero, succ(X)).<BR>isPlus(succ(X), succ(Y), succ(succ(Z)))&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(succ(X), pred(Y), Z)&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(pred(X), zero, pred(X)).<BR>isPlus(pred(X), succ(Y), Z)&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(pred(X), pred(Y), pred(pred(Z)))&#160;:-&#160;isPlus(X, Y, Z).<BR>isMinus(X, zero, X).<BR>isMinus(zero, succ(Y), pred(Z))&#160;:-&#160;isMinus(zero, Y, Z).<BR>isMinus(zero, pred(Y), succ(Z))&#160;:-&#160;isMinus(zero, Y, Z).<BR>isMinus(succ(X), succ(Y), Z)&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(succ(X), pred(Y), succ(succ(Z)))&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(pred(X), succ(Y), pred(pred(Z)))&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(pred(X), pred(Y), Z)&#160;:-&#160;isMinus(X, Y, Z).<BR>isTimes(X, zero, zero).<BR>isTimes(zero, succ(Y), zero).<BR>isTimes(zero, pred(Y), zero).<BR>isTimes(succ(X), succ(Y), Z)&#160;:-&#160;','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).<BR>isTimes(succ(X), pred(Y), Z)&#160;:-&#160;','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).<BR>isTimes(pred(X), succ(Y), Z)&#160;:-&#160;','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).<BR>isTimes(pred(X), pred(Y), Z)&#160;:-&#160;','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).<BR>isDiv(zero, succ(Y), zero).<BR>isDiv(zero, pred(Y), zero).<BR>isDiv(succ(X), succ(Y), zero)&#160;:-&#160;isMinus(succ(X), succ(Y), pred(Z)).<BR>isDiv(succ(X), succ(Y), succ(Z))&#160;:-&#160;','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).<BR>isDiv(succ(X), pred(Y), Z)&#160;:-&#160;','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).<BR>isDiv(pred(X), pred(Y), zero)&#160;:-&#160;isMinus(pred(X), pred(Y), succ(Z)).<BR>isDiv(pred(X), pred(Y), succ(Z))&#160;:-&#160;','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).<BR>isDiv(pred(X), succ(Y), Z)&#160;:-&#160;','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).<BR>isModulo(X, Y, Z)&#160;:-&#160;','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).<BR>=(X, X).<BR><BR>Queries:<BR><BR>deriv(g,g,a).<BR><BR>Added facts for all undefined predicates.<BR><BR><pre>&#8627 Prolog</pre><pre>  &#8627 PredefinedPredicateTransformerProof</pre><pre>    &#8627 Prolog</pre><pre>      &#8627 CutEliminatorProof</pre><pre>        &#8627 Prolog</pre><pre>          &#8627 UndefinedPredicateHandlerProof</pre><pre>            &#8627 <B>Prolog</B></pre><pre>              &#8627 PrologToPiTRSProof</pre><BR>Clauses:<BR><BR>d(+(U, V), X, +(DU, DV))&#160;:-&#160;','(d(U, X, DU), d(V, X, DV)).<BR>d(-(U, V), X, -(DU, DV))&#160;:-&#160;','(d(U, X, DU), d(V, X, DV)).<BR>d(*(U, V), X, +(*(DU, V), *(U, DV)))&#160;:-&#160;','(d(U, X, DU), d(V, X, DV)).<BR>d(/(U, V), X, /(-(*(DU, V), *(U, DV)), ^(V, succ(succ(zero)))))&#160;:-&#160;','(d(U, X, DU), d(V, X, DV)).<BR>d(^(U, N), X, *(DU, *(N, ^(U, N1))))&#160;:-&#160;','(integer(N), ','(isMinus(N, succ(zero), U), ','(=(N1, U), d(U, X, DU)))).<BR>d(-(U), X, -(DU))&#160;:-&#160;d(U, X, DU).<BR>d(exp(U), X, *(exp(U), DU))&#160;:-&#160;d(U, X, DU).<BR>d(log(U), X, /(DU, U))&#160;:-&#160;d(U, X, DU).<BR>d(X, X, succ(zero))&#160;:-&#160;true.<BR>d(C, X, zero).<BR>main&#160;:-&#160;','(expression(X), ','(d(X, x, Y), write(Y))).<BR>expression(+(Exp, -(Exp, *(Exp, /(Exp, *(Exp, /(Exp, Exp)))))))&#160;:-&#160;value(Exp).<BR>value(/(+(*(succ(succ(succ(zero))), x), -(*(succ(succ(succ(succ(zero)))), *(exp(^(x, succ(succ(succ(zero))))), log(^(x, succ(succ(zero)))))), succ(succ(zero)))), +(-(*(succ(succ(succ(zero))), x)), /(succ(succ(succ(succ(succ(zero))))), +(exp(^(x, succ(succ(succ(succ(zero)))))), succ(succ(zero))))))).<BR>isPlus(zero, X, X).<BR>isPlus(succ(X), zero, succ(X)).<BR>isPlus(succ(X), succ(Y), succ(succ(Z)))&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(succ(X), pred(Y), Z)&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(pred(X), zero, pred(X)).<BR>isPlus(pred(X), succ(Y), Z)&#160;:-&#160;isPlus(X, Y, Z).<BR>isPlus(pred(X), pred(Y), pred(pred(Z)))&#160;:-&#160;isPlus(X, Y, Z).<BR>isMinus(X, zero, X).<BR>isMinus(zero, succ(Y), pred(Z))&#160;:-&#160;isMinus(zero, Y, Z).<BR>isMinus(zero, pred(Y), succ(Z))&#160;:-&#160;isMinus(zero, Y, Z).<BR>isMinus(succ(X), succ(Y), Z)&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(succ(X), pred(Y), succ(succ(Z)))&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(pred(X), succ(Y), pred(pred(Z)))&#160;:-&#160;isMinus(X, Y, Z).<BR>isMinus(pred(X), pred(Y), Z)&#160;:-&#160;isMinus(X, Y, Z).<BR>isTimes(X, zero, zero).<BR>isTimes(zero, succ(Y), zero).<BR>isTimes(zero, pred(Y), zero).<BR>isTimes(succ(X), succ(Y), Z)&#160;:-&#160;','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).<BR>isTimes(succ(X), pred(Y), Z)&#160;:-&#160;','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).<BR>isTimes(pred(X), succ(Y), Z)&#160;:-&#160;','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).<BR>isTimes(pred(X), pred(Y), Z)&#160;:-&#160;','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).<BR>isDiv(zero, succ(Y), zero).<BR>isDiv(zero, pred(Y), zero).<BR>isDiv(succ(X), succ(Y), zero)&#160;:-&#160;isMinus(succ(X), succ(Y), pred(Z)).<BR>isDiv(succ(X), succ(Y), succ(Z))&#160;:-&#160;','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).<BR>isDiv(succ(X), pred(Y), Z)&#160;:-&#160;','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).<BR>isDiv(pred(X), pred(Y), zero)&#160;:-&#160;isMinus(pred(X), pred(Y), succ(Z)).<BR>isDiv(pred(X), pred(Y), succ(Z))&#160;:-&#160;','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).<BR>isDiv(pred(X), succ(Y), Z)&#160;:-&#160;','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).<BR>isModulo(X, Y, Z)&#160;:-&#160;','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).<BR>=(X, X).<BR>integer(X0).<BR>true.<BR>write(X0).<BR><BR>Queries:<BR><BR>deriv(g,g,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 PredefinedPredicateTransformerProof</pre><pre>    &#8627 Prolog</pre><pre>      &#8627 CutEliminatorProof</pre><pre>        &#8627 Prolog</pre><pre>          &#8627 UndefinedPredicateHandlerProof</pre><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>

