YES Problem: f(x,y) -> h(x,y) f(x,y) -> h(y,x) h(x,x) -> x Proof: DP Processor: DPs: f#(x,y) -> h#(x,y) f#(x,y) -> h#(y,x) TRS: f(x,y) -> h(x,y) f(x,y) -> h(y,x) h(x,x) -> x Arctic Interpretation Processor: dimension: 1 interpretation: [h#](x0, x1) = 4x0 + x1 + -14, [f#](x0, x1) = 5x0 + 5x1 + 0, [h](x0, x1) = 8x0 + -9x1 + 8, [f](x0, x1) = 9x0 + 9x1 + 12 orientation: f#(x,y) = 5x + 5y + 0 >= 4x + y + -14 = h#(x,y) f#(x,y) = 5x + 5y + 0 >= x + 4y + -14 = h#(y,x) f(x,y) = 9x + 9y + 12 >= 8x + -9y + 8 = h(x,y) f(x,y) = 9x + 9y + 12 >= -9x + 8y + 8 = h(y,x) h(x,x) = 8x + 8 >= x = x problem: DPs: TRS: f(x,y) -> h(x,y) f(x,y) -> h(y,x) h(x,x) -> x Qed