YES

Problem:
 f(empty(),l) -> l
 f(cons(x,k),l) -> g(k,l,cons(x,k))
 g(a,b,c) -> f(a,cons(b,c))

Proof:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [g](x0, x1, x2) = 4x0 + x1 + 2x2 + 5,
   
   [cons](x0, x1) = x0 + 2x1 + 1,
   
   [f](x0, x1) = 4x0 + x1 + 4,
   
   [empty] = 4
  orientation:
   f(empty(),l) = l + 20 >= l = l
   
   f(cons(x,k),l) = 8k + l + 4x + 8 >= 8k + l + 2x + 7 = g(k,l,cons(x,k))
   
   g(a,b,c) = 4a + b + 2c + 5 >= 4a + b + 2c + 5 = f(a,cons(b,c))
  problem:
   g(a,b,c) -> f(a,cons(b,c))
  Matrix Interpretation Processor: dim=3
   
   interpretation:
                      [1 0 0]     [1 0 0]     [1 0 0]     [1]
    [g](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 + [0]
                      [0 0 0]     [0 0 0]     [0 0 0]     [0],
    
                     [1 0 0]     [1 0 0]  
    [cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                     [0 0 0]     [0 0 0]  ,
    
                  [1 0 0]     [1 0 0]  
    [f](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                  [0 0 0]     [0 0 0]  
   orientation:
               [1 0 0]    [1 0 0]    [1 0 0]    [1]    [1 0 0]    [1 0 0]    [1 0 0]                  
    g(a,b,c) = [0 0 0]a + [0 0 0]b + [0 0 0]c + [0] >= [0 0 0]a + [0 0 0]b + [0 0 0]c = f(a,cons(b,c))
               [0 0 0]    [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0 0 0]                  
   problem:
    
   Qed