Problem Der95 08

YES(?,O(n^2))

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

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)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^2))

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

This order satisfies following ordering constraints

         [D(t())] = 1                                            
                  >                                              
                  = [1()]                                        
                                                                 
  [D(constant())] = 1                                            
                  >                                              
                  = [0()]                                        
                                                                 
     [D(+(x, y))] = 9 + 8*x + 8*y + 2*x^2 + 2*x*y + 2*y*x + 2*y^2
                  > 4 + 2*x^2 + 2*y^2                            
                  = [+(D(x), D(y))]                              
                                                                 
     [D(*(x, y))] = 9 + 8*x + 8*y + 2*x^2 + 2*x*y + 2*y*x + 2*y^2
                  > 8 + y + 2*x^2 + x + 2*y^2                    
                  = [+(*(y, D(x)), *(x, D(y)))]                  
                                                                 
     [D(-(x, y))] = 9 + 8*x + 8*y + 2*x^2 + 2*x*y + 2*y*x + 2*y^2
                  > 4 + 2*x^2 + 2*y^2                            
                  = [-(D(x), D(y))]                              
                                                                 

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:
  { 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)) }
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(D) = {}, safe(t) = {}, safe(1) = {}, safe(constant) = {},
 safe(0) = {}, safe(+) = {1, 2}, safe(*) = {1, 2}, safe(-) = {1, 2}

and precedence

 empty .

Following symbols are considered recursive:

 {D}

The recursion depth is 1.

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

 Strict DPs: 
 Weak DPs  : 
 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;)) }
 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:
  { 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)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,PRIMREC)

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

 D > 1, D > +, D > *, D > -, constant > 0 .

Hurray, we answered YES(?,PRIMREC)

MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

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)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

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)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..