YES Problem: f(x,y) -> x g(a()) -> h(a(),b(),a()) i(x) -> f(x,x) h(x,x,y) -> g(x) Proof: Polynomial Interpretation Processor: dimension: 1 interpretation: [i](x0) = 7x0 + 7x0x0 + 5, [h](x0, x1, x2) = 4x0 + 5x1 + 2x2 + x1x1 + 1, [b] = 0, [g](x0) = 4x0 + x0x0, [a] = 4, [f](x0, x1) = 3x0 + 4x1 + 6x0x0 + x1x1 + 4 orientation: f(x,y) = 3x + 6x*x + 4y + y*y + 4 >= x = x g(a()) = 32 >= 25 = h(a(),b(),a()) i(x) = 7x + 7x*x + 5 >= 7x + 7x*x + 4 = f(x,x) h(x,x,y) = 9x + x*x + 2y + 1 >= 4x + x*x = g(x) problem: Qed