Problem TCT 09 ma4

YES(?,O(n^2))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).

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(?,O(n^2))

The following argument positions are usable:
  Uargs(plus) = {1, 2}, Uargs(s) = {1}, Uargs(d) = {}, Uargs(q) = {}
TcT has computed following constructor-restricted polynomial
interpretation.
[plus](x1, x2) = x1 + 3*x2        
                                  
         [0]() = 1                
                                  
       [s](x1) = 3 + x1           
                                  
       [d](x1) = 3*x1             
                                  
       [q](x1) = 1 + 2*x1 + 3*x1^2
                                  

This order satisfies following ordering constraints

   [plus(x, 0())] = x + 3                
                  > x                    
                  = [x]                  
                                         
  [plus(x, s(y))] = x + 9 + 3*y          
                  > 3 + x + 3*y          
                  = [s(plus(x, y))]      
                                         
         [d(0())] = 3                    
                  > 1                    
                  = [0()]                
                                         
        [d(s(x))] = 9 + 3*x              
                  > 6 + 3*x              
                  = [s(s(d(x)))]         
                                         
         [q(0())] = 6                    
                  > 1                    
                  = [0()]                
                                         
        [q(s(x))] = 34 + 20*x + 3*x^2    
                  > 4 + 11*x + 3*x^2     
                  = [s(plus(q(x), d(x)))]
                                         

Hurray, we answered YES(?,O(n^2))

YES(?,ELEMENTARY)

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

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

The input was oriented with the instance of 'Lightweight Multiset
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 .

Following symbols are considered recursive:

 {plus, d, q}

The recursion depth is 2.

For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:

 Strict DPs: 
 Weak DPs  : 
 Strict Trs:
   { 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;))) }
 Weak Trs  : 

Hurray, we answered YES(?,ELEMENTARY)

YES(?,PRIMREC)

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

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

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

 plus > s, d > s, q > plus, q > s, q > d .

Hurray, we answered YES(?,PRIMREC)

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 .

Following symbols are considered recursive:

 {plus, d, q}

The recursion depth is 2.

For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:

 Strict DPs: 
 Weak DPs  : 
 Strict Trs:
   { 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;))) }
 Weak Trs  : 

Hurray, we answered YES(?,POLY)

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
(PS)' as induced by the safe mapping

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

and precedence

 q > plus, q > d .

Following symbols are considered recursive:

 {plus, d, q}

The recursion depth is 2.

For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:

 Strict DPs: 
 Weak DPs  : 
 Strict Trs:
   { 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;))) }
 Weak Trs  : 

Hurray, we answered YES(?,POLY)