YES(?,O(n^2))

Problem:
 rev(xs) -> revtl(xs,nil())
 revtl(nil(),ys) -> ys
 revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys))

Proof:
 Complexity Transformation Processor:
  strict:
   rev(xs) -> revtl(xs,nil())
   revtl(nil(),ys) -> ys
   revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [cons](x0, x1) = x0 + x1,
     
     [revtl](x0, x1) = x0 + x1,
     
     [nil] = 0,
     
     [rev](x0) = x0 + 1
    orientation:
     rev(xs) = xs + 1 >= xs = revtl(xs,nil())
     
     revtl(nil(),ys) = ys >= ys = ys
     
     revtl(cons(x,xs),ys) = x + xs + ys >= x + xs + ys = revtl(xs,cons(x,ys))
    problem:
     strict:
      revtl(nil(),ys) -> ys
      revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys))
     weak:
      rev(xs) -> revtl(xs,nil())
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [cons](x0, x1) = x0 + x1,
       
       [revtl](x0, x1) = x0 + x1,
       
       [nil] = 1,
       
       [rev](x0) = x0 + 1
      orientation:
       revtl(nil(),ys) = ys + 1 >= ys = ys
       
       revtl(cons(x,xs),ys) = x + xs + ys >= x + xs + ys = revtl(xs,cons(x,ys))
       
       rev(xs) = xs + 1 >= xs + 1 = revtl(xs,nil())
      problem:
       strict:
        revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys))
       weak:
        revtl(nil(),ys) -> ys
        rev(xs) -> revtl(xs,nil())
      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]
         [revtl](x0, x1) = [0 1]x0 + x1 + [1],
         
                 [0]
         [nil] = [0],
         
                     [1 1]     [0]
         [rev](x0) = [0 1]x0 + [1]
        orientation:
                                [1 0]    [1 1]          [1]    [1 0]    [1 1]          [0]                       
         revtl(cons(x,xs),ys) = [0 0]x + [0 1]xs + ys + [2] >= [0 0]x + [0 1]xs + ys + [2] = revtl(xs,cons(x,ys))
         
                                [0]           
         revtl(nil(),ys) = ys + [1] >= ys = ys
         
                   [1 1]     [0]    [1 1]     [0]                  
         rev(xs) = [0 1]xs + [1] >= [0 1]xs + [1] = revtl(xs,nil())
        problem:
         strict:
          
         weak:
          revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys))
          revtl(nil(),ys) -> ys
          rev(xs) -> revtl(xs,nil())
        Qed