MAYBE

Problem:
 +(x,0()) -> x
 +(minus(x),x) -> 0()
 minus(0()) -> 0()
 minus(minus(x)) -> x
 minus(+(x,y)) -> +(minus(y),minus(x))
 *(x,1()) -> x
 *(x,0()) -> 0()
 *(x,+(y,z)) -> +(*(x,y),*(x,z))
 *(x,minus(y)) -> minus(*(x,y))

Proof:
 DP Processor:
  DPs:
   minus#(+(x,y)) -> minus#(x)
   minus#(+(x,y)) -> minus#(y)
   minus#(+(x,y)) -> +#(minus(y),minus(x))
   *#(x,+(y,z)) -> *#(x,z)
   *#(x,+(y,z)) -> *#(x,y)
   *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
   *#(x,minus(y)) -> *#(x,y)
   *#(x,minus(y)) -> minus#(*(x,y))
  TRS:
   +(x,0()) -> x
   +(minus(x),x) -> 0()
   minus(0()) -> 0()
   minus(minus(x)) -> x
   minus(+(x,y)) -> +(minus(y),minus(x))
   *(x,1()) -> x
   *(x,0()) -> 0()
   *(x,+(y,z)) -> +(*(x,y),*(x,z))
   *(x,minus(y)) -> minus(*(x,y))
  Open