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