Problem Mixed TRS jones6

YES(?,O(n^1))

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

Strict Trs:
  { f(a, empty()) -> g(a, empty())
  , f(a, cons(x, k)) -> f(cons(x, a), k)
  , g(empty(), d) -> d
  , g(cons(x, k), d) -> g(k, cons(x, d)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

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

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

     [f](x1, x2) = [2] x1 + [3] x2 + [2]
                                        
         [empty] = [2]
                      
     [g](x1, x2) = [2] x1 + [1] x2 + [1]
                                        
  [cons](x1, x2) = [1] x2 + [1]

This order satisfies following ordering constraints

     [f(a, empty())] = [2] a + [8]        
                     > [2] a + [3]        
                     = [g(a, empty())]    
                                          
  [f(a, cons(x, k))] = [2] a + [3] k + [5]
                     > [2] a + [3] k + [4]
                     = [f(cons(x, a), k)] 
                                          
     [g(empty(), d)] = [1] d + [5]        
                     > [1] d + [0]        
                     = [d]                
                                          
  [g(cons(x, k), d)] = [2] k + [1] d + [3]
                     > [2] k + [1] d + [2]
                     = [g(k, cons(x, d))] 
                                          

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

MAYBE

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

Strict Trs:
  { f(a, empty()) -> g(a, empty())
  , f(a, cons(x, k)) -> f(cons(x, a), k)
  , g(empty(), d) -> d
  , g(cons(x, k), d) -> g(k, cons(x, d)) }
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, empty()) -> g(a, empty())
  , f(a, cons(x, k)) -> f(cons(x, a), k)
  , g(empty(), d) -> d
  , g(cons(x, k), d) -> g(k, cons(x, d)) }
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, empty()) -> g(a, empty())
  , f(a, cons(x, k)) -> f(cons(x, a), k)
  , g(empty(), d) -> d
  , g(cons(x, k), d) -> g(k, cons(x, d)) }
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, empty()) -> g(a, empty())
  , f(a, cons(x, k)) -> f(cons(x, a), k)
  , g(empty(), d) -> d
  , g(cons(x, k), d) -> g(k, cons(x, d)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..