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