MAYBE Problem: f(f(s(x),0()),f(y,z)) -> f(f(y,z),f(y,s(z))) f(f(s(x),s(y)),f(z,w)) -> f(f(x,y),f(z,w)) Proof: DP Processor: DPs: f#(f(s(x),0()),f(y,z)) -> f#(y,s(z)) f#(f(s(x),0()),f(y,z)) -> f#(f(y,z),f(y,s(z))) f#(f(s(x),s(y)),f(z,w)) -> f#(x,y) f#(f(s(x),s(y)),f(z,w)) -> f#(f(x,y),f(z,w)) TRS: f(f(s(x),0()),f(y,z)) -> f(f(y,z),f(y,s(z))) f(f(s(x),s(y)),f(z,w)) -> f(f(x,y),f(z,w)) Open