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:
 RT Transformation Processor:
  strict:
   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))
  weak:
   
  Bounds Processor:
   bound: 0
   enrichment: match-rt
   automaton:
    final states: {5}
    transitions:
     f0(5,5) -> 5*
     empty0() -> 5*
     g0(5,5) -> 5*
     cons0(5,5) -> 5*
   problem:
    strict:
     f(a,empty()) -> g(a,empty())
     f(a,cons(x,k)) -> f(cons(x,a),k)
     g(cons(x,k),d) -> g(k,cons(x,d))
    weak:
     g(empty(),d) -> d
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [cons](x0, x1) = x0 + x1 + 1,
     
     [g](x0, x1) = x0 + x1,
     
     [f](x0, x1) = x0 + x1 + 15,
     
     [empty] = 18
    orientation:
     f(a,empty()) = a + 33 >= a + 18 = g(a,empty())
     
     f(a,cons(x,k)) = a + k + x + 16 >= a + k + x + 16 = f(cons(x,a),k)
     
     g(cons(x,k),d) = d + k + x + 1 >= d + k + x + 1 = g(k,cons(x,d))
     
     g(empty(),d) = d + 18 >= d = d
    problem:
     strict:
      f(a,cons(x,k)) -> f(cons(x,a),k)
      g(cons(x,k),d) -> g(k,cons(x,d))
     weak:
      f(a,empty()) -> g(a,empty())
      g(empty(),d) -> d
    Matrix Interpretation Processor:
     dimension: 2
     interpretation:
                       [1 2]          [0]
      [cons](x0, x1) = [0 0]x0 + x1 + [1],
      
                    [1 1]          [1]
      [g](x0, x1) = [0 1]x0 + x1 + [0],
      
                    [1 1]     [1 1]  
      [f](x0, x1) = [0 1]x0 + [0 1]x1,
      
                [8]
      [empty] = [8]
     orientation:
                       [1 1]    [1 1]    [1 2]    [1]    [1 1]    [1 1]    [1 2]    [1]                 
      f(a,cons(x,k)) = [0 1]a + [0 1]k + [0 0]x + [1] >= [0 1]a + [0 1]k + [0 0]x + [1] = f(cons(x,a),k)
      
                           [1 1]    [1 2]    [2]        [1 1]    [1 2]    [1]                 
      g(cons(x,k),d) = d + [0 1]k + [0 0]x + [1] >= d + [0 1]k + [0 0]x + [1] = g(k,cons(x,d))
      
                     [1 1]    [16]    [1 1]    [9]               
      f(a,empty()) = [0 1]a + [8 ] >= [0 1]a + [8] = g(a,empty())
      
                         [17]         
      g(empty(),d) = d + [8 ] >= d = d
     problem:
      strict:
       f(a,cons(x,k)) -> f(cons(x,a),k)
      weak:
       g(cons(x,k),d) -> g(k,cons(x,d))
       f(a,empty()) -> g(a,empty())
       g(empty(),d) -> d
     Matrix Interpretation Processor:
      dimension: 2
      interpretation:
                        [1 0]          [0]
       [cons](x0, x1) = [0 0]x0 + x1 + [1],
       
                               [8]
       [g](x0, x1) = x0 + x1 + [0],
       
                          [1 4]     [0 ]
       [f](x0, x1) = x0 + [0 1]x1 + [12],
       
                 [11]
       [empty] = [2 ]
      orientation:
                            [1 4]    [1 0]    [4 ]        [1 4]    [1 0]    [0 ]                 
       f(a,cons(x,k)) = a + [0 1]k + [0 0]x + [13] >= a + [0 1]k + [0 0]x + [13] = f(cons(x,a),k)
       
                                [1 0]    [8]            [1 0]    [8]                 
       g(cons(x,k),d) = d + k + [0 0]x + [1] >= d + k + [0 0]x + [1] = g(k,cons(x,d))
       
                          [19]        [19]               
       f(a,empty()) = a + [14] >= a + [2 ] = g(a,empty())
       
                          [19]         
       g(empty(),d) = d + [2 ] >= d = d
      problem:
       strict:
        
       weak:
        f(a,cons(x,k)) -> f(cons(x,a),k)
        g(cons(x,k),d) -> g(k,cons(x,d))
        f(a,empty()) -> g(a,empty())
        g(empty(),d) -> d
      Qed