YES(?,O(n^2)) 56.04/31.02 YES(?,O(n^2)) 56.04/31.03 56.04/31.03 Problem: 56.04/31.03 a__f(a(),X,X) -> a__f(X,a__b(),b()) 56.04/31.03 a__b() -> a() 56.04/31.03 mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) 56.04/31.03 mark(b()) -> a__b() 56.04/31.03 mark(a()) -> a() 56.04/31.03 a__f(X1,X2,X3) -> f(X1,X2,X3) 56.04/31.03 a__b() -> b() 56.04/31.03 56.04/31.03 Proof: 56.04/31.03 Complexity Transformation Processor: 56.04/31.03 strict: 56.04/31.03 a__f(a(),X,X) -> a__f(X,a__b(),b()) 56.04/31.03 a__b() -> a() 56.04/31.03 mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) 56.04/31.03 mark(b()) -> a__b() 56.04/31.03 mark(a()) -> a() 56.04/31.03 a__f(X1,X2,X3) -> f(X1,X2,X3) 56.04/31.03 a__b() -> b() 56.04/31.03 weak: 56.04/31.03 56.04/31.03 Matrix Interpretation Processor: dim=1 56.04/31.03 56.04/31.03 max_matrix: 56.04/31.03 1 56.04/31.03 interpretation: 56.04/31.03 [mark](x0) = x0 + 240, 56.04/31.03 56.04/31.03 [f](x0, x1, x2) = x0 + x1 + x2 + 64, 56.04/31.03 56.04/31.03 [b] = 24, 56.04/31.03 56.04/31.03 [a__b] = 191, 56.04/31.03 56.04/31.03 [a__f](x0, x1, x2) = x0 + x1 + x2 + 84, 56.04/31.03 56.04/31.03 [a] = 192 56.04/31.03 orientation: 56.04/31.03 a__f(a(),X,X) = 2X + 276 >= X + 299 = a__f(X,a__b(),b()) 56.04/31.03 56.04/31.03 a__b() = 191 >= 192 = a() 56.04/31.03 56.04/31.03 mark(f(X1,X2,X3)) = X1 + X2 + X3 + 304 >= X1 + X2 + X3 + 324 = a__f(X1,mark(X2),X3) 56.04/31.03 56.04/31.03 mark(b()) = 264 >= 191 = a__b() 56.04/31.03 56.04/31.03 mark(a()) = 432 >= 192 = a() 56.04/31.03 56.04/31.03 a__f(X1,X2,X3) = X1 + X2 + X3 + 84 >= X1 + X2 + X3 + 64 = f(X1,X2,X3) 56.04/31.03 56.04/31.03 a__b() = 191 >= 24 = b() 56.04/31.03 problem: 56.04/31.03 strict: 56.04/31.03 a__f(a(),X,X) -> a__f(X,a__b(),b()) 56.04/31.03 a__b() -> a() 56.04/31.03 mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) 56.04/31.03 weak: 56.04/31.03 mark(b()) -> a__b() 56.04/31.03 mark(a()) -> a() 56.04/31.03 a__f(X1,X2,X3) -> f(X1,X2,X3) 56.04/31.03 a__b() -> b() 56.04/31.03 Matrix Interpretation Processor: dim=1 56.04/31.03 56.04/31.03 max_matrix: 56.04/31.03 1 56.04/31.03 interpretation: 56.04/31.03 [mark](x0) = x0, 56.04/31.03 56.04/31.03 [f](x0, x1, x2) = x0 + x1 + x2 + 1, 56.04/31.03 56.04/31.03 [b] = 0, 56.04/31.03 56.04/31.03 [a__b] = 0, 56.04/31.03 56.04/31.03 [a__f](x0, x1, x2) = x0 + x1 + x2 + 113, 56.04/31.03 56.04/31.03 [a] = 8 56.04/31.03 orientation: 56.04/31.03 a__f(a(),X,X) = 2X + 121 >= X + 113 = a__f(X,a__b(),b()) 56.04/31.03 56.04/31.03 a__b() = 0 >= 8 = a() 56.04/31.03 56.04/31.03 mark(f(X1,X2,X3)) = X1 + X2 + X3 + 1 >= X1 + X2 + X3 + 113 = a__f(X1,mark(X2),X3) 56.04/31.03 56.04/31.03 mark(b()) = 0 >= 0 = a__b() 56.04/31.03 56.04/31.03 mark(a()) = 8 >= 8 = a() 56.04/31.03 56.04/31.03 a__f(X1,X2,X3) = X1 + X2 + X3 + 113 >= X1 + X2 + X3 + 1 = f(X1,X2,X3) 56.04/31.03 56.04/31.03 a__b() = 0 >= 0 = b() 56.04/31.03 problem: 56.04/31.03 strict: 56.04/31.03 a__b() -> a() 56.04/31.03 mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) 56.04/31.03 weak: 56.04/31.03 a__f(a(),X,X) -> a__f(X,a__b(),b()) 56.04/31.03 mark(b()) -> a__b() 56.04/31.03 mark(a()) -> a() 56.04/31.03 a__f(X1,X2,X3) -> f(X1,X2,X3) 56.04/31.03 a__b() -> b() 56.04/31.03 Matrix Interpretation Processor: dim=4 56.04/31.03 56.04/31.03 max_matrix: 56.04/31.03 [1 1 1 0] 56.04/31.03 [0 0 0 0] 56.04/31.03 [0 0 0 1] 56.04/31.03 [0 0 0 0] 56.04/31.03 interpretation: 56.04/31.03 [1 0 0 0] [0] 56.04/31.03 [0 0 0 0] [1] 56.04/31.03 [mark](x0) = [0 0 0 1]x0 + [0] 56.04/31.03 [0 0 0 0] [1], 56.04/31.03 56.04/31.03 [1 1 1 0] [1 0 0 0] [1 1 1 0] [1] 56.04/31.03 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] 56.04/31.03 [f](x0, x1, x2) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0 0 0 0]x2 + [0] 56.04/31.03 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0], 56.04/31.03 56.04/31.03 [1] 56.04/31.03 [0] 56.04/31.03 [b] = [0] 56.04/31.03 [1], 56.04/31.03 56.04/31.03 [1] 56.04/31.03 [1] 56.04/31.03 [a__b] = [1] 56.04/31.03 [1], 56.04/31.03 56.04/31.03 [1 1 1 0] [1 0 0 0] [1 1 1 0] [1] 56.04/31.03 [0 0 0 0] [0 0 0 0] [0 0 0 0] [1] 56.04/31.03 [a__f](x0, x1, x2) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0 0 0 0]x2 + [0] 56.04/31.03 [0 0 0 0] [0 0 0 0] [0 0 0 0] [1], 56.04/31.03 56.04/31.03 [0] 56.04/31.03 [1] 56.04/31.03 [a] = [1] 56.04/31.03 [1] 56.04/31.03 orientation: 56.04/31.03 [1] [0] 56.04/31.03 [1] [1] 56.04/31.03 a__b() = [1] >= [1] = a() 56.04/31.03 [1] [1] 56.04/31.03 56.04/31.03 [1 1 1 0] [1 0 0 0] [1 1 1 0] [1] [1 1 1 0] [1 0 0 0] [1 1 1 0] [1] 56.04/31.03 [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] [1] 56.04/31.03 mark(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] = a__f(X1,mark(X2),X3) 56.04/31.03 [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] [1] 56.04/31.04 56.04/31.04 [2 1 1 0] [3] [1 1 1 0] [3] 56.04/31.04 [0 0 0 0] [1] [0 0 0 0] [1] 56.04/31.04 a__f(a(),X,X) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = a__f(X,a__b(),b()) 56.04/31.04 [0 0 0 0] [1] [0 0 0 0] [1] 56.04/31.04 56.04/31.04 [1] [1] 56.04/31.04 [1] [1] 56.04/31.04 mark(b()) = [1] >= [1] = a__b() 56.04/31.04 [1] [1] 56.04/31.04 56.04/31.04 [0] [0] 56.04/31.04 [1] [1] 56.04/31.04 mark(a()) = [1] >= [1] = a() 56.04/31.04 [1] [1] 56.04/31.04 56.04/31.04 [1 1 1 0] [1 0 0 0] [1 1 1 0] [1] [1 1 1 0] [1 0 0 0] [1 1 1 0] [1] 56.04/31.04 [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] 56.04/31.04 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) 56.04/31.04 [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] 56.04/31.04 56.04/31.04 [1] [1] 56.04/31.04 [1] [0] 56.04/31.04 a__b() = [1] >= [0] = b() 56.04/31.04 [1] [1] 56.04/31.04 problem: 56.04/31.04 strict: 56.04/31.04 mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) 56.04/31.04 weak: 56.04/31.04 a__b() -> a() 56.04/31.04 a__f(a(),X,X) -> a__f(X,a__b(),b()) 56.04/31.04 mark(b()) -> a__b() 56.04/31.04 mark(a()) -> a() 56.04/31.04 a__f(X1,X2,X3) -> f(X1,X2,X3) 56.04/31.04 a__b() -> b() 56.04/31.04 Matrix Interpretation Processor: dim=4 56.04/31.04 56.04/31.04 max_matrix: 56.04/31.04 [1 0 1 1] 56.04/31.04 [0 0 0 0] 56.04/31.04 [0 0 0 1] 56.04/31.04 [0 0 0 1] 56.04/31.04 interpretation: 56.04/31.04 [1 0 1 0] [1] 56.04/31.04 [0 0 0 0] [1] 56.04/31.04 [mark](x0) = [0 0 0 1]x0 + [0] 56.04/31.04 [0 0 0 1] [0], 56.04/31.04 56.04/31.04 [1 0 0 1] [1 0 1 0] [1 0 0 1] [1] 56.04/31.04 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] 56.04/31.04 [f](x0, x1, x2) = [0 0 0 1]x0 + [0 0 0 1]x1 + [0 0 0 0]x2 + [1] 56.04/31.04 [0 0 0 1] [0 0 0 1] [0 0 0 0] [1], 56.04/31.04 56.04/31.04 [0] 56.04/31.04 [0] 56.04/31.04 [b] = [0] 56.04/31.04 [1], 56.04/31.04 56.04/31.04 [0] 56.04/31.04 [0] 56.04/31.04 [a__b] = [0] 56.04/31.04 [1], 56.04/31.04 56.04/31.04 [1 0 0 1] [1 0 1 0] [1 0 0 1] [1] 56.04/31.04 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] 56.04/31.04 [a__f](x0, x1, x2) = [0 0 0 1]x0 + [0 0 0 1]x1 + [0 0 0 0]x2 + [1] 56.04/31.04 [0 0 0 1] [0 0 0 1] [0 0 0 0] [1], 56.04/31.04 56.04/31.04 [0] 56.04/31.04 [0] 56.04/31.04 [a] = [0] 56.04/31.04 [1] 56.04/31.04 orientation: 56.04/31.04 [1 0 0 2] [1 0 1 1] [1 0 0 1] [3] [1 0 0 1] [1 0 1 1] [1 0 0 1] [2] 56.04/31.04 [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] 56.04/31.04 mark(f(X1,X2,X3)) = [0 0 0 1]X1 + [0 0 0 1]X2 + [0 0 0 0]X3 + [1] >= [0 0 0 1]X1 + [0 0 0 1]X2 + [0 0 0 0]X3 + [1] = a__f(X1,mark(X2),X3) 56.04/31.04 [0 0 0 1] [0 0 0 1] [0 0 0 0] [1] [0 0 0 1] [0 0 0 1] [0 0 0 0] [1] 56.04/31.04 56.04/31.04 [0] [0] 56.04/31.04 [0] [0] 56.04/31.04 a__b() = [0] >= [0] = a() 56.04/31.04 [1] [1] 56.04/31.04 56.04/31.04 [2 0 1 1] [2] [1 0 0 1] [2] 56.04/31.04 [0 0 0 0] [0] [0 0 0 0] [0] 56.04/31.04 a__f(a(),X,X) = [0 0 0 1]X + [2] >= [0 0 0 1]X + [2] = a__f(X,a__b(),b()) 56.04/31.04 [0 0 0 1] [2] [0 0 0 1] [2] 56.04/31.04 56.04/31.04 [1] [0] 56.04/31.04 [1] [0] 56.04/31.04 mark(b()) = [1] >= [0] = a__b() 56.04/31.04 [1] [1] 56.04/31.04 56.04/31.04 [1] [0] 56.04/31.04 [1] [0] 56.04/31.04 mark(a()) = [1] >= [0] = a() 56.04/31.04 [1] [1] 56.04/31.04 56.04/31.04 [1 0 0 1] [1 0 1 0] [1 0 0 1] [1] [1 0 0 1] [1 0 1 0] [1 0 0 1] [1] 56.04/31.04 [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] 56.04/31.04 a__f(X1,X2,X3) = [0 0 0 1]X1 + [0 0 0 1]X2 + [0 0 0 0]X3 + [1] >= [0 0 0 1]X1 + [0 0 0 1]X2 + [0 0 0 0]X3 + [1] = f(X1,X2,X3) 56.04/31.04 [0 0 0 1] [0 0 0 1] [0 0 0 0] [1] [0 0 0 1] [0 0 0 1] [0 0 0 0] [1] 56.04/31.04 56.04/31.04 [0] [0] 56.04/31.04 [0] [0] 56.04/31.04 a__b() = [0] >= [0] = b() 56.04/31.04 [1] [1] 56.04/31.04 problem: 56.04/31.04 strict: 56.04/31.04 56.04/31.04 weak: 56.04/31.04 mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3) 56.04/31.04 a__b() -> a() 56.04/31.04 a__f(a(),X,X) -> a__f(X,a__b(),b()) 56.04/31.04 mark(b()) -> a__b() 56.04/31.04 mark(a()) -> a() 56.04/31.04 a__f(X1,X2,X3) -> f(X1,X2,X3) 56.04/31.04 a__b() -> b() 56.04/31.04 Qed 56.04/31.04 EOF