YES(?,O(n^2))

Problem:
 f(a,empty()) -> g(a,empty())
 f(a,cons(x,k)) -> f(cons(x,a),k)
 g(empty(),d) -> d
 g(cons(x,k),d) -> g(k,cons(x,d))

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
                    [1 2]          [0]
   [cons](x0, x1) = [0 1]x0 + x1 + [1],
   
                 [1 1]          [1]
   [g](x0, x1) = [0 1]x0 + x1 + [0],
   
                 [1 2]     [1 4]     [1]
   [f](x0, x1) = [0 1]x0 + [0 1]x1 + [8],
   
             [1]
   [empty] = [6]
  orientation:
                  [1 2]    [26]    [1 1]    [2]               
   f(a,empty()) = [0 1]a + [14] >= [0 1]a + [6] = g(a,empty())
   
                    [1 2]    [1 4]    [1 6]    [5]    [1 2]    [1 4]    [1 4]    [3]                 
   f(a,cons(x,k)) = [0 1]a + [0 1]k + [0 1]x + [9] >= [0 1]a + [0 1]k + [0 1]x + [9] = f(cons(x,a),k)
   
                      [8]         
   g(empty(),d) = d + [6] >= d = d
   
                        [1 1]    [1 3]    [2]        [1 1]    [1 2]    [1]                 
   g(cons(x,k),d) = d + [0 1]k + [0 1]x + [1] >= d + [0 1]k + [0 1]x + [1] = g(k,cons(x,d))
  problem:
   
  Qed