YES(?,O(n^4)) 98.50/34.66 YES(?,O(n^4)) 98.50/34.67 98.50/34.67 Problem: 98.50/34.67 f(a(),x) -> f(b(),f(c(),x)) 98.50/34.67 f(a(),f(b(),x)) -> f(b(),f(a(),x)) 98.50/34.67 f(d(),f(c(),x)) -> f(d(),f(a(),x)) 98.50/34.67 f(a(),f(c(),x)) -> f(c(),f(a(),x)) 98.50/34.67 98.50/34.67 Proof: 98.50/34.67 Uncurry Processor: 98.50/34.67 a1(x) -> b1(c1(x)) 98.50/34.67 a1(b1(x)) -> b1(a1(x)) 98.50/34.67 d1(c1(x)) -> d1(a1(x)) 98.50/34.67 a1(c1(x)) -> c1(a1(x)) 98.50/34.67 f(a(),x1) -> a1(x1) 98.50/34.67 f(b(),x1) -> b1(x1) 98.50/34.67 f(c(),x1) -> c1(x1) 98.50/34.67 f(d(),x1) -> d1(x1) 98.50/34.67 Complexity Transformation Processor: 98.50/34.67 strict: 98.50/34.67 a1(x) -> b1(c1(x)) 98.50/34.67 a1(b1(x)) -> b1(a1(x)) 98.50/34.67 d1(c1(x)) -> d1(a1(x)) 98.50/34.67 a1(c1(x)) -> c1(a1(x)) 98.50/34.67 f(a(),x1) -> a1(x1) 98.50/34.67 f(b(),x1) -> b1(x1) 98.50/34.67 f(c(),x1) -> c1(x1) 98.50/34.67 f(d(),x1) -> d1(x1) 98.50/34.67 weak: 98.50/34.67 98.50/34.67 Matrix Interpretation Processor: dim=1 98.50/34.67 98.50/34.67 max_matrix: 98.50/34.67 1 98.50/34.67 interpretation: 98.50/34.67 [d1](x0) = x0 + 8, 98.50/34.67 98.50/34.67 [c1](x0) = x0 + 168, 98.50/34.67 98.50/34.67 [b1](x0) = x0 + 128, 98.50/34.67 98.50/34.67 [a1](x0) = x0 + 20, 98.50/34.67 98.50/34.67 [d] = 48, 98.50/34.67 98.50/34.67 [c] = 194, 98.50/34.67 98.50/34.67 [b] = 162, 98.50/34.67 98.50/34.67 [f](x0, x1) = x0 + x1 + 31, 98.50/34.67 98.50/34.67 [a] = 0 98.50/34.67 orientation: 98.50/34.67 a1(x) = x + 20 >= x + 296 = b1(c1(x)) 98.50/34.67 98.50/34.67 a1(b1(x)) = x + 148 >= x + 148 = b1(a1(x)) 98.50/34.67 98.50/34.67 d1(c1(x)) = x + 176 >= x + 28 = d1(a1(x)) 98.50/34.67 98.50/34.67 a1(c1(x)) = x + 188 >= x + 188 = c1(a1(x)) 98.50/34.67 98.50/34.67 f(a(),x1) = x1 + 31 >= x1 + 20 = a1(x1) 98.50/34.67 98.50/34.67 f(b(),x1) = x1 + 193 >= x1 + 128 = b1(x1) 98.50/34.67 98.50/34.67 f(c(),x1) = x1 + 225 >= x1 + 168 = c1(x1) 98.50/34.67 98.50/34.67 f(d(),x1) = x1 + 79 >= x1 + 8 = d1(x1) 98.50/34.67 problem: 98.50/34.67 strict: 98.50/34.67 a1(x) -> b1(c1(x)) 98.50/34.67 a1(b1(x)) -> b1(a1(x)) 98.50/34.67 a1(c1(x)) -> c1(a1(x)) 98.50/34.67 weak: 98.50/34.67 d1(c1(x)) -> d1(a1(x)) 98.50/34.67 f(a(),x1) -> a1(x1) 98.50/34.67 f(b(),x1) -> b1(x1) 98.50/34.67 f(c(),x1) -> c1(x1) 98.50/34.67 f(d(),x1) -> d1(x1) 98.50/34.67 Splitting Processor: 98.50/34.67 strict: 98.50/34.67 a1(x) -> b1(c1(x)) 98.50/34.67 weak: 98.50/34.67 d1(c1(x)) -> d1(a1(x)) 98.50/34.67 f(a(),x1) -> a1(x1) 98.50/34.67 f(b(),x1) -> b1(x1) 98.50/34.67 f(c(),x1) -> c1(x1) 98.50/34.67 f(d(),x1) -> d1(x1) 98.50/34.67 a1(b1(x)) -> b1(a1(x)) 98.50/34.67 a1(c1(x)) -> c1(a1(x)) 98.50/34.67 Matrix Interpretation Processor: dim=4 98.50/34.67 98.50/34.67 max_matrix: 98.50/34.67 [1 1 0 0] 98.50/34.67 [0 1 1 0] 98.50/34.67 [0 0 1 1] 98.50/34.67 [0 0 0 0] 98.50/34.67 interpretation: 98.50/34.67 [1 1 0 0] 98.50/34.67 [0 0 0 0] 98.50/34.67 [d1](x0) = [0 0 0 0]x0 98.50/34.67 [0 0 0 0] , 98.50/34.67 98.50/34.67 [1 0 0 0] [0] 98.50/34.67 [0 1 0 0] [1] 98.50/34.67 [c1](x0) = [0 0 1 0]x0 + [0] 98.50/34.67 [0 0 0 0] [0], 98.50/34.67 98.50/34.67 [1 0 0 0] 98.50/34.67 [0 0 0 0] 98.50/34.67 [b1](x0) = [0 0 1 0]x0 98.50/34.67 [0 0 0 0] , 98.50/34.67 98.50/34.67 [1 0 0 0] [1] 98.50/34.67 [0 1 0 0] [0] 98.50/34.67 [a1](x0) = [0 0 1 0]x0 + [1] 98.50/34.67 [0 0 0 0] [1], 98.50/34.67 98.50/34.67 [1] 98.50/34.67 [1] 98.50/34.67 [d] = [0] 98.50/34.67 [0], 98.50/34.67 98.50/34.67 [0] 98.50/34.67 [0] 98.50/34.67 [c] = [0] 98.50/34.67 [1], 98.50/34.67 98.50/34.67 [0] 98.50/34.67 [0] 98.50/34.67 [b] = [0] 98.50/34.67 [1], 98.50/34.67 98.50/34.67 [1 1 0 0] [1 1 0 0] [0] 98.50/34.67 [0 1 1 0] [0 1 0 0] [1] 98.50/34.67 [f](x0, x1) = [0 0 1 1]x0 + [0 0 1 0]x1 + [0] 98.50/34.67 [0 0 0 0] [0 0 0 0] [1], 98.50/34.67 98.50/34.67 [0] 98.50/34.67 [1] 98.50/34.67 [a] = [1] 98.50/34.67 [0] 98.50/34.67 orientation: 98.50/34.67 [1 0 0 0] [1] [1 0 0 0] 98.50/34.67 [0 1 0 0] [0] [0 0 0 0] 98.50/34.67 a1(x) = [0 0 1 0]x + [1] >= [0 0 1 0]x = b1(c1(x)) 98.50/34.67 [0 0 0 0] [1] [0 0 0 0] 98.50/34.67 98.50/34.67 [1 1 0 0] [1] [1 1 0 0] [1] 98.50/34.67 [0 0 0 0] [0] [0 0 0 0] [0] 98.50/34.67 d1(c1(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = d1(a1(x)) 98.50/34.67 [0 0 0 0] [0] [0 0 0 0] [0] 98.50/34.67 98.50/34.67 [1 1 0 0] [1] [1 0 0 0] [1] 98.50/34.67 [0 1 0 0] [3] [0 1 0 0] [0] 98.50/34.67 f(a(),x1) = [0 0 1 0]x1 + [1] >= [0 0 1 0]x1 + [1] = a1(x1) 98.50/34.67 [0 0 0 0] [1] [0 0 0 0] [1] 98.50/34.67 98.50/34.67 [1 1 0 0] [0] [1 0 0 0] 98.50/34.67 [0 1 0 0] [1] [0 0 0 0] 98.50/34.67 f(b(),x1) = [0 0 1 0]x1 + [1] >= [0 0 1 0]x1 = b1(x1) 98.50/34.67 [0 0 0 0] [1] [0 0 0 0] 98.50/34.67 98.50/34.67 [1 1 0 0] [0] [1 0 0 0] [0] 98.50/34.67 [0 1 0 0] [1] [0 1 0 0] [1] 98.50/34.67 f(c(),x1) = [0 0 1 0]x1 + [1] >= [0 0 1 0]x1 + [0] = c1(x1) 98.50/34.67 [0 0 0 0] [1] [0 0 0 0] [0] 98.50/34.67 98.50/34.67 [1 1 0 0] [2] [1 1 0 0] 98.50/34.67 [0 1 0 0] [2] [0 0 0 0] 98.50/34.67 f(d(),x1) = [0 0 1 0]x1 + [0] >= [0 0 0 0]x1 = d1(x1) 98.50/34.67 [0 0 0 0] [1] [0 0 0 0] 98.50/34.67 98.50/34.67 [1 0 0 0] [1] [1 0 0 0] [1] 98.50/34.67 [0 0 0 0] [0] [0 0 0 0] [0] 98.50/34.67 a1(b1(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = b1(a1(x)) 98.50/34.67 [0 0 0 0] [1] [0 0 0 0] [0] 98.50/34.67 98.50/34.67 [1 0 0 0] [1] [1 0 0 0] [1] 98.50/34.67 [0 1 0 0] [1] [0 1 0 0] [1] 98.50/34.67 a1(c1(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = c1(a1(x)) 98.50/34.67 [0 0 0 0] [1] [0 0 0 0] [0] 98.50/34.67 problem: 98.50/34.67 strict: 98.50/34.67 98.50/34.67 weak: 98.50/34.67 a1(x) -> b1(c1(x)) 98.50/34.67 d1(c1(x)) -> d1(a1(x)) 98.50/34.67 f(a(),x1) -> a1(x1) 98.50/34.67 f(b(),x1) -> b1(x1) 98.50/34.67 f(c(),x1) -> c1(x1) 98.50/34.67 f(d(),x1) -> d1(x1) 98.50/34.67 a1(b1(x)) -> b1(a1(x)) 98.50/34.67 a1(c1(x)) -> c1(a1(x)) 98.50/34.67 Qed 98.50/34.67 98.50/34.67 strict: 98.50/34.67 a1(b1(x)) -> b1(a1(x)) 98.50/34.67 a1(c1(x)) -> c1(a1(x)) 98.50/34.67 weak: 98.50/34.67 a1(x) -> b1(c1(x)) 98.50/34.67 d1(c1(x)) -> d1(a1(x)) 98.50/34.67 f(a(),x1) -> a1(x1) 98.50/34.67 f(b(),x1) -> b1(x1) 98.50/34.67 f(c(),x1) -> c1(x1) 98.50/34.67 f(d(),x1) -> d1(x1) 98.50/34.67 Matrix Interpretation Processor: dim=4 98.50/34.67 98.50/34.67 max_matrix: 98.50/34.67 [1 1 1 1] 98.50/34.67 [0 1 1 1] 98.50/34.67 [0 0 1 1] 98.50/34.67 [0 0 0 1] 98.50/34.67 interpretation: 98.50/34.67 [1 1 0 0] [1] 98.50/34.67 [0 1 1 0] [0] 98.50/34.67 [d1](x0) = [0 0 1 0]x0 + [0] 98.50/34.67 [0 0 0 0] [1], 98.50/34.67 98.50/34.67 [1 0 0 0] [0] 98.50/34.68 [0 1 1 1] [0] 98.50/34.68 [c1](x0) = [0 0 1 0]x0 + [1] 98.50/34.68 [0 0 0 1] [1], 98.50/34.68 98.50/34.68 [1 0 0 0] 98.50/34.68 [0 0 0 0] 98.50/34.68 [b1](x0) = [0 0 0 0]x0 98.50/34.68 [0 0 0 1] , 98.50/34.68 98.50/34.68 [1 0 0 1] [0] 98.50/34.68 [0 1 1 0] [0] 98.50/34.68 [a1](x0) = [0 0 1 0]x0 + [0] 98.50/34.68 [0 0 0 1] [1], 98.50/34.68 98.50/34.68 [0] 98.50/34.68 [0] 98.50/34.68 [d] = [1] 98.50/34.68 [1], 98.50/34.68 98.50/34.68 [0] 98.50/34.68 [0] 98.50/34.68 [c] = [1] 98.50/34.68 [1], 98.50/34.68 98.50/34.68 [0] 98.50/34.68 [1] 98.50/34.68 [b] = [0] 98.50/34.68 [0], 98.50/34.68 98.50/34.68 [1 1 1 0] [1 1 1 1] [1] 98.50/34.68 [0 1 0 1] [0 1 1 1] [0] 98.50/34.68 [f](x0, x1) = [0 0 1 1]x0 + [0 0 1 1]x1 + [0] 98.50/34.68 [0 0 0 1] [0 0 0 1] [1], 98.50/34.68 98.50/34.68 [1] 98.50/34.68 [0] 98.50/34.68 [a] = [0] 98.50/34.68 [1] 98.50/34.68 orientation: 98.50/34.68 [1 0 0 1] [0] [1 0 0 1] [0] 98.50/34.68 [0 0 0 0] [0] [0 0 0 0] [0] 98.50/34.68 a1(b1(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = b1(a1(x)) 98.50/34.68 [0 0 0 1] [1] [0 0 0 1] [1] 98.50/34.68 98.50/34.68 [1 0 0 1] [1] [1 0 0 1] [0] 98.50/34.68 [0 1 2 1] [1] [0 1 2 1] [1] 98.50/34.68 a1(c1(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = c1(a1(x)) 98.50/34.68 [0 0 0 1] [2] [0 0 0 1] [2] 98.50/34.68 98.50/34.68 [1 0 0 1] [0] [1 0 0 0] [0] 98.50/34.68 [0 1 1 0] [0] [0 0 0 0] [0] 98.50/34.68 a1(x) = [0 0 1 0]x + [0] >= [0 0 0 0]x + [0] = b1(c1(x)) 98.50/34.68 [0 0 0 1] [1] [0 0 0 1] [1] 98.50/34.68 98.50/34.68 [1 1 1 1] [1] [1 1 1 1] [1] 98.50/34.68 [0 1 2 1] [1] [0 1 2 0] [0] 98.50/34.68 d1(c1(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [0] = d1(a1(x)) 98.50/34.68 [0 0 0 0] [1] [0 0 0 0] [1] 98.50/34.68 98.50/34.68 [1 1 1 1] [2] [1 0 0 1] [0] 98.50/34.68 [0 1 1 1] [1] [0 1 1 0] [0] 98.50/34.68 f(a(),x1) = [0 0 1 1]x1 + [1] >= [0 0 1 0]x1 + [0] = a1(x1) 98.50/34.68 [0 0 0 1] [2] [0 0 0 1] [1] 98.50/34.68 98.50/34.68 [1 1 1 1] [2] [1 0 0 0] 98.50/34.68 [0 1 1 1] [1] [0 0 0 0] 98.50/34.68 f(b(),x1) = [0 0 1 1]x1 + [0] >= [0 0 0 0]x1 = b1(x1) 98.50/34.68 [0 0 0 1] [1] [0 0 0 1] 98.50/34.68 98.50/34.68 [1 1 1 1] [2] [1 0 0 0] [0] 98.50/34.68 [0 1 1 1] [1] [0 1 1 1] [0] 98.50/34.68 f(c(),x1) = [0 0 1 1]x1 + [2] >= [0 0 1 0]x1 + [1] = c1(x1) 98.50/34.68 [0 0 0 1] [2] [0 0 0 1] [1] 98.50/34.68 98.50/34.68 [1 1 1 1] [2] [1 1 0 0] [1] 98.50/34.68 [0 1 1 1] [1] [0 1 1 0] [0] 98.50/34.68 f(d(),x1) = [0 0 1 1]x1 + [2] >= [0 0 1 0]x1 + [0] = d1(x1) 98.50/34.68 [0 0 0 1] [2] [0 0 0 0] [1] 98.50/34.68 problem: 98.50/34.68 strict: 98.50/34.68 a1(b1(x)) -> b1(a1(x)) 98.50/34.68 weak: 98.50/34.68 a1(c1(x)) -> c1(a1(x)) 98.50/34.68 a1(x) -> b1(c1(x)) 98.50/34.68 d1(c1(x)) -> d1(a1(x)) 98.50/34.68 f(a(),x1) -> a1(x1) 98.50/34.68 f(b(),x1) -> b1(x1) 98.50/34.68 f(c(),x1) -> c1(x1) 98.50/34.68 f(d(),x1) -> d1(x1) 98.50/34.68 Matrix Interpretation Processor: dim=4 98.50/34.68 98.50/34.68 max_matrix: 98.50/34.68 [1 1 1 0] 98.50/34.68 [0 1 1 1] 98.50/34.68 [0 0 1 1] 98.50/34.68 [0 0 0 1] 98.50/34.68 interpretation: 98.50/34.68 [1 1 0 0] 98.50/34.68 [0 0 0 0] 98.50/34.68 [d1](x0) = [0 0 0 1]x0 98.50/34.68 [0 0 0 1] , 98.50/34.68 98.50/34.68 [1 0 0 0] [1] 98.50/34.68 [0 1 1 1] [0] 98.50/34.68 [c1](x0) = [0 0 1 0]x0 + [0] 98.50/34.68 [0 0 0 1] [1], 98.50/34.68 98.50/34.68 [1 0 0 0] [0] 98.50/34.68 [0 0 0 0] [0] 98.50/34.68 [b1](x0) = [0 0 1 0]x0 + [1] 98.50/34.68 [0 0 0 0] [0], 98.50/34.68 98.50/34.68 [1 0 1 0] [1] 98.50/34.68 [0 1 0 1] [0] 98.50/34.68 [a1](x0) = [0 0 1 0]x0 + [1] 98.50/34.68 [0 0 0 1] [0], 98.50/34.68 98.50/34.68 [1] 98.50/34.68 [1] 98.50/34.68 [d] = [0] 98.50/34.68 [1], 98.50/34.68 98.50/34.68 [1] 98.50/34.68 [1] 98.50/34.68 [c] = [1] 98.50/34.68 [1], 98.50/34.68 98.50/34.68 [1] 98.50/34.68 [1] 98.50/34.68 [b] = [0] 98.50/34.68 [0], 98.50/34.68 98.50/34.68 [1 0 1 0] [1 1 1 0] [1] 98.50/34.68 [0 1 0 1] [0 1 1 1] [0] 98.50/34.68 [f](x0, x1) = [0 0 0 0]x0 + [0 0 1 1]x1 + [1] 98.50/34.68 [0 0 0 0] [0 0 0 1] [1], 98.50/34.68 98.50/34.68 [1] 98.50/34.68 [1] 98.50/34.68 [a] = [0] 98.50/34.68 [0] 98.50/34.68 orientation: 98.50/34.68 [1 0 1 0] [2] [1 0 1 0] [1] 98.50/34.68 [0 0 0 0] [0] [0 0 0 0] [0] 98.50/34.68 a1(b1(x)) = [0 0 1 0]x + [2] >= [0 0 1 0]x + [2] = b1(a1(x)) 98.50/34.68 [0 0 0 0] [0] [0 0 0 0] [0] 98.50/34.68 98.50/34.68 [1 0 1 0] [2] [1 0 1 0] [2] 98.50/34.68 [0 1 1 2] [1] [0 1 1 2] [1] 98.50/34.68 a1(c1(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = c1(a1(x)) 98.50/34.68 [0 0 0 1] [1] [0 0 0 1] [1] 98.50/34.68 98.50/34.68 [1 0 1 0] [1] [1 0 0 0] [1] 98.50/34.68 [0 1 0 1] [0] [0 0 0 0] [0] 98.50/34.68 a1(x) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = b1(c1(x)) 98.50/34.68 [0 0 0 1] [0] [0 0 0 0] [0] 98.50/34.68 98.50/34.68 [1 1 1 1] [1] [1 1 1 1] [1] 98.50/34.68 [0 0 0 0] [0] [0 0 0 0] [0] 98.50/34.68 d1(c1(x)) = [0 0 0 1]x + [1] >= [0 0 0 1]x + [0] = d1(a1(x)) 98.50/34.68 [0 0 0 1] [1] [0 0 0 1] [0] 98.50/34.68 98.50/34.68 [1 1 1 0] [2] [1 0 1 0] [1] 98.50/34.68 [0 1 1 1] [1] [0 1 0 1] [0] 98.50/34.68 f(a(),x1) = [0 0 1 1]x1 + [1] >= [0 0 1 0]x1 + [1] = a1(x1) 98.50/34.68 [0 0 0 1] [1] [0 0 0 1] [0] 98.50/34.68 98.50/34.68 [1 1 1 0] [2] [1 0 0 0] [0] 98.50/34.68 [0 1 1 1] [1] [0 0 0 0] [0] 98.50/34.68 f(b(),x1) = [0 0 1 1]x1 + [1] >= [0 0 1 0]x1 + [1] = b1(x1) 98.50/34.68 [0 0 0 1] [1] [0 0 0 0] [0] 98.50/34.68 98.50/34.68 [1 1 1 0] [3] [1 0 0 0] [1] 98.50/34.68 [0 1 1 1] [2] [0 1 1 1] [0] 98.50/34.68 f(c(),x1) = [0 0 1 1]x1 + [1] >= [0 0 1 0]x1 + [0] = c1(x1) 98.50/34.68 [0 0 0 1] [1] [0 0 0 1] [1] 98.50/34.68 98.50/34.68 [1 1 1 0] [2] [1 1 0 0] 98.50/34.68 [0 1 1 1] [2] [0 0 0 0] 98.50/34.68 f(d(),x1) = [0 0 1 1]x1 + [1] >= [0 0 0 1]x1 = d1(x1) 98.50/34.68 [0 0 0 1] [1] [0 0 0 1] 98.50/34.68 problem: 98.50/34.68 strict: 98.50/34.68 98.50/34.68 weak: 98.50/34.68 a1(b1(x)) -> b1(a1(x)) 98.50/34.68 a1(c1(x)) -> c1(a1(x)) 98.50/34.68 a1(x) -> b1(c1(x)) 98.50/34.68 d1(c1(x)) -> d1(a1(x)) 98.50/34.68 f(a(),x1) -> a1(x1) 98.50/34.68 f(b(),x1) -> b1(x1) 98.50/34.68 f(c(),x1) -> c1(x1) 98.50/34.68 f(d(),x1) -> d1(x1) 98.50/34.68 Qed 98.50/34.69 EOF