YES Problem: f(g(x,y),f(y,y)) -> f(g(y,x),y) Proof: DP Processor: DPs: f#(g(x,y),f(y,y)) -> f#(g(y,x),y) TRS: f(g(x,y),f(y,y)) -> f(g(y,x),y) Usable Rule Processor: DPs: f#(g(x,y),f(y,y)) -> f#(g(y,x),y) TRS: Arctic Interpretation Processor: dimension: 1 usable rules: interpretation: [f#](x0, x1) = 1x0 + -4x1 + -16, [f](x0, x1) = 11x0 + x1 + 4, [g](x0, x1) = 1x0 + x1 + -7 orientation: f#(g(x,y),f(y,y)) = 2x + 7y + 0 >= 1x + 2y + -6 = f#(g(y,x),y) problem: DPs: TRS: Qed