MAYBE

Problem:
 minus(x,0()) -> x
 minus(s(x),s(y)) -> minus(x,y)
 double(0()) -> 0()
 double(s(x)) -> s(s(double(x)))
 plus(0(),y) -> y
 plus(s(x),y) -> s(plus(x,y))
 plus(s(x),y) -> plus(x,s(y))
 plus(s(x),y) -> s(plus(minus(x,y),double(y)))
 plus(s(plus(x,y)),z) -> s(plus(plus(x,y),z))

Proof:
 DP Processor:
  DPs:
   minus#(s(x),s(y)) -> minus#(x,y)
   double#(s(x)) -> double#(x)
   plus#(s(x),y) -> plus#(x,y)
   plus#(s(x),y) -> plus#(x,s(y))
   plus#(s(x),y) -> double#(y)
   plus#(s(x),y) -> minus#(x,y)
   plus#(s(x),y) -> plus#(minus(x,y),double(y))
   plus#(s(plus(x,y)),z) -> plus#(plus(x,y),z)
  TRS:
   minus(x,0()) -> x
   minus(s(x),s(y)) -> minus(x,y)
   double(0()) -> 0()
   double(s(x)) -> s(s(double(x)))
   plus(0(),y) -> y
   plus(s(x),y) -> s(plus(x,y))
   plus(s(x),y) -> plus(x,s(y))
   plus(s(x),y) -> s(plus(minus(x,y),double(y)))
   plus(s(plus(x,y)),z) -> s(plus(plus(x,y),z))
  Open