MAYBE

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)))
  Open