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()))) Arctic Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = 2x1 + 4, [f](x0, x1) = 2x1 + 0, [a] = 1, [g](x0) = 2, [h](x0, x1) = x0 + 6 orientation: f#(g(h(x,y)),f(a(),a())) = 5 >= 4 = f#(y,a()) f#(g(h(x,y)),f(a(),a())) = 5 >= 4 = f#(h(x,x),g(f(y,a()))) f(g(h(x,y)),f(a(),a())) = 5 >= 4 = f(h(x,x),g(f(y,a()))) problem: DPs: TRS: f(g(h(x,y)),f(a(),a())) -> f(h(x,x),g(f(y,a()))) Qed