YES(?,PRIMREC)

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

Strict Trs:
  { +(0(), y) -> y
  , +(s(x), y) -> s(+(x, y))
  , +(p(x), y) -> p(+(x, y))
  , minus(0()) -> 0()
  , minus(s(x)) -> p(minus(x))
  , minus(p(x)) -> s(minus(x))
  , *(0(), y) -> 0()
  , *(s(x), y) -> +(*(x, y), y)
  , *(p(x), y) -> +(*(x, y), minus(y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,PRIMREC)

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

 + > s, + > p, + > minus, 0 > +, 0 > s, 0 > p, 0 > minus, minus > s,
 minus > p, * > +, * > s, * > p, * > minus, 0 ~ *, s ~ p .

Hurray, we answered YES(?,PRIMREC)