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