YES(?,O(n^1))

Problem:
 f(0()) -> s(0())
 f(s(0())) -> s(s(0()))
 f(s(0())) -> *(s(s(0())),f(0()))
 f(+(x,s(0()))) -> +(s(s(0())),f(x))
 f(+(x,y)) -> *(f(x),f(y))

Proof:
 RT Transformation Processor:
  strict:
   f(0()) -> s(0())
   f(s(0())) -> s(s(0()))
   f(s(0())) -> *(s(s(0())),f(0()))
   f(+(x,s(0()))) -> +(s(s(0())),f(x))
   f(+(x,y)) -> *(f(x),f(y))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [+](x0, x1) = x0 + x1 + 20,
    
    [*](x0, x1) = x0 + x1,
    
    [s](x0) = x0,
    
    [f](x0) = x0,
    
    [0] = 0
   orientation:
    f(0()) = 0 >= 0 = s(0())
    
    f(s(0())) = 0 >= 0 = s(s(0()))
    
    f(s(0())) = 0 >= 0 = *(s(s(0())),f(0()))
    
    f(+(x,s(0()))) = x + 20 >= x + 20 = +(s(s(0())),f(x))
    
    f(+(x,y)) = x + y + 20 >= x + y = *(f(x),f(y))
   problem:
    strict:
     f(0()) -> s(0())
     f(s(0())) -> s(s(0()))
     f(s(0())) -> *(s(s(0())),f(0()))
     f(+(x,s(0()))) -> +(s(s(0())),f(x))
    weak:
     f(+(x,y)) -> *(f(x),f(y))
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [+](x0, x1) = x0 + x1 + 17,
     
     [*](x0, x1) = x0 + x1 + 8,
     
     [s](x0) = x0,
     
     [f](x0) = x0 + 4,
     
     [0] = 0
    orientation:
     f(0()) = 4 >= 0 = s(0())
     
     f(s(0())) = 4 >= 0 = s(s(0()))
     
     f(s(0())) = 4 >= 12 = *(s(s(0())),f(0()))
     
     f(+(x,s(0()))) = x + 21 >= x + 21 = +(s(s(0())),f(x))
     
     f(+(x,y)) = x + y + 21 >= x + y + 16 = *(f(x),f(y))
    problem:
     strict:
      f(s(0())) -> *(s(s(0())),f(0()))
      f(+(x,s(0()))) -> +(s(s(0())),f(x))
     weak:
      f(0()) -> s(0())
      f(s(0())) -> s(s(0()))
      f(+(x,y)) -> *(f(x),f(y))
    Bounds Processor:
     bound: 3
     enrichment: match-rt
     automaton:
      final states: {6}
      transitions:
       *3(54,53) -> 38*
       *1(22,25) -> 19,6
       *1(19,19) -> 19,6
       *1(19,31) -> 6*
       f3(30) -> 54*
       f3(27) -> 53*
       s1(20) -> 25,19,21
       s1(19) -> 31,19
       s1(21) -> 22*
       01() -> 20*
       f1(20) -> 25*
       f1(22) -> 19*
       f1(19) -> 31*
       f1(6) -> 19*
       +1(22,19) -> 19,6
       *2(27,38) -> 38,31,19
       *2(30,44) -> 38,31
       f0(6) -> 6*
       f2(30) -> 30*
       f2(27) -> 44*
       f2(22) -> 27*
       f2(19) -> 38*
       f2(28) -> 44*
       s0(6) -> 6*
       +2(30,27) -> 38,31,19
       00() -> 6*
       s2(29) -> 38,30
       s2(28) -> 44,29
       *0(6,6) -> 6*
       02() -> 28*
       +0(6,6) -> 6*
     problem:
      strict:
       f(s(0())) -> *(s(s(0())),f(0()))
      weak:
       f(+(x,s(0()))) -> +(s(s(0())),f(x))
       f(0()) -> s(0())
       f(s(0())) -> s(s(0()))
       f(+(x,y)) -> *(f(x),f(y))
     Bounds Processor:
      bound: 3
      enrichment: match-rt
      automaton:
       final states: {6}
       transitions:
        *3(32,31) -> 21*
        *1(14,12) -> 15,6
        *1(14,14) -> 6*
        *1(15,15) -> 15,6
        f3(20) -> 32*
        f3(22) -> 31*
        s1(12) -> 12,15
        s1(11) -> 15,12,13
        s1(13) -> 14*
        01() -> 11*
        f1(15) -> 12*
        f1(14) -> 14*
        f1(11) -> 12*
        f1(6) -> 15*
        +1(14,14) -> 6*
        +1(14,15) -> 15,6
        *2(22,22) -> 15*
        *2(22,21) -> 21,12,15
        *2(20,18) -> 21,12
        f0(6) -> 6*
        f2(20) -> 20*
        f2(15) -> 21*
        f2(22) -> 18*
        f2(17) -> 18*
        f2(14) -> 22*
        s0(6) -> 6*
        +2(20,22) -> 21,15,12
        00() -> 6*
        s2(17) -> 18,19
        s2(19) -> 20*
        s2(18) -> 21*
        *0(6,6) -> 6*
        02() -> 17*
        +0(6,6) -> 6*
      problem:
       strict:
        
       weak:
        f(s(0())) -> *(s(s(0())),f(0()))
        f(+(x,s(0()))) -> +(s(s(0())),f(x))
        f(0()) -> s(0())
        f(s(0())) -> s(s(0()))
        f(+(x,y)) -> *(f(x),f(y))
      Qed