YES(?,PRIMREC)

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

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

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

 D > 1, D > +, D > *, D > -, D > minus, D > div, D > pow, D > 2,
 D > ln, t > D, t > 1, t > +, t > *, t > -, t > minus, t > div,
 t > pow, t > 2, t > ln, constant > D, constant > 1, constant > +,
 constant > *, constant > -, constant > minus, constant > div,
 constant > pow, constant > 2, constant > ln, 0 > D, 0 > 1, 0 > +,
 0 > *, 0 > -, 0 > minus, 0 > div, 0 > pow, 0 > 2, 0 > ln, + > 1,
 + > div, + > pow, + > 2, + > ln, * > 1, * > div, * > pow, * > 2,
 * > ln, - > 1, - > div, - > pow, - > 2, - > ln, minus > 1,
 minus > div, minus > pow, minus > 2, minus > ln, t ~ constant,
 t ~ 0, 1 ~ div, 1 ~ pow, 1 ~ 2, 1 ~ ln, constant ~ 0, + ~ *, + ~ -,
 + ~ minus, * ~ -, * ~ minus, - ~ minus, div ~ pow, div ~ 2,
 pow ~ 2, 2 ~ ln .

Hurray, we answered YES(?,PRIMREC)