YES(?,O(n^2)) 67.36/30.07 YES(?,O(n^2)) 67.36/30.08 67.36/30.08 Problem: 67.36/30.08 a__f(f(a())) -> c(f(g(f(a())))) 67.36/30.08 mark(f(X)) -> a__f(mark(X)) 67.36/30.08 mark(a()) -> a() 67.36/30.08 mark(c(X)) -> c(X) 67.36/30.08 mark(g(X)) -> g(mark(X)) 67.36/30.08 a__f(X) -> f(X) 67.36/30.08 67.36/30.08 Proof: 67.36/30.08 Complexity Transformation Processor: 67.36/30.08 strict: 67.36/30.08 a__f(f(a())) -> c(f(g(f(a())))) 67.36/30.08 mark(f(X)) -> a__f(mark(X)) 67.36/30.08 mark(a()) -> a() 67.36/30.08 mark(c(X)) -> c(X) 67.36/30.08 mark(g(X)) -> g(mark(X)) 67.36/30.08 a__f(X) -> f(X) 67.36/30.08 weak: 67.36/30.08 67.36/30.08 Matrix Interpretation Processor: dim=1 67.36/30.08 67.36/30.08 max_matrix: 67.36/30.08 1 67.36/30.08 interpretation: 67.36/30.08 [mark](x0) = x0 + 138, 67.36/30.08 67.36/30.08 [c](x0) = x0 + 30, 67.36/30.08 67.36/30.08 [g](x0) = x0 + 32, 67.36/30.08 67.36/30.08 [a__f](x0) = x0 + 63, 67.36/30.08 67.36/30.08 [f](x0) = x0 + 8, 67.36/30.08 67.36/30.08 [a] = 184 67.36/30.08 orientation: 67.36/30.08 a__f(f(a())) = 255 >= 262 = c(f(g(f(a())))) 67.36/30.08 67.36/30.08 mark(f(X)) = X + 146 >= X + 201 = a__f(mark(X)) 67.36/30.08 67.36/30.08 mark(a()) = 322 >= 184 = a() 67.36/30.08 67.36/30.08 mark(c(X)) = X + 168 >= X + 30 = c(X) 67.36/30.08 67.36/30.08 mark(g(X)) = X + 170 >= X + 170 = g(mark(X)) 67.36/30.08 67.36/30.08 a__f(X) = X + 63 >= X + 8 = f(X) 67.36/30.08 problem: 67.36/30.08 strict: 67.36/30.08 a__f(f(a())) -> c(f(g(f(a())))) 67.36/30.08 mark(f(X)) -> a__f(mark(X)) 67.36/30.08 mark(g(X)) -> g(mark(X)) 67.36/30.08 weak: 67.36/30.08 mark(a()) -> a() 67.36/30.08 mark(c(X)) -> c(X) 67.36/30.08 a__f(X) -> f(X) 67.36/30.08 Matrix Interpretation Processor: dim=1 67.36/30.08 67.36/30.08 max_matrix: 67.36/30.08 1 67.36/30.08 interpretation: 67.36/30.08 [mark](x0) = x0, 67.36/30.08 67.36/30.08 [c](x0) = x0 + 8, 67.36/30.08 67.36/30.08 [g](x0) = x0 + 8, 67.36/30.08 67.36/30.08 [a__f](x0) = x0 + 17, 67.36/30.08 67.36/30.08 [f](x0) = x0, 67.36/30.08 67.36/30.08 [a] = 0 67.36/30.08 orientation: 67.36/30.08 a__f(f(a())) = 17 >= 16 = c(f(g(f(a())))) 67.36/30.08 67.36/30.08 mark(f(X)) = X >= X + 17 = a__f(mark(X)) 67.36/30.08 67.36/30.08 mark(g(X)) = X + 8 >= X + 8 = g(mark(X)) 67.36/30.08 67.36/30.08 mark(a()) = 0 >= 0 = a() 67.36/30.08 67.36/30.08 mark(c(X)) = X + 8 >= X + 8 = c(X) 67.36/30.08 67.36/30.08 a__f(X) = X + 17 >= X = f(X) 67.36/30.08 problem: 67.36/30.08 strict: 67.36/30.08 mark(f(X)) -> a__f(mark(X)) 67.36/30.08 mark(g(X)) -> g(mark(X)) 67.36/30.08 weak: 67.36/30.08 a__f(f(a())) -> c(f(g(f(a())))) 67.36/30.08 mark(a()) -> a() 67.36/30.08 mark(c(X)) -> c(X) 67.36/30.08 a__f(X) -> f(X) 67.36/30.08 Matrix Interpretation Processor: dim=2 67.36/30.08 67.36/30.08 max_matrix: 67.36/30.08 [1 2] 67.36/30.08 [0 1] 67.36/30.08 interpretation: 67.36/30.08 [1 2] 67.36/30.08 [mark](x0) = [0 1]x0, 67.36/30.08 67.36/30.08 [1 0] 67.36/30.08 [c](x0) = [0 0]x0, 67.36/30.08 67.36/30.08 67.36/30.08 [g](x0) = x0, 67.36/30.08 67.36/30.08 [1] 67.36/30.08 [a__f](x0) = x0 + [4], 67.36/30.08 67.36/30.08 [1] 67.36/30.08 [f](x0) = x0 + [4], 67.36/30.08 67.36/30.08 [7] 67.36/30.08 [a] = [4] 67.36/30.08 orientation: 67.36/30.08 [1 2] [9] [1 2] [1] 67.36/30.08 mark(f(X)) = [0 1]X + [4] >= [0 1]X + [4] = a__f(mark(X)) 67.36/30.08 67.36/30.08 [1 2] [1 2] 67.36/30.08 mark(g(X)) = [0 1]X >= [0 1]X = g(mark(X)) 67.36/30.08 67.36/30.08 [9 ] [9] 67.36/30.08 a__f(f(a())) = [12] >= [0] = c(f(g(f(a())))) 67.36/30.08 67.36/30.08 [15] [7] 67.36/30.08 mark(a()) = [4 ] >= [4] = a() 67.36/30.08 67.36/30.08 [1 0] [1 0] 67.36/30.08 mark(c(X)) = [0 0]X >= [0 0]X = c(X) 67.36/30.08 67.36/30.08 [1] [1] 67.36/30.08 a__f(X) = X + [4] >= X + [4] = f(X) 67.36/30.08 problem: 67.36/30.08 strict: 67.36/30.08 mark(g(X)) -> g(mark(X)) 67.36/30.08 weak: 67.36/30.08 mark(f(X)) -> a__f(mark(X)) 67.36/30.08 a__f(f(a())) -> c(f(g(f(a())))) 67.36/30.08 mark(a()) -> a() 67.36/30.08 mark(c(X)) -> c(X) 67.36/30.08 a__f(X) -> f(X) 67.36/30.08 Matrix Interpretation Processor: dim=4 67.36/30.08 67.36/30.08 max_matrix: 67.36/30.08 [1 1 1 1] 67.36/30.08 [0 1 1 0] 67.36/30.08 [0 0 0 0] 67.36/30.08 [0 0 0 0] 67.36/30.08 interpretation: 67.36/30.08 [1 1 1 0] [0] 67.36/30.08 [0 1 1 0] [0] 67.36/30.08 [mark](x0) = [0 0 0 0]x0 + [1] 67.36/30.08 [0 0 0 0] [1], 67.36/30.08 67.36/30.08 [1 0 0 0] [0] 67.36/30.08 [0 0 0 0] [0] 67.36/30.08 [c](x0) = [0 0 0 0]x0 + [1] 67.36/30.08 [0 0 0 0] [0], 67.36/30.08 67.36/30.08 [1 0 0 0] [1] 67.36/30.08 [0 1 1 0] [0] 67.36/30.08 [g](x0) = [0 0 0 0]x0 + [1] 67.36/30.08 [0 0 0 0] [0], 67.36/30.08 67.36/30.08 [1 0 0 1] [0] 67.36/30.08 [0 1 1 0] [0] 67.36/30.08 [a__f](x0) = [0 0 0 0]x0 + [1] 67.36/30.08 [0 0 0 0] [1], 67.36/30.08 67.36/30.08 [1 0 0 1] [0] 67.36/30.08 [0 1 1 0] [0] 67.36/30.08 [f](x0) = [0 0 0 0]x0 + [1] 67.36/30.08 [0 0 0 0] [1], 67.36/30.08 67.36/30.08 [1] 67.36/30.08 [0] 67.36/30.08 [a] = [0] 67.36/30.08 [0] 67.36/30.08 orientation: 67.36/30.08 [1 1 1 0] [2] [1 1 1 0] [1] 67.36/30.08 [0 1 1 0] [1] [0 1 1 0] [1] 67.36/30.08 mark(g(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = g(mark(X)) 67.36/30.08 [0 0 0 0] [1] [0 0 0 0] [0] 67.36/30.08 67.36/30.08 [1 1 1 1] [1] [1 1 1 0] [1] 67.36/30.08 [0 1 1 0] [1] [0 1 1 0] [1] 67.36/30.08 mark(f(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = a__f(mark(X)) 67.36/30.08 [0 0 0 0] [1] [0 0 0 0] [1] 67.36/30.08 67.36/30.08 [2] [2] 67.36/30.08 [1] [0] 67.36/30.08 a__f(f(a())) = [1] >= [1] = c(f(g(f(a())))) 67.36/30.08 [1] [0] 67.36/30.08 67.36/30.08 [1] [1] 67.36/30.08 [0] [0] 67.36/30.08 mark(a()) = [1] >= [0] = a() 67.36/30.08 [1] [0] 67.36/30.08 67.36/30.08 [1 0 0 0] [1] [1 0 0 0] [0] 67.36/30.08 [0 0 0 0] [1] [0 0 0 0] [0] 67.36/30.08 mark(c(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = c(X) 67.36/30.08 [0 0 0 0] [1] [0 0 0 0] [0] 67.36/30.08 67.36/30.08 [1 0 0 1] [0] [1 0 0 1] [0] 67.36/30.08 [0 1 1 0] [0] [0 1 1 0] [0] 67.36/30.08 a__f(X) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = f(X) 67.36/30.08 [0 0 0 0] [1] [0 0 0 0] [1] 67.36/30.08 problem: 67.36/30.08 strict: 67.36/30.08 67.36/30.08 weak: 67.36/30.08 mark(g(X)) -> g(mark(X)) 67.36/30.08 mark(f(X)) -> a__f(mark(X)) 67.36/30.08 a__f(f(a())) -> c(f(g(f(a())))) 67.36/30.08 mark(a()) -> a() 67.36/30.08 mark(c(X)) -> c(X) 67.36/30.08 a__f(X) -> f(X) 67.36/30.08 Qed 67.36/30.08 EOF