MAYBE

Problem:
 dx(X) -> one()
 dx(a()) -> zero()
 dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
 dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
 dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
 dx(neg(ALPHA)) -> neg(dx(ALPHA))
 dx(div(ALPHA,BETA)) -> minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
 dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA)
 dx(exp(ALPHA,BETA)) ->
 plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA))),times
                                                                (exp(ALPHA,BETA),
                                                                 times
                                                                 (ln(ALPHA),dx(BETA))))

Proof:
 DP Processor:
  DPs:
   dx#(plus(ALPHA,BETA)) -> dx#(BETA)
   dx#(plus(ALPHA,BETA)) -> dx#(ALPHA)
   dx#(times(ALPHA,BETA)) -> dx#(BETA)
   dx#(times(ALPHA,BETA)) -> dx#(ALPHA)
   dx#(minus(ALPHA,BETA)) -> dx#(BETA)
   dx#(minus(ALPHA,BETA)) -> dx#(ALPHA)
   dx#(neg(ALPHA)) -> dx#(ALPHA)
   dx#(div(ALPHA,BETA)) -> dx#(BETA)
   dx#(div(ALPHA,BETA)) -> dx#(ALPHA)
   dx#(ln(ALPHA)) -> dx#(ALPHA)
   dx#(exp(ALPHA,BETA)) -> dx#(BETA)
   dx#(exp(ALPHA,BETA)) -> dx#(ALPHA)
  TRS:
   dx(X) -> one()
   dx(a()) -> zero()
   dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
   dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
   dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
   dx(neg(ALPHA)) -> neg(dx(ALPHA))
   dx(div(ALPHA,BETA)) -> minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
   dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA)
   dx(exp(ALPHA,BETA)) ->
   plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA))),times
                                                                  (exp(ALPHA,BETA),
                                                                   times
                                                                   (ln(ALPHA),dx(BETA))))
  SCC Processor:
   #sccs: 1
   #rules: 12
   #arcs: 144/144
   DPs:
    dx#(plus(ALPHA,BETA)) -> dx#(BETA)
    dx#(plus(ALPHA,BETA)) -> dx#(ALPHA)
    dx#(times(ALPHA,BETA)) -> dx#(BETA)
    dx#(times(ALPHA,BETA)) -> dx#(ALPHA)
    dx#(minus(ALPHA,BETA)) -> dx#(BETA)
    dx#(minus(ALPHA,BETA)) -> dx#(ALPHA)
    dx#(neg(ALPHA)) -> dx#(ALPHA)
    dx#(div(ALPHA,BETA)) -> dx#(BETA)
    dx#(div(ALPHA,BETA)) -> dx#(ALPHA)
    dx#(ln(ALPHA)) -> dx#(ALPHA)
    dx#(exp(ALPHA,BETA)) -> dx#(BETA)
    dx#(exp(ALPHA,BETA)) -> dx#(ALPHA)
   TRS:
    dx(X) -> one()
    dx(a()) -> zero()
    dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
    dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
    dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
    dx(neg(ALPHA)) -> neg(dx(ALPHA))
    dx(div(ALPHA,BETA)) -> minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
    dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA)
    dx(exp(ALPHA,BETA)) ->
    plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA))),times
                                                                   (exp(ALPHA,BETA),
                                                                    times
                                                                    (ln(ALPHA),dx(BETA))))
   Open