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