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:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
                    [1 5]          [1]
   [cons](x0, x1) = [0 1]x0 + x1 + [1],
   
                  [1 1]          [1]
   [r1](x0, x1) = [0 1]x0 + x1 + [0],
   
             [7]
   [empty] = [8],
   
               [1 2]     [9 ]
   [rev](x0) = [0 1]x0 + [12]
  orientation:
             [1 2]     [9 ]    [1 1]     [8]                 
   rev(ls) = [0 1]ls + [12] >= [0 1]ls + [8] = r1(ls,empty())
   
                       [16]         
   r1(empty(),a) = a + [8 ] >= a = a
   
                         [1 1]    [1 6]    [3]        [1 1]    [1 5]    [2]                  
   r1(cons(x,k),a) = a + [0 1]k + [0 1]x + [1] >= a + [0 1]k + [0 1]x + [1] = r1(k,cons(x,a))
  problem:
   
  Qed