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:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
                    [1 2]          [4]
   [cons](x0, x1) = [0 0]x0 + x1 + [9],
   
                     [1 2]          [1]
   [revtl](x0, x1) = [0 1]x0 + x1 + [6],
   
           [13]
   [nil] = [1 ],
   
               [1 8]     [15]
   [rev](x0) = [0 1]x0 + [8 ]
  orientation:
             [1 8]     [15]    [1 2]     [14]                  
   rev(xs) = [0 1]xs + [8 ] >= [0 1]xs + [7 ] = revtl(xs,nil())
   
                          [16]           
   revtl(nil(),ys) = ys + [7 ] >= ys = ys
   
                          [1 2]    [1 2]          [23]    [1 2]    [1 2]          [5 ]                       
   revtl(cons(x,xs),ys) = [0 0]x + [0 1]xs + ys + [15] >= [0 0]x + [0 1]xs + ys + [15] = revtl(xs,cons(x,ys))
  problem:
   
  Qed