YES(?,POLY)

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

Strict Trs:
  { plus(x, 0()) -> x
  , plus(x, s(y)) -> s(plus(x, y))
  , d(0()) -> 0()
  , d(s(x)) -> s(s(d(x)))
  , q(0()) -> 0()
  , q(s(x)) -> s(plus(q(x), d(x))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,POLY)

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

 safe(plus) = {1}, safe(0) = {}, safe(s) = {1}, safe(d) = {},
 safe(q) = {}

and precedence

 q > plus, q > d, plus ~ d .

Following symbols are considered recursive:

 {plus, d, q}

The recursion depth is 2.

For your convenience, here are the satisfied ordering constraints:

     plus(0(); x) > x                      
                                           
  plus(s(; y); x) > s(; plus(y; x))        
                                           
          d(0();) > 0()                    
                                           
       d(s(; x);) > s(; s(; d(x;)))        
                                           
          q(0();) > 0()                    
                                           
       q(s(; x);) > s(; plus(d(x;); q(x;)))
                                           

Hurray, we answered YES(?,POLY)