YES(?,O(n^2)) 28.36/9.22 YES(?,O(n^2)) 28.36/9.22 28.36/9.22 Problem: 28.36/9.22 a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) 28.36/9.22 f(a(x),a(y)) -> a(f(x,y)) 28.36/9.22 f(b(x),b(y)) -> b(f(x,y)) 28.36/9.22 28.36/9.22 Proof: 28.36/9.22 Complexity Transformation Processor: 28.36/9.22 strict: 28.36/9.22 a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) 28.36/9.22 f(a(x),a(y)) -> a(f(x,y)) 28.36/9.22 f(b(x),b(y)) -> b(f(x,y)) 28.36/9.22 weak: 28.36/9.22 28.36/9.22 Matrix Interpretation Processor: dim=1 28.36/9.22 28.36/9.22 max_matrix: 28.36/9.22 1 28.36/9.22 interpretation: 28.36/9.22 [b](x0) = x0 + 1, 28.36/9.22 28.36/9.22 [a](x0) = x0 + 73, 28.36/9.22 28.36/9.22 [f](x0, x1) = x0 + x1 + 27 28.36/9.22 orientation: 28.36/9.22 a(a(f(x,y))) = x + y + 173 >= x + y + 469 = f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) 28.36/9.22 28.36/9.22 f(a(x),a(y)) = x + y + 173 >= x + y + 100 = a(f(x,y)) 28.36/9.22 28.36/9.22 f(b(x),b(y)) = x + y + 29 >= x + y + 28 = b(f(x,y)) 28.36/9.22 problem: 28.36/9.22 strict: 28.36/9.22 a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) 28.36/9.22 weak: 28.36/9.22 f(a(x),a(y)) -> a(f(x,y)) 28.36/9.22 f(b(x),b(y)) -> b(f(x,y)) 28.36/9.22 Matrix Interpretation Processor: dim=3 28.36/9.22 28.36/9.22 max_matrix: 28.36/9.22 [1 1 0] 28.36/9.22 [0 1 0] 28.36/9.22 [0 0 0] 28.36/9.22 interpretation: 28.36/9.22 [1 0 0] 28.36/9.22 [b](x0) = [0 0 0]x0 28.36/9.22 [0 0 0] , 28.36/9.22 28.36/9.22 [1 1 0] [0] 28.36/9.22 [a](x0) = [0 1 0]x0 + [1] 28.36/9.22 [0 0 0] [0], 28.36/9.22 28.36/9.22 [1 0 0] [1 0 0] 28.36/9.22 [f](x0, x1) = [0 1 0]x0 + [0 1 0]x1 28.36/9.22 [0 0 0] [0 0 0] 28.36/9.22 orientation: 28.36/9.22 [1 2 0] [1 2 0] [1] [1 1 0] [1 1 0] [0] 28.36/9.22 a(a(f(x,y))) = [0 1 0]x + [0 1 0]y + [2] >= [0 0 0]x + [0 0 0]y + [2] = f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) 28.36/9.22 [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] 28.36/9.22 28.36/9.22 [1 1 0] [1 1 0] [0] [1 1 0] [1 1 0] [0] 28.36/9.22 f(a(x),a(y)) = [0 1 0]x + [0 1 0]y + [2] >= [0 1 0]x + [0 1 0]y + [1] = a(f(x,y)) 28.36/9.22 [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] 28.36/9.22 28.36/9.22 [1 0 0] [1 0 0] [1 0 0] [1 0 0] 28.36/9.22 f(b(x),b(y)) = [0 0 0]x + [0 0 0]y >= [0 0 0]x + [0 0 0]y = b(f(x,y)) 28.36/9.22 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 28.36/9.22 problem: 28.36/9.22 strict: 28.36/9.22 28.36/9.22 weak: 28.36/9.22 a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) 28.36/9.22 f(a(x),a(y)) -> a(f(x,y)) 28.36/9.22 f(b(x),b(y)) -> b(f(x,y)) 28.36/9.22 Qed 28.36/9.23 EOF