YES(?,O(n^1))

Problem:
 f(f(x)) -> f(x)
 f(s(x)) -> f(x)
 g(s(0())) -> g(f(s(0())))

Proof:
 RT Transformation Processor:
  strict:
   f(f(x)) -> f(x)
   f(s(x)) -> f(x)
   g(s(0())) -> g(f(s(0())))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [g](x0) = x0,
    
    [0] = 4,
    
    [s](x0) = x0 + 18,
    
    [f](x0) = x0 + 4
   orientation:
    f(f(x)) = x + 8 >= x + 4 = f(x)
    
    f(s(x)) = x + 22 >= x + 4 = f(x)
    
    g(s(0())) = 22 >= 26 = g(f(s(0())))
   problem:
    strict:
     g(s(0())) -> g(f(s(0())))
    weak:
     f(f(x)) -> f(x)
     f(s(x)) -> f(x)
   Bounds Processor:
    bound: 1
    enrichment: match-rt
    automaton:
     final states: {5}
     transitions:
      g1(12) -> 13*
      f1(14) -> 15*
      f1(11) -> 12*
      s1(10) -> 11*
      01() -> 10*
      g0(5) -> 5*
      s0(5) -> 5*
      00() -> 5*
      f0(5) -> 5*
      10 -> 14*
      13 -> 5*
      15 -> 12*
    problem:
     strict:
      
     weak:
      g(s(0())) -> g(f(s(0())))
      f(f(x)) -> f(x)
      f(s(x)) -> f(x)
    Qed