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