YES(?,O(n^2)) 19.85/9.28 YES(?,O(n^2)) 19.85/9.28 19.85/9.28 Problem: 19.85/9.28 minus(minus(x)) -> x 19.85/9.28 minus(h(x)) -> h(minus(x)) 19.85/9.28 minus(f(x,y)) -> f(minus(y),minus(x)) 19.85/9.28 19.85/9.28 Proof: 19.85/9.28 Complexity Transformation Processor: 19.85/9.28 strict: 19.85/9.28 minus(minus(x)) -> x 19.85/9.28 minus(h(x)) -> h(minus(x)) 19.85/9.28 minus(f(x,y)) -> f(minus(y),minus(x)) 19.85/9.28 weak: 19.85/9.28 19.85/9.28 Matrix Interpretation Processor: dim=1 19.85/9.28 19.85/9.28 max_matrix: 19.85/9.28 1 19.85/9.28 interpretation: 19.85/9.28 [f](x0, x1) = x0 + x1 + 196, 19.85/9.28 19.85/9.28 [h](x0) = x0, 19.85/9.28 19.85/9.28 [minus](x0) = x0 + 6 19.85/9.28 orientation: 19.85/9.28 minus(minus(x)) = x + 12 >= x = x 19.85/9.28 19.85/9.28 minus(h(x)) = x + 6 >= x + 6 = h(minus(x)) 19.85/9.28 19.85/9.28 minus(f(x,y)) = x + y + 202 >= x + y + 208 = f(minus(y),minus(x)) 19.85/9.28 problem: 19.85/9.28 strict: 19.85/9.28 minus(h(x)) -> h(minus(x)) 19.85/9.28 minus(f(x,y)) -> f(minus(y),minus(x)) 19.85/9.28 weak: 19.85/9.28 minus(minus(x)) -> x 19.85/9.28 Splitting Processor: 19.85/9.28 strict: 19.85/9.28 minus(h(x)) -> h(minus(x)) 19.85/9.28 weak: 19.85/9.28 minus(minus(x)) -> x 19.85/9.28 minus(f(x,y)) -> f(minus(y),minus(x)) 19.85/9.28 Matrix Interpretation Processor: dim=2 19.85/9.28 19.85/9.28 max_matrix: 19.85/9.28 [1 1] 19.85/9.28 [0 1] 19.85/9.28 interpretation: 19.85/9.28 [2] 19.85/9.28 [f](x0, x1) = x0 + x1 + [3], 19.85/9.28 19.85/9.28 [0] 19.85/9.28 [h](x0) = x0 + [3], 19.85/9.28 19.85/9.28 [1 1] [2] 19.85/9.28 [minus](x0) = [0 1]x0 + [0] 19.85/9.28 orientation: 19.85/9.28 [1 1] [1 1] [7] [1 1] [1 1] [6] 19.85/9.28 minus(f(x,y)) = [0 1]x + [0 1]y + [3] >= [0 1]x + [0 1]y + [3] = f(minus(y),minus(x)) 19.85/9.28 19.85/9.28 [1 1] [5] [1 1] [2] 19.85/9.28 minus(h(x)) = [0 1]x + [3] >= [0 1]x + [3] = h(minus(x)) 19.85/9.28 19.85/9.28 [1 2] [4] 19.85/9.28 minus(minus(x)) = [0 1]x + [0] >= x = x 19.85/9.28 problem: 19.85/9.28 strict: 19.85/9.28 19.85/9.28 weak: 19.85/9.28 minus(f(x,y)) -> f(minus(y),minus(x)) 19.85/9.28 minus(h(x)) -> h(minus(x)) 19.85/9.28 minus(minus(x)) -> x 19.85/9.28 Qed 19.85/9.28 19.85/9.28 strict: 19.85/9.28 minus(f(x,y)) -> f(minus(y),minus(x)) 19.85/9.28 weak: 19.85/9.28 minus(h(x)) -> h(minus(x)) 19.85/9.28 minus(minus(x)) -> x 19.85/9.28 Matrix Interpretation Processor: dim=2 19.85/9.28 19.85/9.28 max_matrix: 19.85/9.28 [1 2] 19.85/9.28 [0 1] 19.85/9.28 interpretation: 19.85/9.28 [2] 19.85/9.28 [f](x0, x1) = x0 + x1 + [1], 19.85/9.28 19.85/9.28 [1 2] [0] 19.85/9.28 [h](x0) = [0 1]x0 + [1], 19.85/9.28 19.85/9.28 [1 1] 19.85/9.28 [minus](x0) = [0 1]x0 19.85/9.28 orientation: 19.85/9.28 [1 3] [1] [1 3] [0] 19.85/9.28 minus(h(x)) = [0 1]x + [1] >= [0 1]x + [1] = h(minus(x)) 19.85/9.28 19.85/9.28 [1 2] 19.85/9.28 minus(minus(x)) = [0 1]x >= x = x 19.85/9.28 19.85/9.28 [1 1] [1 1] [3] [1 1] [1 1] [2] 19.85/9.28 minus(f(x,y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = f(minus(y),minus(x)) 19.85/9.28 problem: 19.85/9.28 strict: 19.85/9.28 19.85/9.28 weak: 19.85/9.28 minus(h(x)) -> h(minus(x)) 19.85/9.28 minus(minus(x)) -> x 19.85/9.28 minus(f(x,y)) -> f(minus(y),minus(x)) 19.85/9.28 Qed 19.85/9.29 EOF