Problem Transformed CSR 04 Ex15 Luc06 GM

YES(?,O(n^3))

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

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

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

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

               [1 3 0]      [2]
  [a__f](x1) = [1 1 0] x1 + [3]
               [3 2 0]      [2]
                               
               [1 0 0]      [0]
     [f](x1) = [1 1 0] x1 + [2]
               [0 0 0]      [1]
                               
               [1]
         [a] = [1]
               [1]
                  
               [1 0 0]      [2]
     [g](x1) = [0 0 0] x1 + [0]
               [0 1 1]      [0]
                               
               [2 3 3]      [2]
  [mark](x1) = [0 1 0] x1 + [1]
               [3 2 3]      [0]

This order satisfies following ordering constraints

       [a__f(X)] = [1 3 0]     [2]  
                   [1 1 0] X + [3]  
                   [3 2 0]     [2]  
                 > [1 0 0]     [0]  
                   [1 1 0] X + [2]  
                   [0 0 0]     [1]  
                 = [f(X)]           
                                    
  [a__f(f(a()))] = [15]             
                   [8]              
                   [13]             
                 > [5]              
                   [6]              
                   [11]             
                 = [a__f(g(f(a())))]
                                    
    [mark(f(X))] = [5 3 0]     [11] 
                   [1 1 0] X + [3]  
                   [5 2 0]     [7]  
                 > [1 3 0]     [2]  
                   [1 1 0] X + [3]  
                   [3 2 0]     [2]  
                 = [a__f(X)]        
                                    
     [mark(a())] = [10]             
                   [2]              
                   [8]              
                 > [1]              
                   [1]              
                   [1]              
                 = [a()]            
                                    
    [mark(g(X))] = [2 3 3]     [6]  
                   [0 0 0] X + [1]  
                   [3 3 3]     [6]  
                 > [2 3 3]     [4]  
                   [0 0 0] X + [0]  
                   [3 3 3]     [1]  
                 = [g(mark(X))]     
                                    

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

MAYBE

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

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

The input cannot be shown compatible

Arrrr..