YES Problem: f(x,y) -> h(x,y) f(x,y) -> h(y,x) h(x,x) -> x Proof: Polynomial Interpretation Processor: dimension: 1 interpretation: [h](x0, x1) = 5x0 + 5x1 + 4, [f](x0, x1) = 5x0 + 5x1 + 5 orientation: f(x,y) = 5x + 5y + 5 >= 5x + 5y + 4 = h(x,y) f(x,y) = 5x + 5y + 5 >= 5x + 5y + 4 = h(y,x) h(x,x) = 10x + 4 >= x = x problem: Qed