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