YES Problem: g(f(x,y),z) -> f(x,g(y,z)) g(h(x,y),z) -> g(x,f(y,z)) g(x,h(y,z)) -> h(g(x,y),z) Proof: Matrix Interpretation Processor: dim=1 interpretation: [h](x0, x1) = x0 + 7x1 + 4, [g](x0, x1) = x0 + 4x1, [f](x0, x1) = x0 + x1 + 1 orientation: g(f(x,y),z) = x + y + 4z + 1 >= x + y + 4z + 1 = f(x,g(y,z)) g(h(x,y),z) = x + 7y + 4z + 4 >= x + 4y + 4z + 4 = g(x,f(y,z)) g(x,h(y,z)) = x + 4y + 28z + 16 >= x + 4y + 7z + 4 = h(g(x,y),z) problem: g(f(x,y),z) -> f(x,g(y,z)) g(h(x,y),z) -> g(x,f(y,z)) Matrix Interpretation Processor: dim=1 interpretation: [h](x0, x1) = x0 + 4x1 + 1, [g](x0, x1) = x0 + x1 + 6, [f](x0, x1) = 4x0 + x1 orientation: g(f(x,y),z) = 4x + y + z + 6 >= 4x + y + z + 6 = f(x,g(y,z)) g(h(x,y),z) = x + 4y + z + 7 >= x + 4y + z + 6 = g(x,f(y,z)) problem: g(f(x,y),z) -> f(x,g(y,z)) Matrix Interpretation Processor: dim=3 interpretation: [1 1 0] [1 1 0] [g](x0, x1) = [0 0 1]x0 + [0 0 0]x1 [0 1 0] [0 0 0] , [1 0 0] [1 1 0] [0] [f](x0, x1) = [0 1 0]x0 + [0 0 1]x1 + [1] [0 1 0] [0 1 0] [1] orientation: [1 1 0] [1 1 1] [1 1 0] [1] [1 0 0] [1 1 1] [1 1 0] [0] g(f(x,y),z) = [0 1 0]x + [0 1 0]y + [0 0 0]z + [1] >= [0 1 0]x + [0 1 0]y + [0 0 0]z + [1] = f(x,g(y,z)) [0 1 0] [0 0 1] [0 0 0] [1] [0 1 0] [0 0 1] [0 0 0] [1] problem: Qed