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