Problem AG01 3.53b

YES(?,O(n^3))

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

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

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

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

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

This order satisfies following ordering constraints

         [g(x, y)] = [1 0 0]     [1 0 0]     [2] 
                     [0 2 0] x + [0 2 0] y + [0] 
                     [0 0 2]     [0 0 2]     [0] 
                   > [1 0 0]     [0]             
                     [0 1 0] x + [0]             
                     [0 0 1]     [0]             
                   = [x]                         
                                                 
         [g(x, y)] = [1 0 0]     [1 0 0]     [2] 
                     [0 2 0] x + [0 2 0] y + [0] 
                     [0 0 2]     [0 0 2]     [0] 
                   > [1 0 0]     [0]             
                     [0 1 0] y + [0]             
                     [0 0 1]     [0]             
                   = [y]                         
                                                 
   [f(x, y, s(z))] = [0 0 1]     [1 1 2]     [8] 
                     [0 0 2] x + [3 1 6] z + [12]
                     [0 0 0]     [0 0 0]     [0] 
                   > [1 1 2]     [6]             
                     [3 1 2] z + [5]             
                     [0 0 0]     [0]             
                   = [s(f(0(), 1(), z))]         
                                                 
  [f(0(), 1(), x)] = [1 1 2]     [3]             
                     [3 1 2] x + [2]             
                     [0 0 0]     [0]             
                   > [1 1 2]     [2]             
                     [3 1 2] x + [0]             
                     [0 0 0]     [0]             
                   = [f(s(x), x, x)]             
                                                 

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

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(0(), 1(), x) -> f(s(x), x, x)
  , f(x, y, s(z)) -> s(f(0(), 1(), z)) }
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(0(), 1(), x) -> f(s(x), x, x)
  , f(x, y, s(z)) -> s(f(0(), 1(), z)) }
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(0(), 1(), x) -> f(s(x), x, x)
  , f(x, y, s(z)) -> s(f(0(), 1(), z)) }
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(0(), 1(), x) -> f(s(x), x, x)
  , f(x, y, s(z)) -> s(f(0(), 1(), z)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..