Problem Mixed TRS jones4

YES(?,O(n^1))

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

Strict Trs:
  { p(m, n, s(r)) -> p(m, r, n)
  , p(m, s(n), 0()) -> p(0(), n, m)
  , p(m, 0(), 0()) -> m }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The following argument positions are usable:
  Uargs(p) = {}, Uargs(s) = {}

TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).

  [p](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [3]
                                                  
          [s](x1) = [1] x1 + [1]
                                
              [0] = [0]

This order satisfies following ordering constraints

    [p(m, n, s(r))] = [1] m + [1] n + [1] r + [4]
                    > [1] m + [1] n + [1] r + [3]
                    = [p(m, r, n)]               
                                                 
  [p(m, s(n), 0())] = [1] m + [1] n + [4]        
                    > [1] m + [1] n + [3]        
                    = [p(0(), n, m)]             
                                                 
   [p(m, 0(), 0())] = [1] m + [3]                
                    > [1] m + [0]                
                    = [m]                        
                                                 

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

YES(?,ELEMENTARY)

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

Strict Trs:
  { p(m, n, s(r)) -> p(m, r, n)
  , p(m, s(n), 0()) -> p(0(), n, m)
  , p(m, 0(), 0()) -> m }
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(p) = {}, safe(s) = {1}, safe(0) = {}

and precedence

 empty .

Following symbols are considered recursive:

 {p}

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:
   { p(m,  n,  s(; r);) -> p(m,  r,  n;)
   , p(m,  s(; n),  0();) -> p(0(),  n,  m;)
   , p(m,  0(),  0();) -> 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:
  { p(m, n, s(r)) -> p(m, r, n)
  , p(m, s(n), 0()) -> p(0(), n, m)
  , p(m, 0(), 0()) -> m }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,PRIMREC)

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

 empty .

Hurray, we answered YES(?,PRIMREC)

YES(?,POLY)

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

Strict Trs:
  { p(m, n, s(r)) -> p(m, r, n)
  , p(m, s(n), 0()) -> p(0(), n, m)
  , p(m, 0(), 0()) -> m }
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(p) = {}, safe(s) = {1}, safe(0) = {}

and precedence

 empty .

Following symbols are considered recursive:

 {p}

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:
   { p(m,  n,  s(; r);) -> p(m,  r,  n;)
   , p(m,  s(; n),  0();) -> p(0(),  n,  m;)
   , p(m,  0(),  0();) -> 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:
  { p(m, n, s(r)) -> p(m, r, n)
  , p(m, s(n), 0()) -> p(0(), n, m)
  , p(m, 0(), 0()) -> m }
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(p) = {}, safe(s) = {1}, safe(0) = {}

and precedence

 empty .

Following symbols are considered recursive:

 {p}

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:
   { p(m,  n,  s(; r);) -> p(m,  r,  n;)
   , p(m,  s(; n),  0();) -> p(0(),  n,  m;)
   , p(m,  0(),  0();) -> m }
 Weak Trs  : 

Hurray, we answered YES(?,POLY)