MAYBE

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

Proof:
 DP Processor:
  DPs:
   sum#(s(x)) -> sum#(x)
   sum#(s(x)) -> +#(sum(x),s(x))
   +#(x,s(y)) -> +#(x,y)
  TRS:
   sum(0()) -> 0()
   sum(s(x)) -> +(sum(x),s(x))
   +(x,0()) -> x
   +(x,s(y)) -> s(+(x,y))
  Open