YES

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

Proof:
 DP Processor:
  DPs:
   f#(s(x)) -> g#(x,s(x))
   g#(s(x),y) -> +#(y,s(x))
   g#(s(x),y) -> g#(x,+(y,s(x)))
   +#(x,s(y)) -> +#(x,y)
   g#(s(x),y) -> +#(y,x)
   g#(s(x),y) -> g#(x,s(+(y,x)))
  TRS:
   f(0()) -> 1()
   f(s(x)) -> g(x,s(x))
   g(0(),y) -> y
   g(s(x),y) -> g(x,+(y,s(x)))
   +(x,0()) -> x
   +(x,s(y)) -> s(+(x,y))
   g(s(x),y) -> g(x,s(+(y,x)))
  Usable Rule Processor:
   DPs:
    f#(s(x)) -> g#(x,s(x))
    g#(s(x),y) -> +#(y,s(x))
    g#(s(x),y) -> g#(x,+(y,s(x)))
    +#(x,s(y)) -> +#(x,y)
    g#(s(x),y) -> +#(y,x)
    g#(s(x),y) -> g#(x,s(+(y,x)))
   TRS:
    +(x,s(y)) -> s(+(x,y))
    +(x,0()) -> x
   Matrix Interpretation Processor: dim=1
    
    usable rules:
     
    interpretation:
     [+#](x0, x1) = 5x1 + 1,
     
     [g#](x0, x1) = 5x0 + 6,
     
     [f#](x0) = 5x0 + 6,
     
     [+](x0, x1) = 4x0 + 4x1 + 4,
     
     [s](x0) = x0 + 5,
     
     [0] = 3
    orientation:
     f#(s(x)) = 5x + 31 >= 5x + 6 = g#(x,s(x))
     
     g#(s(x),y) = 5x + 31 >= 5x + 26 = +#(y,s(x))
     
     g#(s(x),y) = 5x + 31 >= 5x + 6 = g#(x,+(y,s(x)))
     
     +#(x,s(y)) = 5y + 26 >= 5y + 1 = +#(x,y)
     
     g#(s(x),y) = 5x + 31 >= 5x + 1 = +#(y,x)
     
     g#(s(x),y) = 5x + 31 >= 5x + 6 = g#(x,s(+(y,x)))
     
     +(x,s(y)) = 4x + 4y + 24 >= 4x + 4y + 9 = s(+(x,y))
     
     +(x,0()) = 4x + 16 >= x = x
    problem:
     DPs:
      
     TRS:
      +(x,s(y)) -> s(+(x,y))
      +(x,0()) -> x
    Qed