YES(?,O(n^2)) 523.97/295.21 YES(?,O(n^2)) 523.97/295.22 523.97/295.22 Problem: 523.97/295.22 active(f(f(a()))) -> mark(f(g(f(a())))) 523.97/295.22 mark(f(X)) -> active(f(mark(X))) 523.97/295.22 mark(a()) -> active(a()) 523.97/295.22 mark(g(X)) -> active(g(X)) 523.97/295.22 f(mark(X)) -> f(X) 523.97/295.22 f(active(X)) -> f(X) 523.97/295.22 g(mark(X)) -> g(X) 523.97/295.22 g(active(X)) -> g(X) 523.97/295.22 523.97/295.22 Proof: 523.97/295.22 Complexity Transformation Processor: 523.97/295.22 strict: 523.97/295.22 active(f(f(a()))) -> mark(f(g(f(a())))) 523.97/295.22 mark(f(X)) -> active(f(mark(X))) 523.97/295.22 mark(a()) -> active(a()) 523.97/295.22 mark(g(X)) -> active(g(X)) 523.97/295.22 f(mark(X)) -> f(X) 523.97/295.22 f(active(X)) -> f(X) 523.97/295.22 g(mark(X)) -> g(X) 523.97/295.22 g(active(X)) -> g(X) 523.97/295.22 weak: 523.97/295.22 523.97/295.22 Matrix Interpretation Processor: dim=1 523.97/295.22 523.97/295.22 max_matrix: 523.97/295.22 1 523.97/295.22 interpretation: 523.97/295.22 [mark](x0) = x0 + 1, 523.97/295.22 523.97/295.22 [g](x0) = x0 + 12, 523.97/295.22 523.97/295.22 [active](x0) = x0 + 1, 523.97/295.22 523.97/295.22 [f](x0) = x0 + 3, 523.97/295.22 523.97/295.22 [a] = 2 523.97/295.22 orientation: 523.97/295.22 active(f(f(a()))) = 9 >= 21 = mark(f(g(f(a())))) 523.97/295.22 523.97/295.22 mark(f(X)) = X + 4 >= X + 5 = active(f(mark(X))) 523.97/295.22 523.97/295.22 mark(a()) = 3 >= 3 = active(a()) 523.97/295.22 523.97/295.22 mark(g(X)) = X + 13 >= X + 13 = active(g(X)) 523.97/295.22 523.97/295.22 f(mark(X)) = X + 4 >= X + 3 = f(X) 523.97/295.22 523.97/295.22 f(active(X)) = X + 4 >= X + 3 = f(X) 523.97/295.22 523.97/295.22 g(mark(X)) = X + 13 >= X + 12 = g(X) 523.97/295.22 523.97/295.22 g(active(X)) = X + 13 >= X + 12 = g(X) 523.97/295.22 problem: 523.97/295.22 strict: 523.97/295.22 active(f(f(a()))) -> mark(f(g(f(a())))) 523.97/295.22 mark(f(X)) -> active(f(mark(X))) 523.97/295.22 mark(a()) -> active(a()) 523.97/295.22 mark(g(X)) -> active(g(X)) 523.97/295.22 weak: 523.97/295.22 f(mark(X)) -> f(X) 523.97/295.22 f(active(X)) -> f(X) 523.97/295.22 g(mark(X)) -> g(X) 523.97/295.22 g(active(X)) -> g(X) 523.97/295.22 Matrix Interpretation Processor: dim=1 523.97/295.22 523.97/295.22 max_matrix: 523.97/295.22 1 523.97/295.22 interpretation: 523.97/295.22 [mark](x0) = x0 + 2, 523.97/295.22 523.97/295.22 [g](x0) = x0 + 2, 523.97/295.22 523.97/295.22 [active](x0) = x0 + 1, 523.97/295.22 523.97/295.22 [f](x0) = x0 + 38, 523.97/295.22 523.97/295.22 [a] = 50 523.97/295.22 orientation: 523.97/295.22 active(f(f(a()))) = 127 >= 130 = mark(f(g(f(a())))) 523.97/295.22 523.97/295.22 mark(f(X)) = X + 40 >= X + 41 = active(f(mark(X))) 523.97/295.22 523.97/295.22 mark(a()) = 52 >= 51 = active(a()) 523.97/295.22 523.97/295.22 mark(g(X)) = X + 4 >= X + 3 = active(g(X)) 523.97/295.22 523.97/295.22 f(mark(X)) = X + 40 >= X + 38 = f(X) 523.97/295.22 523.97/295.22 f(active(X)) = X + 39 >= X + 38 = f(X) 523.97/295.22 523.97/295.22 g(mark(X)) = X + 4 >= X + 2 = g(X) 523.97/295.22 523.97/295.22 g(active(X)) = X + 3 >= X + 2 = g(X) 523.97/295.22 problem: 523.97/295.22 strict: 523.97/295.22 active(f(f(a()))) -> mark(f(g(f(a())))) 523.97/295.22 mark(f(X)) -> active(f(mark(X))) 523.97/295.22 weak: 523.97/295.22 mark(a()) -> active(a()) 523.97/295.22 mark(g(X)) -> active(g(X)) 523.97/295.22 f(mark(X)) -> f(X) 523.97/295.22 f(active(X)) -> f(X) 523.97/295.22 g(mark(X)) -> g(X) 523.97/295.22 g(active(X)) -> g(X) 523.97/295.22 Splitting Processor: 523.97/295.22 strict: 523.97/295.22 active(f(f(a()))) -> mark(f(g(f(a())))) 523.97/295.22 weak: 523.97/295.22 mark(a()) -> active(a()) 523.97/295.22 mark(g(X)) -> active(g(X)) 523.97/295.22 f(mark(X)) -> f(X) 523.97/295.22 f(active(X)) -> f(X) 523.97/295.22 g(mark(X)) -> g(X) 523.97/295.22 g(active(X)) -> g(X) 523.97/295.22 mark(f(X)) -> active(f(mark(X))) 523.97/295.22 Matrix Interpretation Processor: dim=5 523.97/295.22 523.97/295.22 max_matrix: 523.97/295.22 [1 0 1 0 1] 523.97/295.22 [0 0 0 1 0] 523.97/295.22 [0 0 0 0 1] 523.97/295.22 [0 0 0 0 0] 523.97/295.22 [0 0 0 0 0] 523.97/295.22 interpretation: 523.97/295.22 [1 0 1 0 0] 523.97/295.22 [0 0 0 1 0] 523.97/295.22 [mark](x0) = [0 0 0 0 1]x0 523.97/295.22 [0 0 0 0 0] 523.97/295.22 [0 0 0 0 0] , 523.97/295.22 523.97/295.22 [1 0 1 0 0] [0] 523.97/295.22 [0 0 0 0 0] [0] 523.97/295.22 [g](x0) = [0 0 0 0 0]x0 + [0] 523.97/295.22 [0 0 0 0 0] [1] 523.97/295.22 [0 0 0 0 0] [0], 523.97/295.22 523.97/295.22 [1 0 1 0 0] 523.97/295.22 [0 0 0 0 0] 523.97/295.22 [active](x0) = [0 0 0 0 1]x0 523.97/295.22 [0 0 0 0 0] 523.97/295.22 [0 0 0 0 0] , 523.97/295.22 523.97/295.22 [1 0 1 0 1] [0] 523.97/295.22 [0 0 0 0 0] [0] 523.97/295.22 [f](x0) = [0 0 0 0 0]x0 + [0] 523.97/295.22 [0 0 0 0 0] [0] 523.97/295.22 [0 0 0 0 0] [1], 523.97/295.22 523.97/295.22 [0] 523.97/295.22 [0] 523.97/295.22 [a] = [0] 523.97/295.22 [0] 523.97/295.22 [0] 523.97/295.22 orientation: 523.97/295.22 [1] [0] 523.97/295.22 [0] [0] 523.97/295.22 active(f(f(a()))) = [1] >= [1] = mark(f(g(f(a())))) 523.97/295.22 [0] [0] 523.97/295.22 [0] [0] 523.97/295.22 523.97/295.22 [0] [0] 523.97/295.22 [0] [0] 523.97/295.22 mark(a()) = [0] >= [0] = active(a()) 523.97/295.22 [0] [0] 523.97/295.22 [0] [0] 523.97/295.22 523.97/295.22 [1 0 1 0 0] [0] [1 0 1 0 0] 523.97/295.22 [0 0 0 0 0] [1] [0 0 0 0 0] 523.97/295.22 mark(g(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X = active(g(X)) 523.97/295.22 [0 0 0 0 0] [0] [0 0 0 0 0] 523.97/295.22 [0 0 0 0 0] [0] [0 0 0 0 0] 523.97/295.22 523.97/295.22 [1 0 1 0 1] [0] [1 0 1 0 1] [0] 523.97/295.22 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 523.97/295.22 f(mark(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = f(X) 523.97/295.22 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 523.97/295.22 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 523.97/295.22 523.97/295.22 [1 0 1 0 1] [0] [1 0 1 0 1] [0] 523.97/295.22 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 523.97/295.22 f(active(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = f(X) 523.97/295.22 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 523.97/295.22 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 523.97/295.22 523.97/295.22 [1 0 1 0 1] [0] [1 0 1 0 0] [0] 523.97/295.22 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 523.97/295.22 g(mark(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = g(X) 523.97/295.22 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 523.97/295.22 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 523.97/295.22 523.97/295.22 [1 0 1 0 1] [0] [1 0 1 0 0] [0] 523.97/295.22 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 523.97/295.22 g(active(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = g(X) 523.97/295.22 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 523.97/295.22 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 523.97/295.22 523.97/295.22 [1 0 1 0 1] [0] [1 0 1 0 1] [0] 523.97/295.22 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 523.97/295.22 mark(f(X)) = [0 0 0 0 0]X + [1] >= [0 0 0 0 0]X + [1] = active(f(mark(X))) 523.97/295.22 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 523.97/295.22 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 523.97/295.22 problem: 523.97/295.22 strict: 523.97/295.22 523.97/295.22 weak: 523.97/295.22 active(f(f(a()))) -> mark(f(g(f(a())))) 523.97/295.22 mark(a()) -> active(a()) 523.97/295.22 mark(g(X)) -> active(g(X)) 523.97/295.22 f(mark(X)) -> f(X) 523.97/295.22 f(active(X)) -> f(X) 523.97/295.22 g(mark(X)) -> g(X) 523.97/295.22 g(active(X)) -> g(X) 523.97/295.22 mark(f(X)) -> active(f(mark(X))) 523.97/295.22 Qed 523.97/295.22 523.97/295.22 strict: 523.97/295.22 mark(f(X)) -> active(f(mark(X))) 523.97/295.22 weak: 523.97/295.22 active(f(f(a()))) -> mark(f(g(f(a())))) 523.97/295.22 mark(a()) -> active(a()) 523.97/295.22 mark(g(X)) -> active(g(X)) 523.97/295.22 f(mark(X)) -> f(X) 523.97/295.22 f(active(X)) -> f(X) 523.97/295.22 g(mark(X)) -> g(X) 523.97/295.22 g(active(X)) -> g(X) 523.97/295.22 Matrix Interpretation Processor: dim=3 523.97/295.22 523.97/295.22 max_matrix: 523.97/295.22 [1 0 1] 523.97/295.22 [0 0 0] 523.97/295.22 [0 0 1] 523.97/295.22 interpretation: 523.97/295.22 [1 0 1] 523.97/295.22 [mark](x0) = [0 0 0]x0 523.97/295.22 [0 0 1] , 523.97/295.22 523.97/295.22 [1 0 0] [0] 523.97/295.22 [g](x0) = [0 0 0]x0 + [1] 523.97/295.22 [0 0 0] [0], 523.97/295.22 523.97/295.22 [1 0 0] 523.97/295.22 [active](x0) = [0 0 0]x0 523.97/295.22 [0 0 1] , 523.97/295.22 523.97/295.22 [1 0 1] [0] 523.97/295.22 [f](x0) = [0 0 0]x0 + [0] 523.97/295.22 [0 0 1] [1], 523.97/295.22 523.97/295.22 [0] 523.97/295.22 [a] = [0] 523.97/295.22 [0] 523.97/295.22 orientation: 523.97/295.22 [1 0 2] [1] [1 0 2] [0] 523.97/295.22 mark(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(f(mark(X))) 523.97/295.22 [0 0 1] [1] [0 0 1] [1] 523.97/295.22 523.97/295.22 [1] [1] 523.97/295.22 active(f(f(a()))) = [0] >= [0] = mark(f(g(f(a())))) 523.97/295.22 [2] [1] 523.97/295.22 523.97/295.22 [0] [0] 523.97/295.22 mark(a()) = [0] >= [0] = active(a()) 523.97/295.22 [0] [0] 523.97/295.23 523.97/295.23 [1 0 0] [1 0 0] 523.97/295.23 mark(g(X)) = [0 0 0]X >= [0 0 0]X = active(g(X)) 523.97/295.23 [0 0 0] [0 0 0] 523.97/295.23 523.97/295.23 [1 0 2] [0] [1 0 1] [0] 523.97/295.23 f(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(X) 523.97/295.23 [0 0 1] [1] [0 0 1] [1] 523.97/295.23 523.97/295.23 [1 0 1] [0] [1 0 1] [0] 523.97/295.23 f(active(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(X) 523.97/295.23 [0 0 1] [1] [0 0 1] [1] 523.97/295.23 523.97/295.23 [1 0 1] [0] [1 0 0] [0] 523.97/295.23 g(mark(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = g(X) 523.97/295.23 [0 0 0] [0] [0 0 0] [0] 523.97/295.23 523.97/295.23 [1 0 0] [0] [1 0 0] [0] 523.97/295.23 g(active(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = g(X) 523.97/295.23 [0 0 0] [0] [0 0 0] [0] 523.97/295.23 problem: 523.97/295.23 strict: 523.97/295.23 523.97/295.23 weak: 523.97/295.23 mark(f(X)) -> active(f(mark(X))) 523.97/295.23 active(f(f(a()))) -> mark(f(g(f(a())))) 523.97/295.23 mark(a()) -> active(a()) 523.97/295.23 mark(g(X)) -> active(g(X)) 523.97/295.23 f(mark(X)) -> f(X) 523.97/295.23 f(active(X)) -> f(X) 523.97/295.23 g(mark(X)) -> g(X) 523.97/295.23 g(active(X)) -> g(X) 523.97/295.23 Qed 523.97/295.23 EOF