MAYBE Problem: +(x,0()) -> x +(x,i(x)) -> 0() +(+(x,y),z) -> +(x,+(y,z)) *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(+(x,y),z) -> +(*(x,z),*(y,z)) Proof: DP Processor: DPs: +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) *#(x,+(y,z)) -> *#(x,z) *#(x,+(y,z)) -> *#(x,y) *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) *#(+(x,y),z) -> *#(y,z) *#(+(x,y),z) -> *#(x,z) *#(+(x,y),z) -> +#(*(x,z),*(y,z)) TRS: +(x,0()) -> x +(x,i(x)) -> 0() +(+(x,y),z) -> +(x,+(y,z)) *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(+(x,y),z) -> +(*(x,z),*(y,z)) Open