YES Problem: f(f(x,a()),y) -> f(f(a(),y),f(a(),x)) Proof: DP Processor: DPs: f#(f(x,a()),y) -> f#(a(),x) f#(f(x,a()),y) -> f#(a(),y) f#(f(x,a()),y) -> f#(f(a(),y),f(a(),x)) TRS: f(f(x,a()),y) -> f(f(a(),y),f(a(),x)) EDG Processor: DPs: f#(f(x,a()),y) -> f#(a(),x) f#(f(x,a()),y) -> f#(a(),y) f#(f(x,a()),y) -> f#(f(a(),y),f(a(),x)) TRS: f(f(x,a()),y) -> f(f(a(),y),f(a(),x)) graph: f#(f(x,a()),y) -> f#(f(a(),y),f(a(),x)) -> f#(f(x,a()),y) -> f#(a(),x) f#(f(x,a()),y) -> f#(f(a(),y),f(a(),x)) -> f#(f(x,a()),y) -> f#(a(),y) f#(f(x,a()),y) -> f#(f(a(),y),f(a(),x)) -> f#(f(x,a()),y) -> f#(f(a(),y),f(a(),x)) CDG Processor: DPs: f#(f(x,a()),y) -> f#(a(),x) f#(f(x,a()),y) -> f#(a(),y) f#(f(x,a()),y) -> f#(f(a(),y),f(a(),x)) TRS: f(f(x,a()),y) -> f(f(a(),y),f(a(),x)) graph: Qed