YES(?,O(n^2)) 12.98/7.13 YES(?,O(n^2)) 12.98/7.14 12.98/7.14 Problem: 12.98/7.14 +(x,+(y,z)) -> +(+(x,y),z) 12.98/7.14 +(*(x,y),+(x,z)) -> *(x,+(y,z)) 12.98/7.14 +(*(x,y),+(*(x,z),u)) -> +(*(x,+(y,z)),u) 12.98/7.14 12.98/7.14 Proof: 12.98/7.14 Complexity Transformation Processor: 12.98/7.14 strict: 12.98/7.14 +(x,+(y,z)) -> +(+(x,y),z) 12.98/7.14 +(*(x,y),+(x,z)) -> *(x,+(y,z)) 12.98/7.14 +(*(x,y),+(*(x,z),u)) -> +(*(x,+(y,z)),u) 12.98/7.14 weak: 12.98/7.14 12.98/7.14 Matrix Interpretation Processor: dim=1 12.98/7.14 12.98/7.14 max_matrix: 12.98/7.14 1 12.98/7.14 interpretation: 12.98/7.14 [*](x0, x1) = x0 + x1 + 96, 12.98/7.14 12.98/7.14 [+](x0, x1) = x0 + x1 12.98/7.14 orientation: 12.98/7.14 +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z) 12.98/7.14 12.98/7.14 +(*(x,y),+(x,z)) = 2x + y + z + 96 >= x + y + z + 96 = *(x,+(y,z)) 12.98/7.14 12.98/7.14 +(*(x,y),+(*(x,z),u)) = u + 2x + y + z + 192 >= u + x + y + z + 96 = +(*(x,+(y,z)),u) 12.98/7.14 problem: 12.98/7.14 strict: 12.98/7.14 +(x,+(y,z)) -> +(+(x,y),z) 12.98/7.14 +(*(x,y),+(x,z)) -> *(x,+(y,z)) 12.98/7.14 weak: 12.98/7.14 +(*(x,y),+(*(x,z),u)) -> +(*(x,+(y,z)),u) 12.98/7.14 Matrix Interpretation Processor: dim=1 12.98/7.14 12.98/7.14 max_matrix: 12.98/7.14 1 12.98/7.14 interpretation: 12.98/7.14 [*](x0, x1) = x0 + x1, 12.98/7.14 12.98/7.14 [+](x0, x1) = x0 + x1 + 16 12.98/7.14 orientation: 12.98/7.14 +(x,+(y,z)) = x + y + z + 32 >= x + y + z + 32 = +(+(x,y),z) 12.98/7.14 12.98/7.14 +(*(x,y),+(x,z)) = 2x + y + z + 32 >= x + y + z + 16 = *(x,+(y,z)) 12.98/7.14 12.98/7.14 +(*(x,y),+(*(x,z),u)) = u + 2x + y + z + 32 >= u + x + y + z + 32 = +(*(x,+(y,z)),u) 12.98/7.14 problem: 12.98/7.14 strict: 12.98/7.14 +(x,+(y,z)) -> +(+(x,y),z) 12.98/7.14 weak: 12.98/7.14 +(*(x,y),+(x,z)) -> *(x,+(y,z)) 12.98/7.14 +(*(x,y),+(*(x,z),u)) -> +(*(x,+(y,z)),u) 12.98/7.14 Matrix Interpretation Processor: dim=4 12.98/7.14 12.98/7.14 max_matrix: 12.98/7.14 [1 1 1 1] 12.98/7.14 [0 0 0 0] 12.98/7.14 [0 0 1 0] 12.98/7.14 [0 0 0 0] 12.98/7.14 interpretation: 12.98/7.14 [1 0 1 0] [1 1 0 1] 12.98/7.14 [0 0 0 0] [0 0 0 0] 12.98/7.14 [*](x0, x1) = [0 0 1 0]x0 + [0 0 1 0]x1 12.98/7.14 [0 0 0 0] [0 0 0 0] , 12.98/7.14 12.98/7.14 [1 1 0 1] [1 1 1 0] [0] 12.98/7.14 [0 0 0 0] [0 0 0 0] [1] 12.98/7.14 [+](x0, x1) = [0 0 1 0]x0 + [0 0 1 0]x1 + [1] 12.98/7.14 [0 0 0 0] [0 0 0 0] [0] 12.98/7.14 orientation: 12.98/7.14 [1 1 0 1] [1 1 1 1] [1 1 2 0] [2] [1 1 0 1] [1 1 1 0] [1 1 1 0] [1] 12.98/7.14 [0 0 0 0] [0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [0 0 0 0] [1] 12.98/7.14 +(x,+(y,z)) = [0 0 1 0]x + [0 0 1 0]y + [0 0 1 0]z + [2] >= [0 0 1 0]x + [0 0 1 0]y + [0 0 1 0]z + [2] = +(+(x,y),z) 12.98/7.14 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] 12.98/7.14 12.98/7.14 [2 1 2 1] [1 1 0 1] [1 1 2 0] [2] [1 0 1 0] [1 1 0 1] [1 1 1 0] [1] 12.98/7.14 [0 0 0 0] [0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] 12.98/7.14 +(*(x,y),+(x,z)) = [0 0 2 0]x + [0 0 1 0]y + [0 0 1 0]z + [2] >= [0 0 1 0]x + [0 0 1 0]y + [0 0 1 0]z + [1] = *(x,+(y,z)) 12.98/7.14 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] 12.98/7.14 12.98/7.14 [1 1 2 0] [2 0 3 0] [1 1 0 1] [1 1 1 1] [2] [1 1 1 0] [1 0 1 0] [1 1 0 1] [1 1 1 0] [1] 12.98/7.14 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [1] 12.98/7.14 +(*(x,y),+(*(x,z),u)) = [0 0 1 0]u + [0 0 2 0]x + [0 0 1 0]y + [0 0 1 0]z + [2] >= [0 0 1 0]u + [0 0 1 0]x + [0 0 1 0]y + [0 0 1 0]z + [2] = +(*(x,+(y,z)),u) 12.98/7.14 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] 12.98/7.14 problem: 12.98/7.14 strict: 12.98/7.14 12.98/7.14 weak: 12.98/7.14 +(x,+(y,z)) -> +(+(x,y),z) 12.98/7.14 +(*(x,y),+(x,z)) -> *(x,+(y,z)) 12.98/7.14 +(*(x,y),+(*(x,z),u)) -> +(*(x,+(y,z)),u) 12.98/7.14 Qed 12.98/7.15 EOF