YES Problem: g(x,y) -> x g(x,y) -> y 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: g(x,y) -> x g(x,y) -> y f(s(x),y,y) -> f(y,x,s(x)) Usable Rule Processor: DPs: f#(s(x),y,y) -> f#(y,x,s(x)) TRS: Arctic Interpretation Processor: dimension: 1 usable rules: interpretation: [f#](x0, x1, x2) = 1x0 + 2x1 + x2 + -16, [s](x0) = 2x0 + 4 orientation: f#(s(x),y,y) = 3x + 2y + 5 >= 2x + 1y + 4 = f#(y,x,s(x)) problem: DPs: TRS: Qed