Problem SK90 4.05

YES(?,O(n^2))

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

Strict Trs:
  { *(x, +(y, z)) -> +(*(x, y), *(x, z))
  , *(x, 1()) -> x
  , *(+(x, y), z) -> +(*(x, z), *(y, z))
  , *(1(), y) -> y }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^2))

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

This order satisfies following ordering constraints

  [*(x, +(y, z))] = 5 + 4*x + x*y + x*z + 2*y + 2*z
                  > 4 + 4*x + x*y + 2*y + x*z + 2*z
                  = [+(*(x, y), *(x, z))]          
                                                   
      [*(x, 1())] = 1 + 2*x                        
                  > x                              
                  = [x]                            
                                                   
  [*(+(x, y), z)] = 5 + 2*x + 2*y + 4*z + x*z + y*z
                  > 4 + 2*x + x*z + 4*z + 2*y + y*z
                  = [+(*(x, z), *(y, z))]          
                                                   
      [*(1(), y)] = 1 + 2*y                        
                  > y                              
                  = [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:
  { *(x, +(y, z)) -> +(*(x, y), *(x, z))
  , *(+(x, y), z) -> +(*(x, z), *(y, z))
  , *(x, 1()) -> x
  , *(1(), y) -> 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(*) = {}, safe(+) = {1, 2}, safe(1) = {}

and precedence

 empty .

Following symbols are considered recursive:

 {*}

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:
   { *(x,  +(; y,  z);) -> +(; *(x,  y;),  *(x,  z;))
   , *(+(; x,  y),  z;) -> +(; *(x,  z;),  *(y,  z;))
   , *(x,  1();) -> x
   , *(1(),  y;) -> 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:
  { *(x, +(y, z)) -> +(*(x, y), *(x, z))
  , *(+(x, y), z) -> +(*(x, z), *(y, z))
  , *(x, 1()) -> x
  , *(1(), y) -> y }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,PRIMREC)

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

 * > + .

Hurray, we answered YES(?,PRIMREC)

MAYBE

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

Strict Trs:
  { *(x, +(y, z)) -> +(*(x, y), *(x, z))
  , *(+(x, y), z) -> +(*(x, z), *(y, z))
  , *(x, 1()) -> x
  , *(1(), y) -> 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:
  { *(x, +(y, z)) -> +(*(x, y), *(x, z))
  , *(+(x, y), z) -> +(*(x, z), *(y, z))
  , *(x, 1()) -> x
  , *(1(), y) -> y }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..