YES(?,ELEMENTARY)

We are left with following problem, upon which TcT provides the
certificate YES(?,ELEMENTARY).

Strict 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(exp(ALPHA, BETA)) ->
    plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))),
         times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA))))
  , dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,ELEMENTARY)

The input was oriented with the instance of 'Lightweight Multiset
Path Order' as induced by the safe mapping

 safe(dx) = {}, safe(one) = {}, safe(a) = {}, safe(zero) = {},
 safe(plus) = {1, 2}, safe(times) = {1, 2}, safe(minus) = {1, 2},
 safe(neg) = {1}, safe(div) = {1, 2}, safe(exp) = {1, 2},
 safe(two) = {}, safe(ln) = {1}

and precedence

 empty .

Following symbols are considered recursive:

 {dx}

The recursion depth is 1.

For your convenience, here are the satisfied ordering constraints:

                      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(exp(; ALPHA,  BETA);) > plus(; times(; BETA,                                                        
                                              times(; exp(; ALPHA,  minus(; BETA,  one())),  dx(ALPHA;))), 
                                      times(; exp(; ALPHA,  BETA),  times(; ln(; ALPHA),  dx(BETA;))))     
                                                                                                           
            dx(ln(; ALPHA);) > div(; dx(ALPHA;),  ALPHA)                                                   
                                                                                                           

Hurray, we answered YES(?,ELEMENTARY)