YES
Left Termination proof of ../tpdb/LP/terminweb/combination/der.pl
Left Termination of the query pattern
der_in_4(g, g, a, a)
w.r.t. the given Prolog program could successfully be proven:
↳ Prolog
↳ PrologToPiTRSProof
Clauses:
der(d(e(t)), const(1)).
der(d(e(const(A))), const(0)).
der(d(e(+(X, Y))), +(DX, DY)) :- ','(der(d(e(X)), DX), der(d(e(Y)), DY)).
der(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) :- ','(der(d(e(X)), DX), der(d(e(Y)), DY)).
der(d(d(X)), DDX) :- ','(der(d(X), DX), der(d(e(DX)), DDX)).
Queries:
der(g,g,a,a).
We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
R is empty.
Pi is empty.
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ RisEmptyProof
Pi-finite rewrite system:
R is empty.
Pi is empty.
The TRS R is empty. Hence, termination is trivially proven.