YES(?,ELEMENTARY)

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

Strict Trs:
  { D(t()) -> 1()
  , D(constant()) -> 0()
  , D(+(x, y)) -> +(D(x), D(y))
  , D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
  , D(-(x, y)) -> -(D(x), D(y))
  , D(minus(x)) -> minus(D(x))
  , D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2())))
  , D(pow(x, y)) ->
    +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y)))
  , D(ln(x)) -> div(D(x), x) }
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(D) = {}, safe(t) = {}, safe(1) = {}, safe(constant) = {},
 safe(0) = {}, safe(+) = {1, 2}, safe(*) = {1, 2}, safe(-) = {1, 2},
 safe(minus) = {1}, safe(div) = {1, 2}, safe(pow) = {1, 2},
 safe(2) = {}, safe(ln) = {1}

and precedence

 empty .

Following symbols are considered recursive:

 {D}

The recursion depth is 1.

For your convenience, here are the satisfied ordering constraints:

           D(t();) > 1()                                                           
                                                                                   
    D(constant();) > 0()                                                           
                                                                                   
    D(+(; x,  y);) > +(; D(x;),  D(y;))                                            
                                                                                   
    D(*(; x,  y);) > +(; *(; y,  D(x;)),  *(; x,  D(y;)))                          
                                                                                   
    D(-(; x,  y);) > -(; D(x;),  D(y;))                                            
                                                                                   
    D(minus(; x);) > minus(; D(x;))                                                
                                                                                   
  D(div(; x,  y);) > -(; div(; D(x;),  y),  div(; *(; x,  D(y;)),  pow(; y,  2())))
                                                                                   
  D(pow(; x,  y);) > +(; *(; *(; y,  pow(; x,  -(; y,  1()))),  D(x;)),            
                         *(; *(; pow(; x,  y),  ln(; x)),  D(y;)))                 
                                                                                   
       D(ln(; x);) > div(; D(x;),  x)                                              
                                                                                   

Hurray, we answered YES(?,ELEMENTARY)