YES(?,O(n^2))

Problem:
 rev(ls) -> r1(ls,empty())
 r1(empty(),a) -> a
 r1(cons(x,k),a) -> r1(k,cons(x,a))

Proof:
 Complexity Transformation Processor:
  strict:
   rev(ls) -> r1(ls,empty())
   r1(empty(),a) -> a
   r1(cons(x,k),a) -> r1(k,cons(x,a))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [cons](x0, x1) = x0 + x1,
     
     [r1](x0, x1) = x0 + x1,
     
     [empty] = 0,
     
     [rev](x0) = x0 + 1
    orientation:
     rev(ls) = ls + 1 >= ls = r1(ls,empty())
     
     r1(empty(),a) = a >= a = a
     
     r1(cons(x,k),a) = a + k + x >= a + k + x = r1(k,cons(x,a))
    problem:
     strict:
      r1(empty(),a) -> a
      r1(cons(x,k),a) -> r1(k,cons(x,a))
     weak:
      rev(ls) -> r1(ls,empty())
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [cons](x0, x1) = x0 + x1,
       
       [r1](x0, x1) = x0 + x1,
       
       [empty] = 1,
       
       [rev](x0) = x0 + 1
      orientation:
       r1(empty(),a) = a + 1 >= a = a
       
       r1(cons(x,k),a) = a + k + x >= a + k + x = r1(k,cons(x,a))
       
       rev(ls) = ls + 1 >= ls + 1 = r1(ls,empty())
      problem:
       strict:
        r1(cons(x,k),a) -> r1(k,cons(x,a))
       weak:
        r1(empty(),a) -> a
        rev(ls) -> r1(ls,empty())
      Matrix Interpretation Processor:
       dimension: 2
       max_matrix:
        [1 1]
        [0 1]
        interpretation:
                          [1 0]          [0]
         [cons](x0, x1) = [0 0]x0 + x1 + [1],
         
                        [1 1]          [0]
         [r1](x0, x1) = [0 1]x0 + x1 + [1],
         
                   [0]
         [empty] = [0],
         
                     [1 1]     [0]
         [rev](x0) = [0 1]x0 + [1]
        orientation:
                               [1 1]    [1 0]    [1]        [1 1]    [1 0]    [0]                  
         r1(cons(x,k),a) = a + [0 1]k + [0 0]x + [2] >= a + [0 1]k + [0 0]x + [2] = r1(k,cons(x,a))
         
                             [0]         
         r1(empty(),a) = a + [1] >= a = a
         
                   [1 1]     [0]    [1 1]     [0]                 
         rev(ls) = [0 1]ls + [1] >= [0 1]ls + [1] = r1(ls,empty())
        problem:
         strict:
          
         weak:
          r1(cons(x,k),a) -> r1(k,cons(x,a))
          r1(empty(),a) -> a
          rev(ls) -> r1(ls,empty())
        Qed