YES(?,O(n^2)) 51.11/26.76 YES(?,O(n^2)) 51.11/26.77 51.11/26.77 Problem: 51.11/26.77 f(a(),f(b(),x)) -> f(b(),f(a(),x)) 51.11/26.77 f(b(),f(c(),x)) -> f(c(),f(b(),x)) 51.11/26.77 f(c(),f(a(),x)) -> f(a(),f(c(),x)) 51.11/26.77 51.11/26.77 Proof: 51.11/26.77 Uncurry Processor: 51.11/26.77 a1(b1(x)) -> b1(a1(x)) 51.11/26.77 b1(c1(x)) -> c1(b1(x)) 51.11/26.77 c1(a1(x)) -> a1(c1(x)) 51.11/26.77 f(a(),x1) -> a1(x1) 51.11/26.77 f(b(),x1) -> b1(x1) 51.11/26.77 f(c(),x1) -> c1(x1) 51.11/26.77 Complexity Transformation Processor: 51.11/26.77 strict: 51.11/26.77 a1(b1(x)) -> b1(a1(x)) 51.11/26.77 b1(c1(x)) -> c1(b1(x)) 51.11/26.77 c1(a1(x)) -> a1(c1(x)) 51.11/26.77 f(a(),x1) -> a1(x1) 51.11/26.77 f(b(),x1) -> b1(x1) 51.11/26.77 f(c(),x1) -> c1(x1) 51.11/26.77 weak: 51.11/26.77 51.11/26.77 Matrix Interpretation Processor: dim=1 51.11/26.77 51.11/26.77 max_matrix: 51.11/26.77 1 51.11/26.77 interpretation: 51.11/26.77 [c1](x0) = x0 + 20, 51.11/26.77 51.11/26.77 [b1](x0) = x0 + 128, 51.11/26.77 51.11/26.77 [a1](x0) = x0 + 28, 51.11/26.77 51.11/26.77 [c] = 65, 51.11/26.77 51.11/26.77 [f](x0, x1) = x0 + x1 + 220, 51.11/26.77 51.11/26.77 [b] = 0, 51.11/26.77 51.11/26.77 [a] = 41 51.11/26.77 orientation: 51.11/26.77 a1(b1(x)) = x + 156 >= x + 156 = b1(a1(x)) 51.11/26.77 51.11/26.77 b1(c1(x)) = x + 148 >= x + 148 = c1(b1(x)) 51.11/26.77 51.11/26.77 c1(a1(x)) = x + 48 >= x + 48 = a1(c1(x)) 51.11/26.77 51.11/26.77 f(a(),x1) = x1 + 261 >= x1 + 28 = a1(x1) 51.11/26.77 51.11/26.77 f(b(),x1) = x1 + 220 >= x1 + 128 = b1(x1) 51.11/26.77 51.11/26.77 f(c(),x1) = x1 + 285 >= x1 + 20 = c1(x1) 51.11/26.77 problem: 51.11/26.77 strict: 51.11/26.77 a1(b1(x)) -> b1(a1(x)) 51.11/26.77 b1(c1(x)) -> c1(b1(x)) 51.11/26.77 c1(a1(x)) -> a1(c1(x)) 51.11/26.77 weak: 51.11/26.77 f(a(),x1) -> a1(x1) 51.11/26.77 f(b(),x1) -> b1(x1) 51.11/26.77 f(c(),x1) -> c1(x1) 51.11/26.77 Splitting Processor: 51.11/26.77 strict: 51.11/26.77 c1(a1(x)) -> a1(c1(x)) 51.11/26.77 weak: 51.11/26.77 f(a(),x1) -> a1(x1) 51.11/26.77 f(b(),x1) -> b1(x1) 51.11/26.77 f(c(),x1) -> c1(x1) 51.11/26.77 a1(b1(x)) -> b1(a1(x)) 51.11/26.77 b1(c1(x)) -> c1(b1(x)) 51.11/26.77 Matrix Interpretation Processor: dim=4 51.11/26.77 51.11/26.77 max_matrix: 51.11/26.77 [1 1 1 1] 51.11/26.77 [0 0 1 1] 51.11/26.77 [0 0 0 1] 51.11/26.77 [0 0 0 1] 51.11/26.77 interpretation: 51.11/26.77 [1 0 0 1] [1] 51.11/26.77 [0 0 0 0] [0] 51.11/26.77 [c1](x0) = [0 0 0 0]x0 + [0] 51.11/26.77 [0 0 0 1] [0], 51.11/26.77 51.11/26.77 [1 0 0 0] 51.11/26.77 [0 0 0 0] 51.11/26.77 [b1](x0) = [0 0 0 0]x0 51.11/26.77 [0 0 0 0] , 51.11/26.77 51.11/26.77 [1 0 0 0] [0] 51.11/26.77 [0 0 0 0] [0] 51.11/26.77 [a1](x0) = [0 0 0 0]x0 + [0] 51.11/26.77 [0 0 0 1] [1], 51.11/26.77 51.11/26.77 [0] 51.11/26.77 [0] 51.11/26.77 [c] = [0] 51.11/26.77 [0], 51.11/26.77 51.11/26.77 [1 1 1 0] [1 1 1 1] [1] 51.11/26.77 [0 0 1 0] [0 0 1 1] [1] 51.11/26.77 [f](x0, x1) = [0 0 0 1]x0 + [0 0 0 1]x1 + [0] 51.11/26.77 [0 0 0 0] [0 0 0 1] [1], 51.11/26.77 51.11/26.77 [1] 51.11/26.77 [0] 51.11/26.77 [b] = [0] 51.11/26.77 [1], 51.11/26.77 51.11/26.77 [0] 51.11/26.77 [0] 51.11/26.77 [a] = [0] 51.11/26.77 [0] 51.11/26.77 orientation: 51.11/26.77 [1 0 0 1] [2] [1 0 0 1] [1] 51.11/26.77 [0 0 0 0] [0] [0 0 0 0] [0] 51.11/26.77 c1(a1(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = a1(c1(x)) 51.11/26.77 [0 0 0 1] [1] [0 0 0 1] [1] 51.11/26.77 51.11/26.77 [1 1 1 1] [1] [1 0 0 0] [0] 51.11/26.77 [0 0 1 1] [1] [0 0 0 0] [0] 51.11/26.77 f(a(),x1) = [0 0 0 1]x1 + [0] >= [0 0 0 0]x1 + [0] = a1(x1) 51.11/26.77 [0 0 0 1] [1] [0 0 0 1] [1] 51.11/26.77 51.11/26.77 [1 1 1 1] [2] [1 0 0 0] 51.11/26.77 [0 0 1 1] [1] [0 0 0 0] 51.11/26.77 f(b(),x1) = [0 0 0 1]x1 + [1] >= [0 0 0 0]x1 = b1(x1) 51.11/26.77 [0 0 0 1] [1] [0 0 0 0] 51.11/26.77 51.11/26.77 [1 1 1 1] [1] [1 0 0 1] [1] 51.11/26.77 [0 0 1 1] [1] [0 0 0 0] [0] 51.11/26.77 f(c(),x1) = [0 0 0 1]x1 + [0] >= [0 0 0 0]x1 + [0] = c1(x1) 51.11/26.77 [0 0 0 1] [1] [0 0 0 1] [0] 51.11/26.77 51.11/26.77 [1 0 0 0] [0] [1 0 0 0] 51.11/26.77 [0 0 0 0] [0] [0 0 0 0] 51.11/26.77 a1(b1(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x = b1(a1(x)) 51.11/26.77 [0 0 0 0] [1] [0 0 0 0] 51.11/26.77 51.11/26.77 [1 0 0 1] [1] [1 0 0 0] [1] 51.11/26.77 [0 0 0 0] [0] [0 0 0 0] [0] 51.11/26.77 b1(c1(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = c1(b1(x)) 51.11/26.77 [0 0 0 0] [0] [0 0 0 0] [0] 51.11/26.77 problem: 51.11/26.77 strict: 51.11/26.77 51.11/26.77 weak: 51.11/26.77 c1(a1(x)) -> a1(c1(x)) 51.11/26.77 f(a(),x1) -> a1(x1) 51.11/26.77 f(b(),x1) -> b1(x1) 51.11/26.77 f(c(),x1) -> c1(x1) 51.11/26.77 a1(b1(x)) -> b1(a1(x)) 51.11/26.77 b1(c1(x)) -> c1(b1(x)) 51.11/26.77 Qed 51.11/26.77 51.11/26.77 strict: 51.11/26.77 a1(b1(x)) -> b1(a1(x)) 51.11/26.77 b1(c1(x)) -> c1(b1(x)) 51.11/26.77 weak: 51.11/26.77 c1(a1(x)) -> a1(c1(x)) 51.11/26.77 f(a(),x1) -> a1(x1) 51.11/26.77 f(b(),x1) -> b1(x1) 51.11/26.77 f(c(),x1) -> c1(x1) 51.11/26.77 Splitting Processor: 51.11/26.77 strict: 51.11/26.77 a1(b1(x)) -> b1(a1(x)) 51.11/26.77 weak: 51.11/26.77 c1(a1(x)) -> a1(c1(x)) 51.11/26.77 f(a(),x1) -> a1(x1) 51.11/26.77 f(b(),x1) -> b1(x1) 51.11/26.77 f(c(),x1) -> c1(x1) 51.11/26.77 b1(c1(x)) -> c1(b1(x)) 51.11/26.77 Matrix Interpretation Processor: dim=2 51.11/26.77 51.11/26.77 max_matrix: 51.11/26.77 [1 1] 51.11/26.77 [0 1] 51.11/26.77 interpretation: 51.11/26.77 [0] 51.11/26.77 [c1](x0) = x0 + [2], 51.11/26.77 51.11/26.77 [1 1] [0] 51.11/26.77 [b1](x0) = [0 1]x0 + [1], 51.11/26.77 51.11/26.77 [7] 51.11/26.77 [a1](x0) = x0 + [0], 51.11/26.77 51.11/26.77 [0] 51.11/26.77 [c] = [2], 51.11/26.77 51.11/26.77 [1 1] 51.11/26.77 [f](x0, x1) = x0 + [0 1]x1, 51.11/26.77 51.11/26.77 [0] 51.11/26.77 [b] = [1], 51.11/26.77 51.11/26.77 [7] 51.11/26.77 [a] = [0] 51.11/26.77 orientation: 51.11/26.77 [1 1] [2] [1 1] [0] 51.11/26.77 b1(c1(x)) = [0 1]x + [3] >= [0 1]x + [3] = c1(b1(x)) 51.11/26.77 51.11/26.77 [1 1] [7] [1 1] [7] 51.11/26.77 a1(b1(x)) = [0 1]x + [1] >= [0 1]x + [1] = b1(a1(x)) 51.11/26.77 51.11/26.77 [7] [7] 51.11/26.77 c1(a1(x)) = x + [2] >= x + [2] = a1(c1(x)) 51.11/26.77 51.11/26.77 [1 1] [7] [7] 51.11/26.77 f(a(),x1) = [0 1]x1 + [0] >= x1 + [0] = a1(x1) 51.11/26.77 51.11/26.77 [1 1] [0] [1 1] [0] 51.11/26.77 f(b(),x1) = [0 1]x1 + [1] >= [0 1]x1 + [1] = b1(x1) 51.11/26.77 51.11/26.77 [1 1] [0] [0] 51.11/26.77 f(c(),x1) = [0 1]x1 + [2] >= x1 + [2] = c1(x1) 51.11/26.77 problem: 51.11/26.77 strict: 51.11/26.77 51.11/26.77 weak: 51.11/26.77 b1(c1(x)) -> c1(b1(x)) 51.11/26.77 a1(b1(x)) -> b1(a1(x)) 51.11/26.77 c1(a1(x)) -> a1(c1(x)) 51.11/26.77 f(a(),x1) -> a1(x1) 51.11/26.77 f(b(),x1) -> b1(x1) 51.11/26.77 f(c(),x1) -> c1(x1) 51.11/26.77 Qed 51.11/26.77 51.11/26.77 strict: 51.11/26.77 b1(c1(x)) -> c1(b1(x)) 51.11/26.77 weak: 51.11/26.77 a1(b1(x)) -> b1(a1(x)) 51.11/26.77 c1(a1(x)) -> a1(c1(x)) 51.11/26.77 f(a(),x1) -> a1(x1) 51.11/26.77 f(b(),x1) -> b1(x1) 51.11/26.77 f(c(),x1) -> c1(x1) 51.11/26.77 Matrix Interpretation Processor: dim=5 51.11/26.77 51.11/26.77 max_matrix: 51.11/26.77 [1 0 1 0 1] 51.11/26.77 [0 0 1 1 1] 51.11/26.77 [0 0 0 1 1] 51.11/26.77 [0 0 0 0 1] 51.11/26.77 [0 0 0 0 1] 51.11/26.77 interpretation: 51.11/26.77 [1 0 0 0 0] [1] 51.11/26.77 [0 0 0 0 0] [0] 51.11/26.77 [c1](x0) = [0 0 0 0 0]x0 + [0] 51.11/26.77 [0 0 0 0 0] [0] 51.11/26.77 [0 0 0 0 0] [0], 51.11/26.77 51.11/26.77 [1 0 0 0 0] [0] 51.11/26.77 [0 0 0 0 0] [0] 51.11/26.77 [b1](x0) = [0 0 0 0 0]x0 + [0] 51.11/26.77 [0 0 0 0 0] [0] 51.11/26.77 [0 0 0 0 1] [1], 51.11/26.77 51.11/26.77 [1 0 0 0 1] [1] 51.11/26.77 [0 0 0 0 0] [0] 51.11/26.77 [a1](x0) = [0 0 0 0 0]x0 + [0] 51.11/26.77 [0 0 0 0 0] [0] 51.11/26.77 [0 0 0 0 1] [0], 51.11/26.77 51.11/26.77 [0] 51.11/26.77 [0] 51.11/26.77 [c] = [0] 51.11/26.77 [0] 51.11/26.77 [0], 51.11/26.77 51.11/26.77 [1 0 0 0 0] [1 0 1 0 1] [1] 51.11/26.77 [0 0 1 1 0] [0 0 0 0 1] [0] 51.11/26.77 [f](x0, x1) = [0 0 0 0 0]x0 + [0 0 0 1 1]x1 + [0] 51.11/26.77 [0 0 0 0 1] [0 0 0 0 0] [1] 51.11/26.77 [0 0 0 0 1] [0 0 0 0 1] [1], 51.11/26.77 51.11/26.77 [0] 51.11/26.77 [0] 51.11/26.77 [b] = [0] 51.11/26.77 [0] 51.11/26.77 [1], 51.11/26.77 51.11/26.77 [1] 51.11/26.77 [0] 51.11/26.77 [a] = [1] 51.11/26.77 [1] 51.11/26.77 [0] 51.11/26.77 orientation: 51.11/26.77 [1 0 0 0 1] [2] [1 0 0 0 1] [1] 51.11/26.77 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 51.11/26.77 a1(b1(x)) = [0 0 0 0 0]x + [0] >= [0 0 0 0 0]x + [0] = b1(a1(x)) 51.11/26.78 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 51.11/26.78 [0 0 0 0 1] [1] [0 0 0 0 1] [1] 51.11/26.78 51.11/26.78 [1 0 0 0 1] [2] [1 0 0 0 0] [2] 51.11/26.78 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 51.11/26.78 c1(a1(x)) = [0 0 0 0 0]x + [0] >= [0 0 0 0 0]x + [0] = a1(c1(x)) 51.11/26.78 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 51.11/26.78 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 51.11/26.78 51.11/26.78 [1 0 1 0 1] [2] [1 0 0 0 1] [1] 51.11/26.78 [0 0 0 0 1] [2] [0 0 0 0 0] [0] 51.11/26.78 f(a(),x1) = [0 0 0 1 1]x1 + [0] >= [0 0 0 0 0]x1 + [0] = a1(x1) 51.11/26.78 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 51.11/26.78 [0 0 0 0 1] [1] [0 0 0 0 1] [0] 51.11/26.78 51.11/26.78 [1 0 1 0 1] [1] [1 0 0 0 0] [0] 51.11/26.78 [0 0 0 0 1] [0] [0 0 0 0 0] [0] 51.11/26.78 f(b(),x1) = [0 0 0 1 1]x1 + [0] >= [0 0 0 0 0]x1 + [0] = b1(x1) 51.11/26.78 [0 0 0 0 0] [2] [0 0 0 0 0] [0] 51.11/26.78 [0 0 0 0 1] [2] [0 0 0 0 1] [1] 51.11/26.78 51.11/26.78 [1 0 1 0 1] [1] [1 0 0 0 0] [1] 51.11/26.78 [0 0 0 0 1] [0] [0 0 0 0 0] [0] 51.11/26.78 f(c(),x1) = [0 0 0 1 1]x1 + [0] >= [0 0 0 0 0]x1 + [0] = c1(x1) 51.11/26.78 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 51.11/26.78 [0 0 0 0 1] [1] [0 0 0 0 0] [0] 51.11/26.78 51.11/26.78 [1 0 0 0 0] [1] [1 0 0 0 0] [1] 51.11/26.78 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 51.11/26.78 b1(c1(x)) = [0 0 0 0 0]x + [0] >= [0 0 0 0 0]x + [0] = c1(b1(x)) 51.11/26.78 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 51.11/26.78 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 51.11/26.78 problem: 51.11/26.78 strict: 51.11/26.78 51.11/26.78 weak: 51.11/26.78 a1(b1(x)) -> b1(a1(x)) 51.11/26.78 c1(a1(x)) -> a1(c1(x)) 51.11/26.78 f(a(),x1) -> a1(x1) 51.11/26.78 f(b(),x1) -> b1(x1) 51.11/26.78 f(c(),x1) -> c1(x1) 51.11/26.78 b1(c1(x)) -> c1(b1(x)) 51.11/26.78 Qed 51.11/26.78 EOF