YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   f(0()) -> s(0())
   f(s(0())) -> s(0())
   f(s(s(x))) -> f(f(s(x)))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [s](x0) = x0 + 24,
    
    [f](x0) = x0 + 15,
    
    [0] = 24
   orientation:
    f(0()) = 39 >= 48 = s(0())
    
    f(s(0())) = 63 >= 48 = s(0())
    
    f(s(s(x))) = x + 63 >= x + 54 = f(f(s(x)))
   problem:
    strict:
     f(0()) -> s(0())
    weak:
     f(s(0())) -> s(0())
     f(s(s(x))) -> f(f(s(x)))
   Bounds Processor:
    bound: 1
    enrichment: match-rt
    automaton:
     final states: {4}
     transitions:
      s1(7) -> 8*
      01() -> 7*
      f1(10) -> 11*
      f1(9) -> 10*
      f0(4) -> 4*
      00() -> 4*
      s0(4) -> 4*
      8 -> 11,10,9,4
      11 -> 4*
    problem:
     strict:
      
     weak:
      f(0()) -> s(0())
      f(s(0())) -> s(0())
      f(s(s(x))) -> f(f(s(x)))
    Qed