Problem Mixed TRS jones1

YES(?,O(n^1))

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

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

The following argument positions are usable:
  Uargs(rev) = {}, Uargs(r1) = {}, Uargs(cons) = {}

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

       [rev](x1) = [3] x1 + [3]
                               
    [r1](x1, x2) = [2] x1 + [1] x2 + [1]
                                        
         [empty] = [0]
                      
  [cons](x1, x2) = [1] x2 + [2]

This order satisfies following ordering constraints

            [rev(ls)] = [3] ls + [3]       
                      > [2] ls + [1]       
                      = [r1(ls, empty())]  
                                           
     [r1(empty(), a)] = [1] a + [1]        
                      > [1] a + [0]        
                      = [a]                
                                           
  [r1(cons(x, k), a)] = [1] a + [2] k + [5]
                      > [1] a + [2] k + [3]
                      = [r1(k, cons(x, a))]
                                           

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

MAYBE

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

Strict Trs:
  { rev(ls) -> r1(ls, empty())
  , r1(empty(), a) -> a
  , r1(cons(x, k), a) -> r1(k, cons(x, 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:
  { rev(ls) -> r1(ls, empty())
  , r1(empty(), a) -> a
  , r1(cons(x, k), a) -> r1(k, cons(x, 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:
  { rev(ls) -> r1(ls, empty())
  , r1(empty(), a) -> a
  , r1(cons(x, k), a) -> r1(k, cons(x, a)) }
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:
  { rev(ls) -> r1(ls, empty())
  , r1(empty(), a) -> a
  , r1(cons(x, k), a) -> r1(k, cons(x, a)) }
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(rev) = {}, safe(r1) = {2}, safe(empty) = {},
 safe(cons) = {1, 2}

and precedence

 rev > r1 .

Following symbols are considered recursive:

 {rev, r1}

The recursion depth is 2.

For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:

 Strict DPs: 
 Weak DPs  : 
 Strict Trs:
   { rev(ls;) -> r1(ls; empty())
   , r1(empty(); a) -> a
   , r1(cons(; x,  k); a) -> r1(k; cons(; x,  a)) }
 Weak Trs  : 

Hurray, we answered YES(?,POLY)