YES(?,O(n^2))

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

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^2))

The input was oriented with the instance of 'Small 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 satisfied ordering constraints:

              rev(ls;) > r1(ls; empty())     
                                             
        r1(empty(); a) > a                   
                                             
  r1(cons(; x,  k); a) > r1(k; cons(; x,  a))
                                             

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