YES(?,O(n^2)) Problem: +(x,+(y,z)) -> +(+(x,y),z) +(*(x,y),+(x,z)) -> *(x,+(y,z)) +(*(x,y),+(*(x,z),u)) -> +(*(x,+(y,z)),u) Proof: Complexity Transformation Processor: strict: +(x,+(y,z)) -> +(+(x,y),z) +(*(x,y),+(x,z)) -> *(x,+(y,z)) +(*(x,y),+(*(x,z),u)) -> +(*(x,+(y,z)),u) weak: Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [*](x0, x1) = x0 + x1 + 1, [+](x0, x1) = x0 + x1 orientation: +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z) +(*(x,y),+(x,z)) = 2x + y + z + 1 >= x + y + z + 1 = *(x,+(y,z)) +(*(x,y),+(*(x,z),u)) = u + 2x + y + z + 2 >= u + x + y + z + 1 = +(*(x,+(y,z)),u) problem: strict: +(x,+(y,z)) -> +(+(x,y),z) +(*(x,y),+(x,z)) -> *(x,+(y,z)) weak: +(*(x,y),+(*(x,z),u)) -> +(*(x,+(y,z)),u) Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [*](x0, x1) = x0 + x1, [+](x0, x1) = x0 + x1 + 1 orientation: +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) +(*(x,y),+(x,z)) = 2x + y + z + 2 >= x + y + z + 1 = *(x,+(y,z)) +(*(x,y),+(*(x,z),u)) = u + 2x + y + z + 2 >= u + x + y + z + 2 = +(*(x,+(y,z)),u) problem: strict: +(x,+(y,z)) -> +(+(x,y),z) weak: +(*(x,y),+(x,z)) -> *(x,+(y,z)) +(*(x,y),+(*(x,z),u)) -> +(*(x,+(y,z)),u) Matrix Interpretation Processor: dimension: 2 max_matrix: [1 1] [0 1] interpretation: [1 0] [1 1] [*](x0, x1) = [0 0]x0 + [0 1]x1, [1 1] [0] [+](x0, x1) = x0 + [0 1]x1 + [1] orientation: [1 1] [1 2] [1] [1 1] [1 1] [0] +(x,+(y,z)) = x + [0 1]y + [0 1]z + [2] >= x + [0 1]y + [0 1]z + [2] = +(+(x,y),z) [2 1] [1 1] [1 2] [1] [1 0] [1 1] [1 2] [1] +(*(x,y),+(x,z)) = [0 1]x + [0 1]y + [0 1]z + [2] >= [0 0]x + [0 1]y + [0 1]z + [1] = *(x,+(y,z)) [1 2] [2 0] [1 1] [1 2] [1] [1 1] [1 0] [1 1] [1 2] [1] +(*(x,y),+(*(x,z),u)) = [0 1]u + [0 0]x + [0 1]y + [0 1]z + [2] >= [0 1]u + [0 0]x + [0 1]y + [0 1]z + [2] = +(*(x,+(y,z)),u) problem: strict: weak: +(x,+(y,z)) -> +(+(x,y),z) +(*(x,y),+(x,z)) -> *(x,+(y,z)) +(*(x,y),+(*(x,z),u)) -> +(*(x,+(y,z)),u) Qed