YES
Left Termination proof of ../tpdb/LP/talp/maria/deriv.pl
Left Termination of the query pattern
deriv_in_3(g, g, a)
w.r.t. the given Prolog program could successfully be proven:
↳ Prolog
↳ PredefinedPredicateTransformerProof
Clauses:
d(+(U, V), X, +(DU, DV)) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(-(U, V), X, -(DU, DV)) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(*(U, V), X, +(*(DU, V), *(U, DV))) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(/(U, V), X, /(-(*(DU, V), *(U, DV)), ^(V, 2))) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(^(U, N), X, *(DU, *(N, ^(U, N1)))) :- ','(!, ','(integer(N), ','(is(N1, -(N, 1)), d(U, X, DU)))).
d(-(U), X, -(DU)) :- ','(!, d(U, X, DU)).
d(exp(U), X, *(exp(U), DU)) :- ','(!, d(U, X, DU)).
d(log(U), X, /(DU, U)) :- ','(!, d(U, X, DU)).
d(X, X, 1) :- !.
d(C, X, 0).
main :- ','(expression(X), ','(d(X, x, Y), write(Y))).
expression(+(Exp, -(Exp, *(Exp, /(Exp, *(Exp, /(Exp, Exp))))))) :- value(Exp).
value(/(+(*(3, x), -(*(4, *(exp(^(x, 3)), log(^(x, 2)))), 2)), +(-(*(3, x)), /(5, +(exp(^(x, 4)), 2))))).
Queries:
deriv(g,g,a).
Added definitions of predefined predicates.
↳ Prolog
↳ PredefinedPredicateTransformerProof
↳ Prolog
↳ CutEliminatorProof
Clauses:
d(+(U, V), X, +(DU, DV)) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(-(U, V), X, -(DU, DV)) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(*(U, V), X, +(*(DU, V), *(U, DV))) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(/(U, V), X, /(-(*(DU, V), *(U, DV)), ^(V, succ(succ(zero))))) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(^(U, N), X, *(DU, *(N, ^(U, N1)))) :- ','(!, ','(integer(N), ','(','(isMinus(N, succ(zero), U), =(N1, U)), d(U, X, DU)))).
d(-(U), X, -(DU)) :- ','(!, d(U, X, DU)).
d(exp(U), X, *(exp(U), DU)) :- ','(!, d(U, X, DU)).
d(log(U), X, /(DU, U)) :- ','(!, d(U, X, DU)).
d(X, X, succ(zero)) :- !.
d(C, X, zero).
main :- ','(expression(X), ','(d(X, x, Y), write(Y))).
expression(+(Exp, -(Exp, *(Exp, /(Exp, *(Exp, /(Exp, Exp))))))) :- value(Exp).
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))))))).
isPlus(zero, X, X).
isPlus(succ(X), zero, succ(X)).
isPlus(succ(X), succ(Y), succ(succ(Z))) :- isPlus(X, Y, Z).
isPlus(succ(X), pred(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), zero, pred(X)).
isPlus(pred(X), succ(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), pred(Y), pred(pred(Z))) :- isPlus(X, Y, Z).
isMinus(X, zero, X).
isMinus(zero, succ(Y), pred(Z)) :- isMinus(zero, Y, Z).
isMinus(zero, pred(Y), succ(Z)) :- isMinus(zero, Y, Z).
isMinus(succ(X), succ(Y), Z) :- isMinus(X, Y, Z).
isMinus(succ(X), pred(Y), succ(succ(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), succ(Y), pred(pred(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), pred(Y), Z) :- isMinus(X, Y, Z).
isTimes(X, zero, zero).
isTimes(zero, succ(Y), zero).
isTimes(zero, pred(Y), zero).
isTimes(succ(X), succ(Y), Z) :- ','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).
isTimes(succ(X), pred(Y), Z) :- ','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).
isTimes(pred(X), succ(Y), Z) :- ','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).
isTimes(pred(X), pred(Y), Z) :- ','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).
isDiv(zero, succ(Y), zero).
isDiv(zero, pred(Y), zero).
isDiv(succ(X), succ(Y), zero) :- isMinus(succ(X), succ(Y), pred(Z)).
isDiv(succ(X), succ(Y), succ(Z)) :- ','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).
isDiv(succ(X), pred(Y), Z) :- ','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).
isDiv(pred(X), pred(Y), zero) :- isMinus(pred(X), pred(Y), succ(Z)).
isDiv(pred(X), pred(Y), succ(Z)) :- ','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).
isDiv(pred(X), succ(Y), Z) :- ','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).
isModulo(X, Y, Z) :- ','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).
=(X, X).
Queries:
deriv(g,g,a).
Eliminated all cuts by simply ignoring them.
↳ Prolog
↳ PredefinedPredicateTransformerProof
↳ Prolog
↳ CutEliminatorProof
↳ Prolog
↳ UndefinedPredicateHandlerProof
Clauses:
d(+(U, V), X, +(DU, DV)) :- ','(d(U, X, DU), d(V, X, DV)).
d(-(U, V), X, -(DU, DV)) :- ','(d(U, X, DU), d(V, X, DV)).
d(*(U, V), X, +(*(DU, V), *(U, DV))) :- ','(d(U, X, DU), d(V, X, DV)).
d(/(U, V), X, /(-(*(DU, V), *(U, DV)), ^(V, succ(succ(zero))))) :- ','(d(U, X, DU), d(V, X, DV)).
d(^(U, N), X, *(DU, *(N, ^(U, N1)))) :- ','(integer(N), ','(','(isMinus(N, succ(zero), U), =(N1, U)), d(U, X, DU))).
d(-(U), X, -(DU)) :- d(U, X, DU).
d(exp(U), X, *(exp(U), DU)) :- d(U, X, DU).
d(log(U), X, /(DU, U)) :- d(U, X, DU).
d(X, X, succ(zero)) :- true.
d(C, X, zero).
main :- ','(expression(X), ','(d(X, x, Y), write(Y))).
expression(+(Exp, -(Exp, *(Exp, /(Exp, *(Exp, /(Exp, Exp))))))) :- value(Exp).
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))))))).
isPlus(zero, X, X).
isPlus(succ(X), zero, succ(X)).
isPlus(succ(X), succ(Y), succ(succ(Z))) :- isPlus(X, Y, Z).
isPlus(succ(X), pred(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), zero, pred(X)).
isPlus(pred(X), succ(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), pred(Y), pred(pred(Z))) :- isPlus(X, Y, Z).
isMinus(X, zero, X).
isMinus(zero, succ(Y), pred(Z)) :- isMinus(zero, Y, Z).
isMinus(zero, pred(Y), succ(Z)) :- isMinus(zero, Y, Z).
isMinus(succ(X), succ(Y), Z) :- isMinus(X, Y, Z).
isMinus(succ(X), pred(Y), succ(succ(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), succ(Y), pred(pred(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), pred(Y), Z) :- isMinus(X, Y, Z).
isTimes(X, zero, zero).
isTimes(zero, succ(Y), zero).
isTimes(zero, pred(Y), zero).
isTimes(succ(X), succ(Y), Z) :- ','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).
isTimes(succ(X), pred(Y), Z) :- ','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).
isTimes(pred(X), succ(Y), Z) :- ','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).
isTimes(pred(X), pred(Y), Z) :- ','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).
isDiv(zero, succ(Y), zero).
isDiv(zero, pred(Y), zero).
isDiv(succ(X), succ(Y), zero) :- isMinus(succ(X), succ(Y), pred(Z)).
isDiv(succ(X), succ(Y), succ(Z)) :- ','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).
isDiv(succ(X), pred(Y), Z) :- ','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).
isDiv(pred(X), pred(Y), zero) :- isMinus(pred(X), pred(Y), succ(Z)).
isDiv(pred(X), pred(Y), succ(Z)) :- ','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).
isDiv(pred(X), succ(Y), Z) :- ','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).
isModulo(X, Y, Z) :- ','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).
=(X, X).
Queries:
deriv(g,g,a).
Added facts for all undefined predicates.
↳ Prolog
↳ PredefinedPredicateTransformerProof
↳ Prolog
↳ CutEliminatorProof
↳ Prolog
↳ UndefinedPredicateHandlerProof
↳ Prolog
↳ PrologToPiTRSProof
Clauses:
d(+(U, V), X, +(DU, DV)) :- ','(d(U, X, DU), d(V, X, DV)).
d(-(U, V), X, -(DU, DV)) :- ','(d(U, X, DU), d(V, X, DV)).
d(*(U, V), X, +(*(DU, V), *(U, DV))) :- ','(d(U, X, DU), d(V, X, DV)).
d(/(U, V), X, /(-(*(DU, V), *(U, DV)), ^(V, succ(succ(zero))))) :- ','(d(U, X, DU), d(V, X, DV)).
d(^(U, N), X, *(DU, *(N, ^(U, N1)))) :- ','(integer(N), ','(isMinus(N, succ(zero), U), ','(=(N1, U), d(U, X, DU)))).
d(-(U), X, -(DU)) :- d(U, X, DU).
d(exp(U), X, *(exp(U), DU)) :- d(U, X, DU).
d(log(U), X, /(DU, U)) :- d(U, X, DU).
d(X, X, succ(zero)) :- true.
d(C, X, zero).
main :- ','(expression(X), ','(d(X, x, Y), write(Y))).
expression(+(Exp, -(Exp, *(Exp, /(Exp, *(Exp, /(Exp, Exp))))))) :- value(Exp).
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))))))).
isPlus(zero, X, X).
isPlus(succ(X), zero, succ(X)).
isPlus(succ(X), succ(Y), succ(succ(Z))) :- isPlus(X, Y, Z).
isPlus(succ(X), pred(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), zero, pred(X)).
isPlus(pred(X), succ(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), pred(Y), pred(pred(Z))) :- isPlus(X, Y, Z).
isMinus(X, zero, X).
isMinus(zero, succ(Y), pred(Z)) :- isMinus(zero, Y, Z).
isMinus(zero, pred(Y), succ(Z)) :- isMinus(zero, Y, Z).
isMinus(succ(X), succ(Y), Z) :- isMinus(X, Y, Z).
isMinus(succ(X), pred(Y), succ(succ(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), succ(Y), pred(pred(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), pred(Y), Z) :- isMinus(X, Y, Z).
isTimes(X, zero, zero).
isTimes(zero, succ(Y), zero).
isTimes(zero, pred(Y), zero).
isTimes(succ(X), succ(Y), Z) :- ','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).
isTimes(succ(X), pred(Y), Z) :- ','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).
isTimes(pred(X), succ(Y), Z) :- ','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).
isTimes(pred(X), pred(Y), Z) :- ','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).
isDiv(zero, succ(Y), zero).
isDiv(zero, pred(Y), zero).
isDiv(succ(X), succ(Y), zero) :- isMinus(succ(X), succ(Y), pred(Z)).
isDiv(succ(X), succ(Y), succ(Z)) :- ','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).
isDiv(succ(X), pred(Y), Z) :- ','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).
isDiv(pred(X), pred(Y), zero) :- isMinus(pred(X), pred(Y), succ(Z)).
isDiv(pred(X), pred(Y), succ(Z)) :- ','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).
isDiv(pred(X), succ(Y), Z) :- ','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).
isModulo(X, Y, Z) :- ','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).
=(X, X).
integer(X0).
true.
write(X0).
Queries:
deriv(g,g,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
↳ PredefinedPredicateTransformerProof
↳ Prolog
↳ CutEliminatorProof
↳ Prolog
↳ UndefinedPredicateHandlerProof
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ RisEmptyProof
Pi-finite rewrite system:
R is empty.
Pi is empty.
The TRS R is empty. Hence, termination is trivially proven.