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))
  EDG 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))
   graph:
    +#(x,s(y)) -> +#(x,y) -> +#(x,s(y)) -> +#(x,y)
    sum#(s(x)) -> +#(sum(x),s(x)) -> +#(x,s(y)) -> +#(x,y)
    sum#(s(x)) -> sum#(x) -> sum#(s(x)) -> sum#(x)
    sum#(s(x)) -> sum#(x) -> sum#(s(x)) -> +#(sum(x),s(x))
   Restore Modifier:
    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))
    SCC Processor:
     #sccs: 2
     #rules: 2
     #arcs: 4/9
     DPs:
      sum#(s(x)) -> sum#(x)
     TRS:
      sum(0()) -> 0()
      sum(s(x)) -> +(sum(x),s(x))
      +(x,0()) -> x
      +(x,s(y)) -> s(+(x,y))
     Open
     
     DPs:
      +#(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