(0) Obligation:

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))))).

Query: deriv(a,g,g)

(1) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:none

Compound Symbols:none

(3) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(4) BOUNDS(O(1), O(1))

(5) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:none

Compound Symbols:none