MAYBE

Problem:
 0(#()) -> #()
 +(#(),x) -> x
 +(x,#()) -> x
 +(0(x),0(y)) -> 0(+(x,y))
 +(0(x),1(y)) -> 1(+(x,y))
 +(1(x),0(y)) -> 1(+(x,y))
 +(0(x),j(y)) -> j(+(x,y))
 +(j(x),0(y)) -> j(+(x,y))
 +(1(x),1(y)) -> j(+(+(x,y),1(#())))
 +(j(x),j(y)) -> 1(+(+(x,y),j(#())))
 +(1(x),j(y)) -> 0(+(x,y))
 +(j(x),1(y)) -> 0(+(x,y))
 +(+(x,y),z) -> +(x,+(y,z))
 opp(#()) -> #()
 opp(0(x)) -> 0(opp(x))
 opp(1(x)) -> j(opp(x))
 opp(j(x)) -> 1(opp(x))
 -(x,y) -> +(x,opp(y))
 *(#(),x) -> #()
 *(0(x),y) -> 0(*(x,y))
 *(1(x),y) -> +(0(*(x,y)),y)
 *(j(x),y) -> -(0(*(x,y)),y)
 *(*(x,y),z) -> *(x,*(y,z))

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