YES(?,O(n^2))
TRS:
 {f(x, f(a(), y)) -> f(a(), f(f(f(a(), x), h a()), y))}
 DUP: We consider a non-duplicating system.
  Trs:
   {f(x, f(a(), y)) -> f(a(), f(f(f(a(), x), h a()), y))}
  RLAB:
   Strict:
    {
     f([a,f])(x, f([a,f])(a(), y)) ->
     f([a,f])(a(), f([f,f])(f([f,h])(f([a,a])(a(), x), h(a) a()), y)),
     f([a,f])(x, f([a,h])(a(), y)) ->
     f([a,f])(a(), f([f,h])(f([f,h])(f([a,a])(a(), x), h(a) a()), y)),
     f([a,f])(x, f([a,a])(a(), y)) ->
     f([a,f])(a(), f([f,a])(f([f,h])(f([a,a])(a(), x), h(a) a()), y)),
     f([f,f])(x, f([a,f])(a(), y)) ->
     f([a,f])(a(), f([f,f])(f([f,h])(f([a,f])(a(), x), h(a) a()), y)),
     f([f,f])(x, f([a,h])(a(), y)) ->
     f([a,f])(a(), f([f,h])(f([f,h])(f([a,f])(a(), x), h(a) a()), y)),
     f([f,f])(x, f([a,a])(a(), y)) ->
     f([a,f])(a(), f([f,a])(f([f,h])(f([a,f])(a(), x), h(a) a()), y)),
     f([h,f])(x, f([a,f])(a(), y)) ->
     f([a,f])(a(), f([f,f])(f([f,h])(f([a,h])(a(), x), h(a) a()), y)),
     f([h,f])(x, f([a,h])(a(), y)) ->
     f([a,f])(a(), f([f,h])(f([f,h])(f([a,h])(a(), x), h(a) a()), y)),
     f([h,f])(x, f([a,a])(a(), y)) ->
     f([a,f])(a(), f([f,a])(f([f,h])(f([a,h])(a(), x), h(a) a()), y))
    }
   Weak:
    {}
   Matrix Interpretation:
    Interpretation class: triangular
          [0]
    [a] = [0]
    
           [X1]    [1 0][X1]   [0]
    [h(1)]([X0]) = [0 0][X0] + [0]
    
           [X3]  [X1]    [1 2][X3]   [1 2][X1]   [0]
    [f(7)]([X2], [X0]) = [0 0][X2] + [0 1][X0] + [0]
    
           [X3]  [X1]    [1 0][X3]   [1 2][X1]   [1]
    [f(6)]([X2], [X0]) = [0 0][X2] + [0 1][X0] + [2]
    
           [X3]  [X1]    [1 0][X3]   [1 1][X1]   [3]
    [f(5)]([X2], [X0]) = [0 0][X2] + [0 0][X0] + [0]
    
           [X3]  [X1]    [1 0][X3]   [1 2][X1]   [0]
    [f(4)]([X2], [X0]) = [0 0][X2] + [0 1][X0] + [1]
    
           [X3]  [X1]    [1 2][X3]   [1 2][X1]   [0]
    [f(3)]([X2], [X0]) = [0 0][X2] + [0 1][X0] + [0]
    
           [X3]  [X1]    [1 0][X3]   [1 0][X1]   [0]
    [f(2)]([X2], [X0]) = [0 0][X2] + [0 0][X0] + [0]
    
           [X3]  [X1]    [1 2][X3]   [1 2][X1]   [0]
    [f(0)]([X2], [X0]) = [0 0][X2] + [0 1][X0] + [1]
    
    
    Qed