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