YES Problem: f(s(x),y,y) -> f(y,x,s(x)) Proof: DP Processor: DPs: f#(s(x),y,y) -> f#(y,x,s(x)) TRS: f(s(x),y,y) -> f(y,x,s(x)) Arctic Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1, x2) = -1x0 + 2x1 + -8x2 + 0, [f](x0, x1, x2) = -6x0 + x1 + -8x2 + 0, [s](x0) = 8x0 + 8 orientation: f#(s(x),y,y) = 7x + 2y + 7 >= 2x + -1y + 0 = f#(y,x,s(x)) f(s(x),y,y) = 2x + y + 2 >= x + -6y + 0 = f(y,x,s(x)) problem: DPs: TRS: f(s(x),y,y) -> f(y,x,s(x)) Qed