YES(?,O(n^2)) 38.02/12.55 YES(?,O(n^2)) 38.02/12.57 38.02/12.57 Problem: 38.02/12.57 f(f(a(),f(x,a())),a()) -> f(a(),f(f(x,a()),a())) 38.02/12.57 38.02/12.57 Proof: 38.02/12.57 Uncurry Processor (mirror): 38.02/12.57 a2(a2(x,a()),x5) -> f(a2(a1(x),a()),x5) 38.02/12.57 a1(a2(x,a())) -> a2(a1(x),a()) 38.02/12.57 f(a1(x3),x4) -> a2(x3,x4) 38.02/12.57 f(a(),x4) -> a1(x4) 38.02/12.57 Complexity Transformation Processor: 38.02/12.57 strict: 38.02/12.57 a2(a2(x,a()),x5) -> f(a2(a1(x),a()),x5) 38.02/12.57 a1(a2(x,a())) -> a2(a1(x),a()) 38.02/12.57 f(a1(x3),x4) -> a2(x3,x4) 38.02/12.57 f(a(),x4) -> a1(x4) 38.02/12.57 weak: 38.02/12.57 38.02/12.57 Matrix Interpretation Processor: dim=1 38.02/12.57 38.02/12.57 max_matrix: 38.02/12.57 1 38.02/12.57 interpretation: 38.02/12.57 [a2](x0, x1) = x0 + x1 + 103, 38.02/12.57 38.02/12.57 [a1](x0) = x0, 38.02/12.57 38.02/12.57 [f](x0, x1) = x0 + x1 + 215, 38.02/12.57 38.02/12.57 [a] = 178 38.02/12.57 orientation: 38.02/12.57 a2(a2(x,a()),x5) = x + x5 + 384 >= x + x5 + 496 = f(a2(a1(x),a()),x5) 38.02/12.57 38.02/12.57 a1(a2(x,a())) = x + 281 >= x + 281 = a2(a1(x),a()) 38.02/12.57 38.02/12.57 f(a1(x3),x4) = x3 + x4 + 215 >= x3 + x4 + 103 = a2(x3,x4) 38.02/12.57 38.02/12.57 f(a(),x4) = x4 + 393 >= x4 = a1(x4) 38.02/12.57 problem: 38.02/12.57 strict: 38.02/12.57 a2(a2(x,a()),x5) -> f(a2(a1(x),a()),x5) 38.02/12.57 a1(a2(x,a())) -> a2(a1(x),a()) 38.02/12.57 weak: 38.02/12.57 f(a1(x3),x4) -> a2(x3,x4) 38.02/12.57 f(a(),x4) -> a1(x4) 38.02/12.57 Splitting Processor: 38.02/12.57 strict: 38.02/12.57 a1(a2(x,a())) -> a2(a1(x),a()) 38.02/12.57 weak: 38.02/12.57 f(a1(x3),x4) -> a2(x3,x4) 38.02/12.57 f(a(),x4) -> a1(x4) 38.02/12.57 a2(a2(x,a()),x5) -> f(a2(a1(x),a()),x5) 38.02/12.57 Matrix Interpretation Processor: dim=5 38.02/12.57 38.02/12.57 max_matrix: 38.02/12.57 [1 1 1 1 0] 38.02/12.57 [0 1 0 1 0] 38.02/12.57 [0 0 0 0 0] 38.02/12.57 [0 0 0 0 1] 38.02/12.57 [0 0 0 0 0] 38.02/12.57 interpretation: 38.02/12.57 [1 1 0 0 0] [1 1 0 0 0] [1] 38.02/12.57 [0 1 0 0 0] [0 1 0 1 0] [0] 38.02/12.57 [a2](x0, x1) = [0 0 0 0 0]x0 + [0 0 0 0 0]x1 + [1] 38.02/12.57 [0 0 0 0 0] [0 0 0 0 0] [0] 38.02/12.57 [0 0 0 0 0] [0 0 0 0 0] [0], 38.02/12.57 38.02/12.57 [1 1 0 0 0] [1] 38.02/12.57 [0 1 0 0 0] [0] 38.02/12.57 [a1](x0) = [0 0 0 0 0]x0 + [1] 38.02/12.57 [0 0 0 0 0] [1] 38.02/12.57 [0 0 0 0 0] [0], 38.02/12.57 38.02/12.57 [1 0 1 1 0] [1 1 0 0 0] [0] 38.02/12.57 [0 1 0 0 0] [0 1 0 1 0] [0] 38.02/12.57 [f](x0, x1) = [0 0 0 0 0]x0 + [0 0 0 0 0]x1 + [1] 38.02/12.57 [0 0 0 0 1] [0 0 0 0 0] [0] 38.02/12.57 [0 0 0 0 0] [0 0 0 0 0] [0], 38.02/12.57 38.02/12.57 [0] 38.02/12.57 [0] 38.02/12.57 [a] = [1] 38.02/12.57 [1] 38.02/12.57 [1] 38.02/12.57 orientation: 38.02/12.57 [1 2 0 0 0] [3] [1 2 0 0 0] [2] 38.02/12.57 [0 1 0 0 0] [1] [0 1 0 0 0] [1] 38.02/12.57 a1(a2(x,a())) = [0 0 0 0 0]x + [1] >= [0 0 0 0 0]x + [1] = a2(a1(x),a()) 38.02/12.57 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 38.02/12.57 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 38.02/12.57 38.02/12.57 [1 1 0 0 0] [1 1 0 0 0] [3] [1 1 0 0 0] [1 1 0 0 0] [1] 38.02/12.57 [0 1 0 0 0] [0 1 0 1 0] [0] [0 1 0 0 0] [0 1 0 1 0] [0] 38.02/12.57 f(a1(x3),x4) = [0 0 0 0 0]x3 + [0 0 0 0 0]x4 + [1] >= [0 0 0 0 0]x3 + [0 0 0 0 0]x4 + [1] = a2(x3,x4) 38.02/12.57 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] 38.02/12.57 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] 38.02/12.57 38.02/12.57 [1 1 0 0 0] [2] [1 1 0 0 0] [1] 38.02/12.57 [0 1 0 1 0] [0] [0 1 0 0 0] [0] 38.02/12.57 f(a(),x4) = [0 0 0 0 0]x4 + [1] >= [0 0 0 0 0]x4 + [1] = a1(x4) 38.02/12.57 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 38.02/12.57 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 38.02/12.57 38.02/12.57 [1 2 0 0 0] [1 1 0 0 0] [3] [1 2 0 0 0] [1 1 0 0 0] [3] 38.02/12.57 [0 1 0 0 0] [0 1 0 1 0] [1] [0 1 0 0 0] [0 1 0 1 0] [1] 38.02/12.57 a2(a2(x,a()),x5) = [0 0 0 0 0]x + [0 0 0 0 0]x5 + [1] >= [0 0 0 0 0]x + [0 0 0 0 0]x5 + [1] = f(a2(a1(x),a()),x5) 38.02/12.57 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] 38.02/12.57 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] 38.02/12.57 problem: 38.02/12.57 strict: 38.02/12.57 38.02/12.57 weak: 38.02/12.57 a1(a2(x,a())) -> a2(a1(x),a()) 38.02/12.57 f(a1(x3),x4) -> a2(x3,x4) 38.02/12.57 f(a(),x4) -> a1(x4) 38.02/12.57 a2(a2(x,a()),x5) -> f(a2(a1(x),a()),x5) 38.02/12.57 Qed 38.02/12.57 38.02/12.57 strict: 38.02/12.57 a2(a2(x,a()),x5) -> f(a2(a1(x),a()),x5) 38.02/12.57 weak: 38.02/12.57 a1(a2(x,a())) -> a2(a1(x),a()) 38.02/12.57 f(a1(x3),x4) -> a2(x3,x4) 38.02/12.57 f(a(),x4) -> a1(x4) 38.02/12.57 Matrix Interpretation Processor: dim=5 38.02/12.57 38.02/12.57 max_matrix: 38.02/12.57 [1 1 1 1 1] 38.02/12.57 [0 0 0 1 0] 38.02/12.57 [0 0 0 1 1] 38.02/12.57 [0 0 0 0 1] 38.02/12.57 [0 0 0 0 0] 38.02/12.57 interpretation: 38.02/12.57 [1 0 1 1 0] [1 1 1 0 1] [0] 38.02/12.57 [0 0 0 0 0] [0 0 0 1 0] [0] 38.02/12.57 [a2](x0, x1) = [0 0 0 0 1]x0 + [0 0 0 1 0]x1 + [0] 38.02/12.57 [0 0 0 0 0] [0 0 0 0 1] [1] 38.02/12.57 [0 0 0 0 0] [0 0 0 0 0] [1], 38.02/12.57 38.02/12.57 [1 0 1 0 0] [0] 38.02/12.57 [0 0 0 1 0] [0] 38.02/12.57 [a1](x0) = [0 0 0 1 0]x0 + [0] 38.02/12.57 [0 0 0 0 1] [0] 38.02/12.57 [0 0 0 0 0] [1], 38.02/12.57 38.02/12.57 [1 1 0 0 0] [1 1 1 0 1] [0] 38.02/12.57 [0 0 0 0 0] [0 0 0 1 0] [0] 38.02/12.57 [f](x0, x1) = [0 0 0 1 0]x0 + [0 0 0 1 0]x1 + [0] 38.02/12.57 [0 0 0 0 1] [0 0 0 0 1] [0] 38.02/12.57 [0 0 0 0 0] [0 0 0 0 0] [1], 38.02/12.57 38.02/12.57 [0] 38.02/12.57 [0] 38.02/12.57 [a] = [0] 38.02/12.57 [0] 38.02/12.57 [0] 38.02/12.57 orientation: 38.02/12.57 [1 0 1 1 1] [1 1 1 0 1] [1] [1 0 1 1 1] [1 1 1 0 1] [0] 38.02/12.57 [0 0 0 0 0] [0 0 0 1 0] [0] [0 0 0 0 0] [0 0 0 1 0] [0] 38.02/12.57 a2(a2(x,a()),x5) = [0 0 0 0 0]x + [0 0 0 1 0]x5 + [1] >= [0 0 0 0 0]x + [0 0 0 1 0]x5 + [1] = f(a2(a1(x),a()),x5) 38.02/12.57 [0 0 0 0 0] [0 0 0 0 1] [1] [0 0 0 0 0] [0 0 0 0 1] [1] 38.02/12.57 [0 0 0 0 0] [0 0 0 0 0] [1] [0 0 0 0 0] [0 0 0 0 0] [1] 38.02/12.57 38.02/12.57 [1 0 1 1 1] [0] [1 0 1 1 1] [0] 38.02/12.57 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 38.02/12.57 a1(a2(x,a())) = [0 0 0 0 0]x + [1] >= [0 0 0 0 0]x + [1] = a2(a1(x),a()) 38.02/12.57 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 38.02/12.57 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 38.02/12.57 38.02/12.57 [1 0 1 1 0] [1 1 1 0 1] [0] [1 0 1 1 0] [1 1 1 0 1] [0] 38.02/12.57 [0 0 0 0 0] [0 0 0 1 0] [0] [0 0 0 0 0] [0 0 0 1 0] [0] 38.02/12.57 f(a1(x3),x4) = [0 0 0 0 1]x3 + [0 0 0 1 0]x4 + [0] >= [0 0 0 0 1]x3 + [0 0 0 1 0]x4 + [0] = a2(x3,x4) 38.02/12.57 [0 0 0 0 0] [0 0 0 0 1] [1] [0 0 0 0 0] [0 0 0 0 1] [1] 38.02/12.57 [0 0 0 0 0] [0 0 0 0 0] [1] [0 0 0 0 0] [0 0 0 0 0] [1] 38.02/12.57 38.02/12.57 [1 1 1 0 1] [0] [1 0 1 0 0] [0] 38.02/12.57 [0 0 0 1 0] [0] [0 0 0 1 0] [0] 38.02/12.57 f(a(),x4) = [0 0 0 1 0]x4 + [0] >= [0 0 0 1 0]x4 + [0] = a1(x4) 38.02/12.57 [0 0 0 0 1] [0] [0 0 0 0 1] [0] 38.02/12.57 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 38.02/12.57 problem: 38.02/12.57 strict: 38.02/12.57 38.02/12.57 weak: 38.02/12.57 a2(a2(x,a()),x5) -> f(a2(a1(x),a()),x5) 38.02/12.57 a1(a2(x,a())) -> a2(a1(x),a()) 38.02/12.57 f(a1(x3),x4) -> a2(x3,x4) 38.02/12.57 f(a(),x4) -> a1(x4) 38.02/12.57 Qed 38.02/12.58 EOF