MAYBE

Problem:
 O(0()) -> 0()
 +(0(),x) -> x
 +(x,0()) -> x
 +(O(x),O(y)) -> O(+(x,y))
 +(O(x),I(y)) -> I(+(x,y))
 +(I(x),O(y)) -> I(+(x,y))
 +(I(x),I(y)) -> O(+(+(x,y),I(0())))
 *(0(),x) -> 0()
 *(x,0()) -> 0()
 *(O(x),y) -> O(*(x,y))
 *(I(x),y) -> +(O(*(x,y)),y)

Proof:
 DP Processor:
  DPs:
   +#(O(x),O(y)) -> +#(x,y)
   +#(O(x),O(y)) -> O#(+(x,y))
   +#(O(x),I(y)) -> +#(x,y)
   +#(I(x),O(y)) -> +#(x,y)
   +#(I(x),I(y)) -> +#(x,y)
   +#(I(x),I(y)) -> +#(+(x,y),I(0()))
   +#(I(x),I(y)) -> O#(+(+(x,y),I(0())))
   *#(O(x),y) -> *#(x,y)
   *#(O(x),y) -> O#(*(x,y))
   *#(I(x),y) -> *#(x,y)
   *#(I(x),y) -> O#(*(x,y))
   *#(I(x),y) -> +#(O(*(x,y)),y)
  TRS:
   O(0()) -> 0()
   +(0(),x) -> x
   +(x,0()) -> x
   +(O(x),O(y)) -> O(+(x,y))
   +(O(x),I(y)) -> I(+(x,y))
   +(I(x),O(y)) -> I(+(x,y))
   +(I(x),I(y)) -> O(+(+(x,y),I(0())))
   *(0(),x) -> 0()
   *(x,0()) -> 0()
   *(O(x),y) -> O(*(x,y))
   *(I(x),y) -> +(O(*(x,y)),y)
  Open