YES(?,O(n^2)) 48.37/29.20 YES(?,O(n^2)) 48.37/29.21 48.37/29.21 Problem: 48.37/29.21 a__f(a(),X,X) -> a__f(X,a__b(),b()) 48.37/29.21 a__b() -> a() 48.37/29.21 mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) 48.37/29.21 mark(b()) -> a__b() 48.37/29.21 mark(a()) -> a() 48.37/29.21 a__f(X1,X2,X3) -> f(X1,X2,X3) 48.37/29.21 a__b() -> b() 48.37/29.21 48.37/29.21 Proof: 48.37/29.21 Complexity Transformation Processor: 48.37/29.21 strict: 48.37/29.21 a__f(a(),X,X) -> a__f(X,a__b(),b()) 48.37/29.21 a__b() -> a() 48.37/29.21 mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) 48.37/29.21 mark(b()) -> a__b() 48.37/29.21 mark(a()) -> a() 48.37/29.21 a__f(X1,X2,X3) -> f(X1,X2,X3) 48.37/29.21 a__b() -> b() 48.37/29.21 weak: 48.37/29.21 48.37/29.21 Matrix Interpretation Processor: dim=1 48.37/29.21 48.37/29.21 max_matrix: 48.37/29.21 1 48.37/29.21 interpretation: 48.37/29.21 [mark](x0) = x0 + 35, 48.37/29.21 48.37/29.21 [f](x0, x1, x2) = x0 + x1 + x2 + 4, 48.37/29.21 48.37/29.21 [b] = 32, 48.37/29.21 48.37/29.21 [a__b] = 113, 48.37/29.21 48.37/29.21 [a__f](x0, x1, x2) = x0 + x1 + x2 + 13, 48.37/29.21 48.37/29.21 [a] = 108 48.37/29.21 orientation: 48.37/29.21 a__f(a(),X,X) = 2X + 121 >= X + 158 = a__f(X,a__b(),b()) 48.37/29.21 48.37/29.21 a__b() = 113 >= 108 = a() 48.37/29.21 48.37/29.21 mark(f(X1,X2,X3)) = X1 + X2 + X3 + 39 >= X1 + X2 + X3 + 48 = a__f(X1,mark(X2),X3) 48.37/29.21 48.37/29.21 mark(b()) = 67 >= 113 = a__b() 48.37/29.21 48.37/29.21 mark(a()) = 143 >= 108 = a() 48.37/29.21 48.37/29.21 a__f(X1,X2,X3) = X1 + X2 + X3 + 13 >= X1 + X2 + X3 + 4 = f(X1,X2,X3) 48.37/29.21 48.37/29.21 a__b() = 113 >= 32 = b() 48.37/29.21 problem: 48.37/29.21 strict: 48.37/29.21 a__f(a(),X,X) -> a__f(X,a__b(),b()) 48.37/29.21 mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) 48.37/29.21 mark(b()) -> a__b() 48.37/29.21 weak: 48.37/29.21 a__b() -> a() 48.37/29.21 mark(a()) -> a() 48.37/29.21 a__f(X1,X2,X3) -> f(X1,X2,X3) 48.37/29.21 a__b() -> b() 48.37/29.21 Matrix Interpretation Processor: dim=1 48.37/29.21 48.37/29.21 max_matrix: 48.37/29.21 1 48.37/29.21 interpretation: 48.37/29.21 [mark](x0) = x0 + 8, 48.37/29.21 48.37/29.21 [f](x0, x1, x2) = x0 + x1 + x2, 48.37/29.21 48.37/29.21 [b] = 0, 48.37/29.21 48.37/29.21 [a__b] = 2, 48.37/29.21 48.37/29.21 [a__f](x0, x1, x2) = x0 + x1 + x2 + 1, 48.37/29.21 48.37/29.21 [a] = 0 48.37/29.21 orientation: 48.37/29.21 a__f(a(),X,X) = 2X + 1 >= X + 3 = a__f(X,a__b(),b()) 48.37/29.21 48.37/29.21 mark(f(X1,X2,X3)) = X1 + X2 + X3 + 8 >= X1 + X2 + X3 + 9 = a__f(X1,mark(X2),X3) 48.37/29.21 48.37/29.21 mark(b()) = 8 >= 2 = a__b() 48.37/29.21 48.37/29.21 a__b() = 2 >= 0 = a() 48.37/29.21 48.37/29.21 mark(a()) = 8 >= 0 = a() 48.37/29.21 48.37/29.21 a__f(X1,X2,X3) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 = f(X1,X2,X3) 48.37/29.21 48.37/29.21 a__b() = 2 >= 0 = b() 48.37/29.21 problem: 48.37/29.21 strict: 48.37/29.21 a__f(a(),X,X) -> a__f(X,a__b(),b()) 48.37/29.21 mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) 48.37/29.21 weak: 48.37/29.21 mark(b()) -> a__b() 48.37/29.21 a__b() -> a() 48.37/29.21 mark(a()) -> a() 48.37/29.21 a__f(X1,X2,X3) -> f(X1,X2,X3) 48.37/29.21 a__b() -> b() 48.37/29.21 Splitting Processor: 48.37/29.21 strict: 48.37/29.21 a__f(a(),X,X) -> a__f(X,a__b(),b()) 48.37/29.21 weak: 48.37/29.21 mark(b()) -> a__b() 48.37/29.21 a__b() -> a() 48.37/29.21 mark(a()) -> a() 48.37/29.21 a__f(X1,X2,X3) -> f(X1,X2,X3) 48.37/29.21 a__b() -> b() 48.37/29.21 mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) 48.37/29.21 Matrix Interpretation Processor: dim=5 48.37/29.21 48.37/29.21 max_matrix: 48.37/29.21 [1 1 1 1 1] 48.37/29.21 [0 1 0 1 1] 48.37/29.21 [0 0 0 0 0] 48.37/29.21 [0 0 0 0 0] 48.37/29.21 [0 0 0 0 0] 48.37/29.21 interpretation: 48.37/29.21 [1 0 0 0 0] [1] 48.37/29.21 [0 1 0 0 1] [1] 48.37/29.21 [mark](x0) = [0 0 0 0 0]x0 + [0] 48.37/29.21 [0 0 0 0 0] [1] 48.37/29.21 [0 0 0 0 0] [1], 48.37/29.21 48.37/29.21 [1 0 0 1 1] [1 0 1 0 0] [1 1 0 1 1] [0] 48.37/29.21 [0 0 0 0 1] [0 0 0 0 0] [0 0 0 1 1] [0] 48.37/29.21 [f](x0, x1, x2) = [0 0 0 0 0]x0 + [0 0 0 0 0]x1 + [0 0 0 0 0]x2 + [0] 48.37/29.21 [0 0 0 0 0] [0 0 0 0 0] [0 0 0 0 0] [0] 48.37/29.21 [0 0 0 0 0] [0 0 0 0 0] [0 0 0 0 0] [1], 48.37/29.21 48.37/29.21 [0] 48.37/29.21 [0] 48.37/29.21 [b] = [0] 48.37/29.21 [0] 48.37/29.21 [0], 48.37/29.21 48.37/29.21 [1] 48.37/29.21 [1] 48.37/29.21 [a__b] = [0] 48.37/29.21 [1] 48.37/29.21 [1], 48.37/29.21 48.37/29.21 [1 0 0 1 1] [1 0 1 0 0] [1 1 0 1 1] [0] 48.37/29.21 [0 0 0 0 1] [0 0 0 0 1] [0 0 0 1 1] [0] 48.37/29.21 [a__f](x0, x1, x2) = [0 0 0 0 0]x0 + [0 0 0 0 0]x1 + [0 0 0 0 0]x2 + [0] 48.37/29.21 [0 0 0 0 0] [0 0 0 0 0] [0 0 0 0 0] [0] 48.37/29.21 [0 0 0 0 0] [0 0 0 0 0] [0 0 0 0 0] [1], 48.37/29.21 48.37/29.21 [0] 48.37/29.21 [0] 48.37/29.21 [a] = [0] 48.37/29.21 [1] 48.37/29.21 [1] 48.37/29.21 orientation: 48.37/29.21 [2 1 1 1 1] [2] [1 0 0 1 1] [1] 48.37/29.21 [0 0 0 1 2] [1] [0 0 0 0 1] [1] 48.37/29.21 a__f(a(),X,X) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = a__f(X,a__b(),b()) 48.37/29.21 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 48.37/29.21 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 48.37/29.21 48.37/29.21 [1] [1] 48.37/29.21 [1] [1] 48.37/29.21 mark(b()) = [0] >= [0] = a__b() 48.37/29.21 [1] [1] 48.37/29.21 [1] [1] 48.37/29.21 48.37/29.21 [1] [0] 48.37/29.21 [1] [0] 48.37/29.21 a__b() = [0] >= [0] = a() 48.37/29.21 [1] [1] 48.37/29.21 [1] [1] 48.37/29.21 48.37/29.21 [1] [0] 48.37/29.21 [2] [0] 48.37/29.21 mark(a()) = [0] >= [0] = a() 48.37/29.21 [1] [1] 48.37/29.21 [1] [1] 48.37/29.21 48.37/29.21 [1 0 0 1 1] [1 0 1 0 0] [1 1 0 1 1] [0] [1 0 0 1 1] [1 0 1 0 0] [1 1 0 1 1] [0] 48.37/29.21 [0 0 0 0 1] [0 0 0 0 1] [0 0 0 1 1] [0] [0 0 0 0 1] [0 0 0 0 0] [0 0 0 1 1] [0] 48.37/29.21 a__f(X1,X2,X3) = [0 0 0 0 0]X1 + [0 0 0 0 0]X2 + [0 0 0 0 0]X3 + [0] >= [0 0 0 0 0]X1 + [0 0 0 0 0]X2 + [0 0 0 0 0]X3 + [0] = f(X1,X2,X3) 48.37/29.21 [0 0 0 0 0] [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0 0 0 0 0] [0] 48.37/29.21 [0 0 0 0 0] [0 0 0 0 0] [0 0 0 0 0] [1] [0 0 0 0 0] [0 0 0 0 0] [0 0 0 0 0] [1] 48.37/29.21 48.37/29.21 [1] [0] 48.37/29.21 [1] [0] 48.37/29.21 a__b() = [0] >= [0] = b() 48.37/29.21 [1] [0] 48.37/29.21 [1] [0] 48.37/29.21 48.37/29.21 [1 0 0 1 1] [1 0 1 0 0] [1 1 0 1 1] [1] [1 0 0 1 1] [1 0 0 0 0] [1 1 0 1 1] [1] 48.37/29.21 [0 0 0 0 1] [0 0 0 0 0] [0 0 0 1 1] [2] [0 0 0 0 1] [0 0 0 0 0] [0 0 0 1 1] [1] 48.37/29.21 mark(f(X1,X2,X3)) = [0 0 0 0 0]X1 + [0 0 0 0 0]X2 + [0 0 0 0 0]X3 + [0] >= [0 0 0 0 0]X1 + [0 0 0 0 0]X2 + [0 0 0 0 0]X3 + [0] = a__f(X1,mark(X2),X3) 48.37/29.21 [0 0 0 0 0] [0 0 0 0 0] [0 0 0 0 0] [1] [0 0 0 0 0] [0 0 0 0 0] [0 0 0 0 0] [0] 48.37/29.21 [0 0 0 0 0] [0 0 0 0 0] [0 0 0 0 0] [1] [0 0 0 0 0] [0 0 0 0 0] [0 0 0 0 0] [1] 48.37/29.21 problem: 48.37/29.21 strict: 48.37/29.21 48.37/29.21 weak: 48.37/29.21 a__f(a(),X,X) -> a__f(X,a__b(),b()) 48.37/29.21 mark(b()) -> a__b() 48.37/29.21 a__b() -> a() 48.37/29.21 mark(a()) -> a() 48.37/29.21 a__f(X1,X2,X3) -> f(X1,X2,X3) 48.37/29.21 a__b() -> b() 48.37/29.21 mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) 48.37/29.21 Qed 48.37/29.21 48.37/29.21 strict: 48.37/29.21 mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) 48.37/29.21 weak: 48.37/29.21 a__f(a(),X,X) -> a__f(X,a__b(),b()) 48.37/29.21 mark(b()) -> a__b() 48.37/29.21 a__b() -> a() 48.37/29.21 mark(a()) -> a() 48.37/29.21 a__f(X1,X2,X3) -> f(X1,X2,X3) 48.37/29.21 a__b() -> b() 48.37/29.21 Matrix Interpretation Processor: dim=4 48.37/29.21 48.37/29.21 max_matrix: 48.37/29.21 [1 1 0 1] 48.37/29.21 [0 1 1 1] 48.37/29.21 [0 0 0 0] 48.37/29.21 [0 0 0 0] 48.37/29.21 interpretation: 48.37/29.21 [1 1 0 0] [1] 48.37/29.21 [0 1 0 0] [0] 48.37/29.21 [mark](x0) = [0 0 0 0]x0 + [1] 48.37/29.21 [0 0 0 0] [0], 48.37/29.21 48.37/29.21 [1 0 0 0] [1 0 0 0] [1 0 0 0] [0] 48.37/29.21 [0 1 0 0] [0 1 0 0] [0 1 1 0] [1] 48.37/29.21 [f](x0, x1, x2) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0 0 0 0]x2 + [0] 48.37/29.21 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0], 48.37/29.21 48.37/29.21 [0] 48.37/29.21 [0] 48.37/29.21 [b] = [0] 48.37/29.21 [0], 48.37/29.21 48.37/29.21 [0] 48.37/29.21 [0] 48.37/29.21 [a__b] = [1] 48.37/29.21 [0], 48.37/29.21 48.37/29.21 [1 0 0 0] [1 0 0 1] [1 0 0 0] [0] 48.37/29.21 [0 1 0 0] [0 1 0 1] [0 1 1 0] [1] 48.37/29.21 [a__f](x0, x1, x2) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0 0 0 0]x2 + [0] 48.37/29.22 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0], 48.37/29.22 48.37/29.22 [0] 48.37/29.22 [0] 48.37/29.22 [a] = [0] 48.37/29.22 [0] 48.37/29.22 orientation: 48.37/29.22 [1 1 0 0] [1 1 0 0] [1 1 1 0] [2] [1 0 0 0] [1 1 0 0] [1 0 0 0] [1] 48.37/29.22 [0 1 0 0] [0 1 0 0] [0 1 1 0] [1] [0 1 0 0] [0 1 0 0] [0 1 1 0] [1] 48.37/29.22 mark(f(X1,X2,X3)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 + [1] >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 + [0] = a__f(X1,mark(X2),X3) 48.37/29.22 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] 48.37/29.22 48.37/29.22 [2 0 0 1] [0] [1 0 0 0] [0] 48.37/29.22 [0 2 1 1] [1] [0 1 0 0] [1] 48.37/29.22 a__f(a(),X,X) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = a__f(X,a__b(),b()) 48.37/29.22 [0 0 0 0] [0] [0 0 0 0] [0] 48.37/29.22 48.37/29.22 [1] [0] 48.37/29.22 [0] [0] 48.37/29.22 mark(b()) = [1] >= [1] = a__b() 48.37/29.22 [0] [0] 48.37/29.22 48.37/29.22 [0] [0] 48.37/29.22 [0] [0] 48.37/29.22 a__b() = [1] >= [0] = a() 48.37/29.22 [0] [0] 48.37/29.22 48.37/29.22 [1] [0] 48.37/29.22 [0] [0] 48.37/29.22 mark(a()) = [1] >= [0] = a() 48.37/29.22 [0] [0] 48.37/29.22 48.37/29.22 [1 0 0 0] [1 0 0 1] [1 0 0 0] [0] [1 0 0 0] [1 0 0 0] [1 0 0 0] [0] 48.37/29.22 [0 1 0 0] [0 1 0 1] [0 1 1 0] [1] [0 1 0 0] [0 1 0 0] [0 1 1 0] [1] 48.37/29.22 a__f(X1,X2,X3) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 + [0] >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 + [0] = f(X1,X2,X3) 48.37/29.22 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] 48.37/29.22 48.37/29.22 [0] [0] 48.37/29.22 [0] [0] 48.37/29.22 a__b() = [1] >= [0] = b() 48.37/29.22 [0] [0] 48.37/29.22 problem: 48.37/29.22 strict: 48.37/29.22 48.37/29.22 weak: 48.37/29.22 mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) 48.37/29.22 a__f(a(),X,X) -> a__f(X,a__b(),b()) 48.37/29.22 mark(b()) -> a__b() 48.37/29.22 a__b() -> a() 48.37/29.22 mark(a()) -> a() 48.37/29.22 a__f(X1,X2,X3) -> f(X1,X2,X3) 48.37/29.22 a__b() -> b() 48.37/29.22 Qed 48.37/29.22 EOF