YES Problem: f(x,g(x)) -> x f(x,h(y)) -> f(h(x),y) Proof: Matrix Interpretation Processor: dim=1 interpretation: [h](x0) = x0 + 4, [f](x0, x1) = 2x0 + 4x1 + 1, [g](x0) = 4x0 + 1 orientation: f(x,g(x)) = 18x + 5 >= x = x f(x,h(y)) = 2x + 4y + 17 >= 2x + 4y + 9 = f(h(x),y) problem: Qed