YES(?,O(n^2)) 27.35/11.04 YES(?,O(n^2)) 27.35/11.05 27.35/11.05 Problem: 27.35/11.05 i(0()) -> 0() 27.35/11.05 +(0(),y) -> y 27.35/11.05 +(x,0()) -> x 27.35/11.05 i(i(x)) -> x 27.35/11.05 +(i(x),x) -> 0() 27.35/11.05 +(x,i(x)) -> 0() 27.35/11.05 i(+(x,y)) -> +(i(x),i(y)) 27.35/11.05 +(x,+(y,z)) -> +(+(x,y),z) 27.35/11.05 +(+(x,i(y)),y) -> x 27.35/11.05 +(+(x,y),i(y)) -> x 27.35/11.05 27.35/11.05 Proof: 27.35/11.05 Complexity Transformation Processor: 27.35/11.05 strict: 27.35/11.05 i(0()) -> 0() 27.35/11.05 +(0(),y) -> y 27.35/11.05 +(x,0()) -> x 27.35/11.05 i(i(x)) -> x 27.35/11.05 +(i(x),x) -> 0() 27.35/11.05 +(x,i(x)) -> 0() 27.35/11.05 i(+(x,y)) -> +(i(x),i(y)) 27.35/11.05 +(x,+(y,z)) -> +(+(x,y),z) 27.35/11.05 +(+(x,i(y)),y) -> x 27.35/11.05 +(+(x,y),i(y)) -> x 27.35/11.05 weak: 27.35/11.05 27.35/11.05 Matrix Interpretation Processor: dim=1 27.35/11.05 27.35/11.05 max_matrix: 27.35/11.05 1 27.35/11.05 interpretation: 27.35/11.05 [+](x0, x1) = x0 + x1 + 76, 27.35/11.05 27.35/11.05 [i](x0) = x0 + 36, 27.35/11.05 27.35/11.05 [0] = 119 27.35/11.05 orientation: 27.35/11.05 i(0()) = 155 >= 119 = 0() 27.35/11.05 27.35/11.05 +(0(),y) = y + 195 >= y = y 27.35/11.05 27.35/11.05 +(x,0()) = x + 195 >= x = x 27.35/11.05 27.35/11.05 i(i(x)) = x + 72 >= x = x 27.35/11.05 27.35/11.05 +(i(x),x) = 2x + 112 >= 119 = 0() 27.35/11.05 27.35/11.05 +(x,i(x)) = 2x + 112 >= 119 = 0() 27.35/11.05 27.35/11.05 i(+(x,y)) = x + y + 112 >= x + y + 148 = +(i(x),i(y)) 27.35/11.05 27.35/11.05 +(x,+(y,z)) = x + y + z + 152 >= x + y + z + 152 = +(+(x,y),z) 27.35/11.05 27.35/11.05 +(+(x,i(y)),y) = x + 2y + 188 >= x = x 27.35/11.05 27.35/11.05 +(+(x,y),i(y)) = x + 2y + 188 >= x = x 27.35/11.05 problem: 27.35/11.05 strict: 27.35/11.05 +(i(x),x) -> 0() 27.35/11.05 +(x,i(x)) -> 0() 27.35/11.05 i(+(x,y)) -> +(i(x),i(y)) 27.35/11.05 +(x,+(y,z)) -> +(+(x,y),z) 27.35/11.05 weak: 27.35/11.05 i(0()) -> 0() 27.35/11.05 +(0(),y) -> y 27.35/11.05 +(x,0()) -> x 27.35/11.05 i(i(x)) -> x 27.35/11.05 +(+(x,i(y)),y) -> x 27.35/11.05 +(+(x,y),i(y)) -> x 27.35/11.05 Matrix Interpretation Processor: dim=1 27.35/11.05 27.35/11.05 max_matrix: 27.35/11.05 1 27.35/11.05 interpretation: 27.35/11.05 [+](x0, x1) = x0 + x1, 27.35/11.05 27.35/11.05 [i](x0) = x0 + 1, 27.35/11.05 27.35/11.05 [0] = 0 27.35/11.05 orientation: 27.35/11.05 +(i(x),x) = 2x + 1 >= 0 = 0() 27.35/11.05 27.35/11.05 +(x,i(x)) = 2x + 1 >= 0 = 0() 27.35/11.05 27.35/11.05 i(+(x,y)) = x + y + 1 >= x + y + 2 = +(i(x),i(y)) 27.35/11.05 27.35/11.05 +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z) 27.35/11.05 27.35/11.05 i(0()) = 1 >= 0 = 0() 27.35/11.05 27.35/11.05 +(0(),y) = y >= y = y 27.35/11.05 27.35/11.05 +(x,0()) = x >= x = x 27.35/11.05 27.35/11.05 i(i(x)) = x + 2 >= x = x 27.35/11.05 27.35/11.05 +(+(x,i(y)),y) = x + 2y + 1 >= x = x 27.35/11.05 27.35/11.05 +(+(x,y),i(y)) = x + 2y + 1 >= x = x 27.35/11.05 problem: 27.35/11.05 strict: 27.35/11.05 i(+(x,y)) -> +(i(x),i(y)) 27.35/11.05 +(x,+(y,z)) -> +(+(x,y),z) 27.35/11.05 weak: 27.35/11.05 +(i(x),x) -> 0() 27.35/11.05 +(x,i(x)) -> 0() 27.35/11.05 i(0()) -> 0() 27.35/11.05 +(0(),y) -> y 27.35/11.05 +(x,0()) -> x 27.35/11.05 i(i(x)) -> x 27.35/11.05 +(+(x,i(y)),y) -> x 27.35/11.05 +(+(x,y),i(y)) -> x 27.35/11.05 Splitting Processor: 27.35/11.05 strict: 27.35/11.05 +(x,+(y,z)) -> +(+(x,y),z) 27.35/11.05 weak: 27.35/11.05 +(i(x),x) -> 0() 27.35/11.05 +(x,i(x)) -> 0() 27.35/11.05 i(0()) -> 0() 27.35/11.05 +(0(),y) -> y 27.35/11.05 +(x,0()) -> x 27.35/11.05 i(i(x)) -> x 27.35/11.05 +(+(x,i(y)),y) -> x 27.35/11.05 +(+(x,y),i(y)) -> x 27.35/11.05 i(+(x,y)) -> +(i(x),i(y)) 27.35/11.05 Matrix Interpretation Processor: dim=2 27.35/11.05 27.35/11.05 max_matrix: 27.35/11.05 [1 3] 27.35/11.05 [0 1] 27.35/11.05 interpretation: 27.35/11.05 [1 3] [0] 27.35/11.05 [+](x0, x1) = x0 + [0 1]x1 + [1], 27.35/11.05 27.35/11.05 [1 3] [2] 27.35/11.05 [i](x0) = [0 1]x0 + [0], 27.35/11.05 27.35/11.05 [2] 27.35/11.05 [0] = [1] 27.35/11.05 orientation: 27.35/11.05 [1 3] [1 6] [5] [1 3] [1 6] [4] 27.35/11.05 i(+(x,y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = +(i(x),i(y)) 27.35/11.05 27.35/11.05 [1 3] [1 6] [3] [1 3] [1 3] [0] 27.35/11.05 +(x,+(y,z)) = x + [0 1]y + [0 1]z + [2] >= x + [0 1]y + [0 1]z + [2] = +(+(x,y),z) 27.35/11.05 27.35/11.05 [2 6] [2] [2] 27.35/11.05 +(i(x),x) = [0 2]x + [1] >= [1] = 0() 27.35/11.05 27.35/11.05 [2 6] [2] [2] 27.35/11.05 +(x,i(x)) = [0 2]x + [1] >= [1] = 0() 27.35/11.05 27.35/11.05 [7] [2] 27.35/11.05 i(0()) = [1] >= [1] = 0() 27.35/11.05 27.35/11.05 [1 3] [2] 27.35/11.05 +(0(),y) = [0 1]y + [2] >= y = y 27.35/11.05 27.35/11.05 [5] 27.35/11.05 +(x,0()) = x + [2] >= x = x 27.35/11.05 27.35/11.05 [1 6] [4] 27.35/11.05 i(i(x)) = [0 1]x + [0] >= x = x 27.35/11.05 27.35/11.05 [2 9] [2] 27.35/11.05 +(+(x,i(y)),y) = x + [0 2]y + [2] >= x = x 27.35/11.05 27.35/11.05 [2 9] [2] 27.35/11.05 +(+(x,y),i(y)) = x + [0 2]y + [2] >= x = x 27.35/11.05 problem: 27.35/11.05 strict: 27.35/11.05 27.35/11.05 weak: 27.35/11.05 i(+(x,y)) -> +(i(x),i(y)) 27.35/11.05 +(x,+(y,z)) -> +(+(x,y),z) 27.35/11.05 +(i(x),x) -> 0() 27.35/11.05 +(x,i(x)) -> 0() 27.35/11.05 i(0()) -> 0() 27.35/11.05 +(0(),y) -> y 27.35/11.05 +(x,0()) -> x 27.35/11.05 i(i(x)) -> x 27.35/11.05 +(+(x,i(y)),y) -> x 27.35/11.05 +(+(x,y),i(y)) -> x 27.35/11.05 Qed 27.35/11.05 27.35/11.05 strict: 27.35/11.05 i(+(x,y)) -> +(i(x),i(y)) 27.35/11.05 weak: 27.35/11.05 +(x,+(y,z)) -> +(+(x,y),z) 27.35/11.05 +(i(x),x) -> 0() 27.35/11.05 +(x,i(x)) -> 0() 27.35/11.05 i(0()) -> 0() 27.35/11.05 +(0(),y) -> y 27.35/11.05 +(x,0()) -> x 27.35/11.05 i(i(x)) -> x 27.35/11.05 +(+(x,i(y)),y) -> x 27.35/11.05 +(+(x,y),i(y)) -> x 27.35/11.05 Matrix Interpretation Processor: dim=2 27.35/11.05 27.35/11.05 max_matrix: 27.35/11.05 [1 1] 27.35/11.05 [0 1] 27.35/11.05 interpretation: 27.35/11.05 [1 1] [0] 27.35/11.05 [+](x0, x1) = x0 + [0 1]x1 + [1], 27.35/11.05 27.35/11.05 [1 1] [1] 27.35/11.05 [i](x0) = [0 1]x0 + [0], 27.35/11.05 27.35/11.05 [1] 27.35/11.05 [0] = [0] 27.35/11.05 orientation: 27.35/11.05 [1 1] [1 2] [1] [1 1] [1 1] [0] 27.35/11.05 +(x,+(y,z)) = x + [0 1]y + [0 1]z + [2] >= x + [0 1]y + [0 1]z + [2] = +(+(x,y),z) 27.35/11.05 27.35/11.05 [2 2] [1] [1] 27.35/11.05 +(i(x),x) = [0 2]x + [1] >= [0] = 0() 27.35/11.05 27.35/11.05 [2 2] [1] [1] 27.35/11.05 +(x,i(x)) = [0 2]x + [1] >= [0] = 0() 27.35/11.05 27.35/11.05 [2] [1] 27.35/11.05 i(0()) = [0] >= [0] = 0() 27.35/11.05 27.35/11.05 [1 1] [1] 27.35/11.05 +(0(),y) = [0 1]y + [1] >= y = y 27.35/11.05 27.35/11.05 [1] 27.35/11.05 +(x,0()) = x + [1] >= x = x 27.35/11.05 27.35/11.05 [1 2] [2] 27.35/11.05 i(i(x)) = [0 1]x + [0] >= x = x 27.35/11.05 27.35/11.05 [2 3] [1] 27.35/11.05 +(+(x,i(y)),y) = x + [0 2]y + [2] >= x = x 27.35/11.05 27.35/11.05 [2 3] [1] 27.35/11.05 +(+(x,y),i(y)) = x + [0 2]y + [2] >= x = x 27.35/11.05 27.35/11.05 [1 1] [1 2] [2] [1 1] [1 2] [2] 27.35/11.05 i(+(x,y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = +(i(x),i(y)) 27.35/11.05 problem: 27.35/11.05 strict: 27.35/11.05 27.35/11.05 weak: 27.35/11.05 +(x,+(y,z)) -> +(+(x,y),z) 27.35/11.05 +(i(x),x) -> 0() 27.35/11.05 +(x,i(x)) -> 0() 27.35/11.05 i(0()) -> 0() 27.35/11.05 +(0(),y) -> y 27.35/11.05 +(x,0()) -> x 27.35/11.05 i(i(x)) -> x 27.35/11.05 +(+(x,i(y)),y) -> x 27.35/11.05 +(+(x,y),i(y)) -> x 27.35/11.05 i(+(x,y)) -> +(i(x),i(y)) 27.35/11.05 Qed 27.35/11.05 EOF