YES Problem: +(*(x,y),*(x,z)) -> *(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u()) Proof: Matrix Interpretation Processor: dim=1 interpretation: [u] = 3, [+](x0, x1) = x0 + x1 + 1, [*](x0, x1) = 2x0 + x1 + 2 orientation: +(*(x,y),*(x,z)) = 4x + y + z + 5 >= 2x + y + z + 3 = *(x,+(y,z)) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) +(*(x,y),+(*(x,z),u())) = 4x + y + z + 9 >= 2x + y + z + 7 = +(*(x,+(y,z)),u()) 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