YES(?,O(n^2)) 277.64/179.29 YES(?,O(n^2)) 277.64/179.29 277.64/179.29 Problem: 277.64/179.29 f(a(),f(a(),x)) -> f(c(),f(b(),x)) 277.64/179.29 f(b(),f(b(),x)) -> f(a(),f(c(),x)) 277.64/179.29 f(c(),f(c(),x)) -> f(b(),f(a(),x)) 277.64/179.29 277.64/179.29 Proof: 277.64/179.29 Uncurry Processor: 277.64/179.29 a1(a1(x)) -> c1(b1(x)) 277.64/179.29 b1(b1(x)) -> a1(c1(x)) 277.64/179.29 c1(c1(x)) -> b1(a1(x)) 277.64/179.29 f(a(),x1) -> a1(x1) 277.64/179.29 f(c(),x1) -> c1(x1) 277.64/179.29 f(b(),x1) -> b1(x1) 277.64/179.29 Complexity Transformation Processor: 277.64/179.29 strict: 277.64/179.29 a1(a1(x)) -> c1(b1(x)) 277.64/179.29 b1(b1(x)) -> a1(c1(x)) 277.64/179.29 c1(c1(x)) -> b1(a1(x)) 277.64/179.29 f(a(),x1) -> a1(x1) 277.64/179.29 f(c(),x1) -> c1(x1) 277.64/179.29 f(b(),x1) -> b1(x1) 277.64/179.29 weak: 277.64/179.29 277.64/179.29 Matrix Interpretation Processor: dim=1 277.64/179.29 277.64/179.29 max_matrix: 277.64/179.29 1 277.64/179.29 interpretation: 277.64/179.29 [b1](x0) = x0 + 6, 277.64/179.29 277.64/179.29 [c1](x0) = x0 + 12, 277.64/179.29 277.64/179.29 [a1](x0) = x0 + 6, 277.64/179.29 277.64/179.29 [b] = 1, 277.64/179.29 277.64/179.29 [c] = 0, 277.64/179.29 277.64/179.29 [f](x0, x1) = x0 + x1 + 6, 277.64/179.29 277.64/179.29 [a] = 0 277.64/179.29 orientation: 277.64/179.29 a1(a1(x)) = x + 12 >= x + 18 = c1(b1(x)) 277.64/179.29 277.64/179.29 b1(b1(x)) = x + 12 >= x + 18 = a1(c1(x)) 277.64/179.29 277.64/179.29 c1(c1(x)) = x + 24 >= x + 12 = b1(a1(x)) 277.64/179.29 277.64/179.29 f(a(),x1) = x1 + 6 >= x1 + 6 = a1(x1) 277.64/179.29 277.64/179.29 f(c(),x1) = x1 + 6 >= x1 + 12 = c1(x1) 277.64/179.29 277.64/179.29 f(b(),x1) = x1 + 7 >= x1 + 6 = b1(x1) 277.64/179.29 problem: 277.64/179.29 strict: 277.64/179.29 a1(a1(x)) -> c1(b1(x)) 277.64/179.29 b1(b1(x)) -> a1(c1(x)) 277.64/179.29 f(a(),x1) -> a1(x1) 277.64/179.29 f(c(),x1) -> c1(x1) 277.64/179.29 weak: 277.64/179.29 c1(c1(x)) -> b1(a1(x)) 277.64/179.29 f(b(),x1) -> b1(x1) 277.64/179.29 Matrix Interpretation Processor: dim=1 277.64/179.29 277.64/179.29 max_matrix: 277.64/179.29 1 277.64/179.29 interpretation: 277.64/179.29 [b1](x0) = x0 + 24, 277.64/179.29 277.64/179.29 [c1](x0) = x0 + 16, 277.64/179.29 277.64/179.29 [a1](x0) = x0 + 8, 277.64/179.29 277.64/179.29 [b] = 17, 277.64/179.29 277.64/179.29 [c] = 132, 277.64/179.29 277.64/179.29 [f](x0, x1) = x0 + x1 + 8, 277.64/179.29 277.64/179.29 [a] = 0 277.64/179.29 orientation: 277.64/179.29 a1(a1(x)) = x + 16 >= x + 40 = c1(b1(x)) 277.64/179.29 277.64/179.29 b1(b1(x)) = x + 48 >= x + 24 = a1(c1(x)) 277.64/179.29 277.64/179.29 f(a(),x1) = x1 + 8 >= x1 + 8 = a1(x1) 277.64/179.29 277.64/179.29 f(c(),x1) = x1 + 140 >= x1 + 16 = c1(x1) 277.64/179.29 277.64/179.29 c1(c1(x)) = x + 32 >= x + 32 = b1(a1(x)) 277.64/179.29 277.64/179.29 f(b(),x1) = x1 + 25 >= x1 + 24 = b1(x1) 277.64/179.29 problem: 277.64/179.29 strict: 277.64/179.29 a1(a1(x)) -> c1(b1(x)) 277.64/179.29 f(a(),x1) -> a1(x1) 277.64/179.29 weak: 277.64/179.29 b1(b1(x)) -> a1(c1(x)) 277.64/179.29 f(c(),x1) -> c1(x1) 277.64/179.29 c1(c1(x)) -> b1(a1(x)) 277.64/179.29 f(b(),x1) -> b1(x1) 277.64/179.29 Matrix Interpretation Processor: dim=1 277.64/179.29 277.64/179.29 max_matrix: 277.64/179.29 1 277.64/179.29 interpretation: 277.64/179.29 [b1](x0) = x0 + 8, 277.64/179.29 277.64/179.29 [c1](x0) = x0 + 8, 277.64/179.29 277.64/179.29 [a1](x0) = x0 + 8, 277.64/179.29 277.64/179.29 [b] = 8, 277.64/179.29 277.64/179.29 [c] = 8, 277.64/179.29 277.64/179.29 [f](x0, x1) = x0 + x1, 277.64/179.29 277.64/179.29 [a] = 12 277.64/179.29 orientation: 277.64/179.29 a1(a1(x)) = x + 16 >= x + 16 = c1(b1(x)) 277.64/179.29 277.64/179.29 f(a(),x1) = x1 + 12 >= x1 + 8 = a1(x1) 277.64/179.29 277.64/179.29 b1(b1(x)) = x + 16 >= x + 16 = a1(c1(x)) 277.64/179.29 277.64/179.29 f(c(),x1) = x1 + 8 >= x1 + 8 = c1(x1) 277.64/179.29 277.64/179.29 c1(c1(x)) = x + 16 >= x + 16 = b1(a1(x)) 277.64/179.29 277.64/179.29 f(b(),x1) = x1 + 8 >= x1 + 8 = b1(x1) 277.64/179.29 problem: 277.64/179.29 strict: 277.64/179.29 a1(a1(x)) -> c1(b1(x)) 277.64/179.29 weak: 277.64/179.29 f(a(),x1) -> a1(x1) 277.64/179.29 b1(b1(x)) -> a1(c1(x)) 277.64/179.29 f(c(),x1) -> c1(x1) 277.64/179.29 c1(c1(x)) -> b1(a1(x)) 277.64/179.29 f(b(),x1) -> b1(x1) 277.64/179.29 Matrix Interpretation Processor: dim=4 277.64/179.29 277.64/179.29 max_matrix: 277.64/179.29 [1 2 1 1] 277.64/179.29 [0 0 0 1] 277.64/179.29 [0 1 0 0] 277.64/179.29 [0 0 1 0] 277.64/179.29 interpretation: 277.64/179.29 [1 1 0 1] [0] 277.64/179.29 [0 0 0 1] [0] 277.64/179.29 [b1](x0) = [0 1 0 0]x0 + [0] 277.64/179.29 [0 0 1 0] [2], 277.64/179.29 277.64/179.29 [1 1 1 0] [1] 277.64/179.29 [0 0 0 1] [0] 277.64/179.29 [c1](x0) = [0 1 0 0]x0 + [2] 277.64/179.29 [0 0 1 0] [0], 277.64/179.29 277.64/179.29 [1 2 0 0] [0] 277.64/179.29 [0 0 0 1] [2] 277.64/179.29 [a1](x0) = [0 1 0 0]x0 + [0] 277.64/179.29 [0 0 1 0] [0], 277.64/179.29 277.64/179.29 [1] 277.64/179.29 [0] 277.64/179.29 [b] = [1] 277.64/179.29 [1], 277.64/179.29 277.64/179.29 [1] 277.64/179.29 [1] 277.64/179.29 [c] = [3] 277.64/179.29 [1], 277.64/179.29 277.64/179.29 [1 1 0 1] [1 2 1 1] [0] 277.64/179.29 [0 0 0 1] [0 0 0 1] [0] 277.64/179.29 [f](x0, x1) = [0 0 0 0]x0 + [0 1 0 0]x1 + [3] 277.64/179.29 [0 0 1 0] [0 0 1 0] [3], 277.64/179.29 277.64/179.29 [1] 277.64/179.29 [1] 277.64/179.29 [a] = [0] 277.64/179.29 [2] 277.64/179.29 orientation: 277.64/179.29 [1 2 0 2] [4] [1 2 0 2] [1] 277.64/179.29 [0 0 1 0] [2] [0 0 1 0] [2] 277.64/179.29 a1(a1(x)) = [0 0 0 1]x + [2] >= [0 0 0 1]x + [2] = c1(b1(x)) 277.64/179.29 [0 1 0 0] [0] [0 1 0 0] [0] 277.64/179.29 277.64/179.29 [1 2 1 1] [4] [1 2 0 0] [0] 277.64/179.29 [0 0 0 1] [2] [0 0 0 1] [2] 277.64/179.29 f(a(),x1) = [0 1 0 0]x1 + [3] >= [0 1 0 0]x1 + [0] = a1(x1) 277.64/179.29 [0 0 1 0] [3] [0 0 1 0] [0] 277.64/179.29 277.64/179.29 [1 1 1 2] [2] [1 1 1 2] [1] 277.64/179.29 [0 0 1 0] [2] [0 0 1 0] [2] 277.64/179.29 b1(b1(x)) = [0 0 0 1]x + [0] >= [0 0 0 1]x + [0] = a1(c1(x)) 277.64/179.29 [0 1 0 0] [2] [0 1 0 0] [2] 277.64/179.29 277.64/179.29 [1 2 1 1] [3] [1 1 1 0] [1] 277.64/179.29 [0 0 0 1] [1] [0 0 0 1] [0] 277.64/179.29 f(c(),x1) = [0 1 0 0]x1 + [3] >= [0 1 0 0]x1 + [2] = c1(x1) 277.64/179.29 [0 0 1 0] [6] [0 0 1 0] [0] 277.64/179.29 277.64/179.29 [1 2 1 1] [4] [1 2 1 1] [2] 277.64/179.29 [0 0 1 0] [0] [0 0 1 0] [0] 277.64/179.29 c1(c1(x)) = [0 0 0 1]x + [2] >= [0 0 0 1]x + [2] = b1(a1(x)) 277.64/179.29 [0 1 0 0] [2] [0 1 0 0] [2] 277.64/179.29 277.64/179.29 [1 2 1 1] [2] [1 1 0 1] [0] 277.64/179.29 [0 0 0 1] [1] [0 0 0 1] [0] 277.64/179.29 f(b(),x1) = [0 1 0 0]x1 + [3] >= [0 1 0 0]x1 + [0] = b1(x1) 277.64/179.29 [0 0 1 0] [4] [0 0 1 0] [2] 277.64/179.29 problem: 277.64/179.29 strict: 277.64/179.29 277.64/179.29 weak: 277.64/179.29 a1(a1(x)) -> c1(b1(x)) 277.64/179.29 f(a(),x1) -> a1(x1) 277.64/179.29 b1(b1(x)) -> a1(c1(x)) 277.64/179.29 f(c(),x1) -> c1(x1) 277.64/179.29 c1(c1(x)) -> b1(a1(x)) 277.64/179.29 f(b(),x1) -> b1(x1) 277.64/179.29 Qed 277.64/179.30 EOF