Problem AG01 3.53a

YES(?,O(n^1))

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

Strict Trs:
  { g(x, y) -> x
  , g(x, y) -> y
  , f(s(x), y, y) -> f(y, x, s(x)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

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

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

      [g](x1, x2) = [2] x1 + [2] x2 + [2]
                                         
  [f](x1, x2, x3) = [1] x1 + [1] x2 + [1]
                                         
          [s](x1) = [1] x1 + [2]

This order satisfies following ordering constraints

        [g(x, y)] = [2] x + [2] y + [2]
                  > [1] x + [0]        
                  = [x]                
                                       
        [g(x, y)] = [2] x + [2] y + [2]
                  > [1] y + [0]        
                  = [y]                
                                       
  [f(s(x), y, y)] = [1] x + [1] y + [3]
                  > [1] x + [1] y + [1]
                  = [f(y, x, s(x))]    
                                       

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

MAYBE

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

Strict Trs:
  { g(x, y) -> x
  , g(x, y) -> y
  , f(s(x), y, y) -> f(y, x, s(x)) }
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:
  { g(x, y) -> x
  , g(x, y) -> y
  , f(s(x), y, y) -> f(y, x, s(x)) }
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:
  { g(x, y) -> x
  , g(x, y) -> y
  , f(s(x), y, y) -> f(y, x, s(x)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

YES(?,POLY)

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

Strict Trs:
  { g(x, y) -> x
  , g(x, y) -> y
  , f(s(x), y, y) -> f(y, x, s(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(g) = {}, safe(f) = {3}, safe(s) = {1}

and precedence

 empty .

Following symbols are considered recursive:

 {f}

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:
   { g(x,  y;) -> x
   , g(x,  y;) -> y
   , f(s(; x),  y; y) -> f(y,  x; s(; x)) }
 Weak Trs  : 

Hurray, we answered YES(?,POLY)