Problem Rubio 04 test4

YES(?,O(n^3))

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

Strict Trs:
  { f(a(), a()) -> f(a(), b())
  , f(a(), b()) -> f(s(a()), c())
  , f(s(X), c()) -> f(X, c())
  , f(c(), c()) -> f(a(), a()) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^3))

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

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

                [1 1 3]      [1 1 0]      [3]
  [f](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                [0 0 0]      [0 0 0]      [0]
                                             
                [1]
          [a] = [3]
                [0]
                   
                [2]
          [b] = [0]
                [0]
                   
                [0 1 1]      [1]
      [s](x1) = [1 0 3] x1 + [0]
                [0 0 0]      [0]
                                
                [0]
          [c] = [0]
                [3]

This order satisfies following ordering constraints

   [f(a(), a())] = [11]            
                   [0]             
                   [0]             
                 > [9]             
                   [0]             
                   [0]             
                 = [f(a(), b())]   
                                   
   [f(a(), b())] = [9]             
                   [0]             
                   [0]             
                 > [8]             
                   [0]             
                   [0]             
                 = [f(s(a()), c())]
                                   
  [f(s(X), c())] = [1 1 4]     [4] 
                   [0 0 0] X + [0] 
                   [0 0 0]     [0] 
                 > [1 1 3]     [3] 
                   [0 0 0] X + [0] 
                   [0 0 0]     [0] 
                 = [f(X, c())]     
                                   
   [f(c(), c())] = [12]            
                   [0]             
                   [0]             
                 > [11]            
                   [0]             
                   [0]             
                 = [f(a(), a())]   
                                   

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

MAYBE

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

Strict Trs:
  { f(a(), a()) -> f(a(), b())
  , f(a(), b()) -> f(s(a()), c())
  , f(s(X), c()) -> f(X, c())
  , f(c(), c()) -> f(a(), a()) }
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:
  { f(a(), a()) -> f(a(), b())
  , f(a(), b()) -> f(s(a()), c())
  , f(s(X), c()) -> f(X, c())
  , f(c(), c()) -> f(a(), a()) }
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:
  { f(a(), a()) -> f(a(), b())
  , f(a(), b()) -> f(s(a()), c())
  , f(s(X), c()) -> f(X, c())
  , f(c(), c()) -> f(a(), a()) }
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:
  { f(a(), a()) -> f(a(), b())
  , f(a(), b()) -> f(s(a()), c())
  , f(s(X), c()) -> f(X, c())
  , f(c(), c()) -> f(a(), a()) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..