YES(?,PRIMREC)

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

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(?,PRIMREC)

The input was oriented with the instance of'multiset path order' as
induced by the precedence

 dx > one, dx > plus, dx > times, dx > minus, dx > neg, dx > div,
 dx > exp, dx > two, dx > ln, one > div, one > exp, one > two,
 one > ln, a > dx, a > one, a > zero, a > plus, a > times,
 a > minus, a > neg, a > div, a > exp, a > two, a > ln, zero > dx,
 zero > one, zero > plus, zero > times, zero > minus, zero > neg,
 zero > div, zero > exp, zero > two, zero > ln, plus > one,
 plus > div, plus > exp, plus > two, plus > ln, times > one,
 times > div, times > exp, times > two, times > ln, minus > one,
 minus > div, minus > exp, minus > two, minus > ln, neg > one,
 neg > div, neg > exp, neg > two, neg > ln, plus ~ times,
 plus ~ minus, plus ~ neg, times ~ minus, times ~ neg, minus ~ neg,
 div ~ exp, div ~ two, div ~ ln, exp ~ two, two ~ ln .

Hurray, we answered YES(?,PRIMREC)