Problem Maude 06 MYNAT nosorts

YES(?,O(n^2))

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

Strict Trs:
  { and(tt(), X) -> X
  , plus(N, 0()) -> N
  , plus(N, s(M)) -> s(plus(N, M))
  , x(N, 0()) -> 0()
  , x(N, s(M)) -> plus(x(N, M), N) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^2))

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

This order satisfies following ordering constraints

   [and(tt(), X)] = 1 + X              
                  > X                  
                  = [X]                
                                       
   [plus(N, 0())] = 1 + N              
                  > N                  
                  = [N]                
                                       
  [plus(N, s(M))] = 5 + N + 2*M        
                  > 3 + N + 2*M        
                  = [s(plus(N, M))]    
                                       
      [x(N, 0())] = 1 + 2*N            
                  >                    
                  = [0()]              
                                       
     [x(N, s(M))] = 3 + 6*N + 2*N*M + M
                  > 2 + 4*N + 2*N*M + M
                  = [plus(x(N, M), N)] 
                                       

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:
  { and(tt(), X) -> X
  , plus(N, 0()) -> N
  , plus(N, s(M)) -> s(plus(N, M))
  , x(N, 0()) -> 0()
  , x(N, s(M)) -> plus(x(N, M), N) }
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(and) = {}, safe(tt) = {}, safe(plus) = {1}, safe(0) = {},
 safe(s) = {1}, safe(x) = {}

and precedence

 x > plus .

Following symbols are considered recursive:

 {plus, x}

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:
   { and(tt(),  X;) -> X
   , plus(0(); N) -> N
   , plus(s(; M); N) -> s(; plus(M; N))
   , x(N,  0();) -> 0()
   , x(N,  s(; M);) -> plus(N; x(N,  M;)) }
 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:
  { and(tt(), X) -> X
  , plus(N, 0()) -> N
  , plus(N, s(M)) -> s(plus(N, M))
  , x(N, 0()) -> 0()
  , x(N, s(M)) -> plus(x(N, M), N) }
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, x > plus .

Hurray, we answered YES(?,PRIMREC)

YES(?,POLY)

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

Strict Trs:
  { and(tt(), X) -> X
  , plus(N, 0()) -> N
  , plus(N, s(M)) -> s(plus(N, M))
  , x(N, 0()) -> 0()
  , x(N, s(M)) -> plus(x(N, M), N) }
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(and) = {}, safe(tt) = {}, safe(plus) = {1}, safe(0) = {},
 safe(s) = {1}, safe(x) = {}

and precedence

 x > plus .

Following symbols are considered recursive:

 {plus, x}

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:
   { and(tt(),  X;) -> X
   , plus(0(); N) -> N
   , plus(s(; M); N) -> s(; plus(M; N))
   , x(N,  0();) -> 0()
   , x(N,  s(; M);) -> plus(N; x(N,  M;)) }
 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:
  { and(tt(), X) -> X
  , plus(N, 0()) -> N
  , plus(N, s(M)) -> s(plus(N, M))
  , x(N, 0()) -> 0()
  , x(N, s(M)) -> plus(x(N, M), N) }
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(and) = {}, safe(tt) = {}, safe(plus) = {1}, safe(0) = {},
 safe(s) = {1}, safe(x) = {}

and precedence

 x > plus .

Following symbols are considered recursive:

 {plus, x}

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:
   { and(tt(),  X;) -> X
   , plus(0(); N) -> N
   , plus(s(; M); N) -> s(; plus(M; N))
   , x(N,  0();) -> 0()
   , x(N,  s(; M);) -> plus(N; x(N,  M;)) }
 Weak Trs  : 

Hurray, we answered YES(?,POLY)