MAYBE Problem: f(y,f(x,y)) -> f(f(a(),y),f(a(),x)) Proof: DP Processor: DPs: f#(y,f(x,y)) -> f#(a(),x) f#(y,f(x,y)) -> f#(a(),y) f#(y,f(x,y)) -> f#(f(a(),y),f(a(),x)) TRS: f(y,f(x,y)) -> f(f(a(),y),f(a(),x)) Open