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:
 RT 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
   interpretation:
    [cons](x0, x1) = x0 + x1 + 14,
    
    [revtl](x0, x1) = x0 + x1 + 20,
    
    [nil] = 0,
    
    [rev](x0) = x0 + 24
   orientation:
    rev(xs) = xs + 24 >= xs + 20 = revtl(xs,nil())
    
    revtl(nil(),ys) = ys + 20 >= ys = ys
    
    revtl(cons(x,xs),ys) = x + xs + ys + 34 >= x + xs + ys + 34 = revtl(xs,cons(x,ys))
   problem:
    strict:
     revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys))
    weak:
     rev(xs) -> revtl(xs,nil())
     revtl(nil(),ys) -> ys
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
                      [1 2]          [4]
     [cons](x0, x1) = [0 0]x0 + x1 + [1],
     
                       [1 1]       
     [revtl](x0, x1) = [0 1]x0 + x1,
     
             [4]
     [nil] = [0],
     
                 [1 8]     [4]
     [rev](x0) = [0 1]x0 + [8]
    orientation:
                            [1 2]    [1 1]          [5]    [1 2]    [1 1]          [4]                       
     revtl(cons(x,xs),ys) = [0 0]x + [0 1]xs + ys + [1] >= [0 0]x + [0 1]xs + ys + [1] = revtl(xs,cons(x,ys))
     
               [1 8]     [4]    [1 1]     [4]                  
     rev(xs) = [0 1]xs + [8] >= [0 1]xs + [0] = revtl(xs,nil())
     
                            [4]           
     revtl(nil(),ys) = ys + [0] >= ys = ys
    problem:
     strict:
      
     weak:
      revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys))
      rev(xs) -> revtl(xs,nil())
      revtl(nil(),ys) -> ys
    Qed