YES(?,O(n^2)) 37.92/12.45 YES(?,O(n^2)) 37.92/12.46 37.92/12.46 Problem: 37.92/12.46 f(a(),f(f(a(),x),a())) -> f(f(a(),f(a(),x)),a()) 37.92/12.46 37.92/12.46 Proof: 37.92/12.46 Uncurry Processor: 37.92/12.46 a2(a2(x,a()),x3) -> f(a2(a1(x),a()),x3) 37.92/12.46 a1(a2(x,a())) -> a2(a1(x),a()) 37.92/12.46 f(a1(x1),x2) -> a2(x1,x2) 37.92/12.46 f(a(),x2) -> a1(x2) 37.92/12.46 Complexity Transformation Processor: 37.92/12.46 strict: 37.92/12.46 a2(a2(x,a()),x3) -> f(a2(a1(x),a()),x3) 37.92/12.46 a1(a2(x,a())) -> a2(a1(x),a()) 37.92/12.46 f(a1(x1),x2) -> a2(x1,x2) 37.92/12.46 f(a(),x2) -> a1(x2) 37.92/12.46 weak: 37.92/12.46 37.92/12.46 Matrix Interpretation Processor: dim=1 37.92/12.46 37.92/12.46 max_matrix: 37.92/12.46 1 37.92/12.46 interpretation: 37.92/12.46 [a2](x0, x1) = x0 + x1 + 64, 37.92/12.46 37.92/12.46 [a1](x0) = x0 + 76, 37.92/12.46 37.92/12.46 [f](x0, x1) = x0 + x1 + 109, 37.92/12.46 37.92/12.46 [a] = 0 37.92/12.46 orientation: 37.92/12.46 a2(a2(x,a()),x3) = x + x3 + 128 >= x + x3 + 249 = f(a2(a1(x),a()),x3) 37.92/12.46 37.92/12.46 a1(a2(x,a())) = x + 140 >= x + 140 = a2(a1(x),a()) 37.92/12.46 37.92/12.46 f(a1(x1),x2) = x1 + x2 + 185 >= x1 + x2 + 64 = a2(x1,x2) 37.92/12.46 37.92/12.46 f(a(),x2) = x2 + 109 >= x2 + 76 = a1(x2) 37.92/12.46 problem: 37.92/12.46 strict: 37.92/12.46 a2(a2(x,a()),x3) -> f(a2(a1(x),a()),x3) 37.92/12.46 a1(a2(x,a())) -> a2(a1(x),a()) 37.92/12.46 weak: 37.92/12.46 f(a1(x1),x2) -> a2(x1,x2) 37.92/12.46 f(a(),x2) -> a1(x2) 37.92/12.46 Splitting Processor: 37.92/12.46 strict: 37.92/12.46 a1(a2(x,a())) -> a2(a1(x),a()) 37.92/12.46 weak: 37.92/12.46 f(a1(x1),x2) -> a2(x1,x2) 37.92/12.46 f(a(),x2) -> a1(x2) 37.92/12.46 a2(a2(x,a()),x3) -> f(a2(a1(x),a()),x3) 37.92/12.46 Matrix Interpretation Processor: dim=5 37.92/12.46 37.92/12.46 max_matrix: 37.92/12.46 [1 1 1 1 0] 37.92/12.46 [0 1 0 1 0] 37.92/12.46 [0 0 0 0 0] 37.92/12.46 [0 0 0 0 1] 37.92/12.46 [0 0 0 0 0] 37.92/12.46 interpretation: 37.92/12.46 [1 1 0 0 0] [1 1 0 0 0] [1] 37.92/12.46 [0 1 0 0 0] [0 1 0 1 0] [0] 37.92/12.46 [a2](x0, x1) = [0 0 0 0 0]x0 + [0 0 0 0 0]x1 + [1] 37.92/12.46 [0 0 0 0 0] [0 0 0 0 0] [0] 37.92/12.46 [0 0 0 0 0] [0 0 0 0 0] [0], 37.92/12.46 37.92/12.46 [1 1 0 0 0] [1] 37.92/12.46 [0 1 0 0 0] [0] 37.92/12.46 [a1](x0) = [0 0 0 0 0]x0 + [1] 37.92/12.46 [0 0 0 0 0] [1] 37.92/12.46 [0 0 0 0 0] [0], 37.92/12.46 37.92/12.46 [1 0 1 1 0] [1 1 0 0 0] [0] 37.92/12.46 [0 1 0 0 0] [0 1 0 1 0] [0] 37.92/12.46 [f](x0, x1) = [0 0 0 0 0]x0 + [0 0 0 0 0]x1 + [1] 37.92/12.46 [0 0 0 0 1] [0 0 0 0 0] [0] 37.92/12.46 [0 0 0 0 0] [0 0 0 0 0] [0], 37.92/12.46 37.92/12.46 [0] 37.92/12.46 [0] 37.92/12.46 [a] = [1] 37.92/12.46 [1] 37.92/12.46 [1] 37.92/12.46 orientation: 37.92/12.46 [1 2 0 0 0] [3] [1 2 0 0 0] [2] 37.92/12.46 [0 1 0 0 0] [1] [0 1 0 0 0] [1] 37.92/12.46 a1(a2(x,a())) = [0 0 0 0 0]x + [1] >= [0 0 0 0 0]x + [1] = a2(a1(x),a()) 37.92/12.46 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 37.92/12.46 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 37.92/12.46 37.92/12.46 [1 1 0 0 0] [1 1 0 0 0] [3] [1 1 0 0 0] [1 1 0 0 0] [1] 37.92/12.46 [0 1 0 0 0] [0 1 0 1 0] [0] [0 1 0 0 0] [0 1 0 1 0] [0] 37.92/12.46 f(a1(x1),x2) = [0 0 0 0 0]x1 + [0 0 0 0 0]x2 + [1] >= [0 0 0 0 0]x1 + [0 0 0 0 0]x2 + [1] = a2(x1,x2) 37.92/12.46 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] 37.92/12.46 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] 37.92/12.46 37.92/12.46 [1 1 0 0 0] [2] [1 1 0 0 0] [1] 37.92/12.46 [0 1 0 1 0] [0] [0 1 0 0 0] [0] 37.92/12.46 f(a(),x2) = [0 0 0 0 0]x2 + [1] >= [0 0 0 0 0]x2 + [1] = a1(x2) 37.92/12.46 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 37.92/12.46 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 37.92/12.46 37.92/12.46 [1 2 0 0 0] [1 1 0 0 0] [3] [1 2 0 0 0] [1 1 0 0 0] [3] 37.92/12.46 [0 1 0 0 0] [0 1 0 1 0] [1] [0 1 0 0 0] [0 1 0 1 0] [1] 37.92/12.46 a2(a2(x,a()),x3) = [0 0 0 0 0]x + [0 0 0 0 0]x3 + [1] >= [0 0 0 0 0]x + [0 0 0 0 0]x3 + [1] = f(a2(a1(x),a()),x3) 37.92/12.46 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] 37.92/12.47 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] 37.92/12.47 problem: 37.92/12.47 strict: 37.92/12.47 37.92/12.47 weak: 37.92/12.47 a1(a2(x,a())) -> a2(a1(x),a()) 37.92/12.47 f(a1(x1),x2) -> a2(x1,x2) 37.92/12.47 f(a(),x2) -> a1(x2) 37.92/12.47 a2(a2(x,a()),x3) -> f(a2(a1(x),a()),x3) 37.92/12.47 Qed 37.92/12.47 37.92/12.47 strict: 37.92/12.47 a2(a2(x,a()),x3) -> f(a2(a1(x),a()),x3) 37.92/12.47 weak: 37.92/12.47 a1(a2(x,a())) -> a2(a1(x),a()) 37.92/12.47 f(a1(x1),x2) -> a2(x1,x2) 37.92/12.47 f(a(),x2) -> a1(x2) 37.92/12.47 Matrix Interpretation Processor: dim=5 37.92/12.47 37.92/12.47 max_matrix: 37.92/12.47 [1 1 1 1 1] 37.92/12.47 [0 0 0 1 0] 37.92/12.47 [0 0 0 1 1] 37.92/12.47 [0 0 0 0 1] 37.92/12.47 [0 0 0 0 0] 37.92/12.47 interpretation: 37.92/12.47 [1 0 1 1 0] [1 1 1 0 1] [0] 37.92/12.47 [0 0 0 0 0] [0 0 0 1 0] [0] 37.92/12.47 [a2](x0, x1) = [0 0 0 0 1]x0 + [0 0 0 1 0]x1 + [0] 37.92/12.47 [0 0 0 0 0] [0 0 0 0 1] [1] 37.92/12.47 [0 0 0 0 0] [0 0 0 0 0] [1], 37.92/12.47 37.92/12.47 [1 0 1 0 0] [0] 37.92/12.47 [0 0 0 1 0] [0] 37.92/12.47 [a1](x0) = [0 0 0 1 0]x0 + [0] 37.92/12.47 [0 0 0 0 1] [0] 37.92/12.47 [0 0 0 0 0] [1], 37.92/12.47 37.92/12.47 [1 1 0 0 0] [1 1 1 0 1] [0] 37.92/12.47 [0 0 0 0 0] [0 0 0 1 0] [0] 37.92/12.47 [f](x0, x1) = [0 0 0 1 0]x0 + [0 0 0 1 0]x1 + [0] 37.92/12.47 [0 0 0 0 1] [0 0 0 0 1] [0] 37.92/12.47 [0 0 0 0 0] [0 0 0 0 0] [1], 37.92/12.47 37.92/12.47 [0] 37.92/12.47 [0] 37.92/12.47 [a] = [0] 37.92/12.47 [0] 37.92/12.47 [0] 37.92/12.47 orientation: 37.92/12.47 [1 0 1 1 1] [1 1 1 0 1] [1] [1 0 1 1 1] [1 1 1 0 1] [0] 37.92/12.47 [0 0 0 0 0] [0 0 0 1 0] [0] [0 0 0 0 0] [0 0 0 1 0] [0] 37.92/12.47 a2(a2(x,a()),x3) = [0 0 0 0 0]x + [0 0 0 1 0]x3 + [1] >= [0 0 0 0 0]x + [0 0 0 1 0]x3 + [1] = f(a2(a1(x),a()),x3) 37.92/12.47 [0 0 0 0 0] [0 0 0 0 1] [1] [0 0 0 0 0] [0 0 0 0 1] [1] 37.92/12.47 [0 0 0 0 0] [0 0 0 0 0] [1] [0 0 0 0 0] [0 0 0 0 0] [1] 37.92/12.47 37.92/12.47 [1 0 1 1 1] [0] [1 0 1 1 1] [0] 37.92/12.47 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 37.92/12.47 a1(a2(x,a())) = [0 0 0 0 0]x + [1] >= [0 0 0 0 0]x + [1] = a2(a1(x),a()) 37.92/12.47 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 37.92/12.47 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 37.92/12.47 37.92/12.47 [1 0 1 1 0] [1 1 1 0 1] [0] [1 0 1 1 0] [1 1 1 0 1] [0] 37.92/12.47 [0 0 0 0 0] [0 0 0 1 0] [0] [0 0 0 0 0] [0 0 0 1 0] [0] 37.92/12.47 f(a1(x1),x2) = [0 0 0 0 1]x1 + [0 0 0 1 0]x2 + [0] >= [0 0 0 0 1]x1 + [0 0 0 1 0]x2 + [0] = a2(x1,x2) 37.92/12.47 [0 0 0 0 0] [0 0 0 0 1] [1] [0 0 0 0 0] [0 0 0 0 1] [1] 37.92/12.47 [0 0 0 0 0] [0 0 0 0 0] [1] [0 0 0 0 0] [0 0 0 0 0] [1] 37.92/12.47 37.92/12.47 [1 1 1 0 1] [0] [1 0 1 0 0] [0] 37.92/12.47 [0 0 0 1 0] [0] [0 0 0 1 0] [0] 37.92/12.47 f(a(),x2) = [0 0 0 1 0]x2 + [0] >= [0 0 0 1 0]x2 + [0] = a1(x2) 37.92/12.47 [0 0 0 0 1] [0] [0 0 0 0 1] [0] 37.92/12.47 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 37.92/12.47 problem: 37.92/12.47 strict: 37.92/12.47 37.92/12.47 weak: 37.92/12.47 a2(a2(x,a()),x3) -> f(a2(a1(x),a()),x3) 37.92/12.47 a1(a2(x,a())) -> a2(a1(x),a()) 37.92/12.47 f(a1(x1),x2) -> a2(x1,x2) 37.92/12.47 f(a(),x2) -> a1(x2) 37.92/12.47 Qed 37.92/12.47 EOF