YES(?,O(n^2)) 622.73/295.28 YES(?,O(n^2)) 622.73/295.29 622.73/295.29 Problem: 622.73/295.29 active(f(f(a()))) -> mark(f(g(f(a())))) 622.73/295.29 mark(f(X)) -> active(f(X)) 622.73/295.29 mark(a()) -> active(a()) 622.73/295.29 mark(g(X)) -> active(g(mark(X))) 622.73/295.29 f(mark(X)) -> f(X) 622.73/295.29 f(active(X)) -> f(X) 622.73/295.29 g(mark(X)) -> g(X) 622.73/295.29 g(active(X)) -> g(X) 622.73/295.29 622.73/295.29 Proof: 622.73/295.29 Complexity Transformation Processor: 622.73/295.29 strict: 622.73/295.29 active(f(f(a()))) -> mark(f(g(f(a())))) 622.73/295.29 mark(f(X)) -> active(f(X)) 622.73/295.29 mark(a()) -> active(a()) 622.73/295.29 mark(g(X)) -> active(g(mark(X))) 622.73/295.29 f(mark(X)) -> f(X) 622.73/295.29 f(active(X)) -> f(X) 622.73/295.29 g(mark(X)) -> g(X) 622.73/295.29 g(active(X)) -> g(X) 622.73/295.29 weak: 622.73/295.29 622.73/295.29 Matrix Interpretation Processor: dim=1 622.73/295.29 622.73/295.29 max_matrix: 622.73/295.29 1 622.73/295.29 interpretation: 622.73/295.29 [mark](x0) = x0 + 1, 622.73/295.29 622.73/295.29 [g](x0) = x0 + 8, 622.73/295.29 622.73/295.29 [active](x0) = x0 + 1, 622.73/295.29 622.73/295.29 [f](x0) = x0 + 7, 622.73/295.29 622.73/295.29 [a] = 2 622.73/295.29 orientation: 622.73/295.29 active(f(f(a()))) = 17 >= 25 = mark(f(g(f(a())))) 622.73/295.29 622.73/295.29 mark(f(X)) = X + 8 >= X + 8 = active(f(X)) 622.73/295.29 622.73/295.29 mark(a()) = 3 >= 3 = active(a()) 622.73/295.29 622.73/295.29 mark(g(X)) = X + 9 >= X + 10 = active(g(mark(X))) 622.73/295.29 622.73/295.29 f(mark(X)) = X + 8 >= X + 7 = f(X) 622.73/295.29 622.73/295.29 f(active(X)) = X + 8 >= X + 7 = f(X) 622.73/295.29 622.73/295.29 g(mark(X)) = X + 9 >= X + 8 = g(X) 622.73/295.29 622.73/295.29 g(active(X)) = X + 9 >= X + 8 = g(X) 622.73/295.29 problem: 622.73/295.29 strict: 622.73/295.29 active(f(f(a()))) -> mark(f(g(f(a())))) 622.73/295.29 mark(f(X)) -> active(f(X)) 622.73/295.29 mark(a()) -> active(a()) 622.73/295.29 mark(g(X)) -> active(g(mark(X))) 622.73/295.29 weak: 622.73/295.29 f(mark(X)) -> f(X) 622.73/295.29 f(active(X)) -> f(X) 622.73/295.29 g(mark(X)) -> g(X) 622.73/295.29 g(active(X)) -> g(X) 622.73/295.29 Matrix Interpretation Processor: dim=1 622.73/295.29 622.73/295.29 max_matrix: 622.73/295.29 1 622.73/295.29 interpretation: 622.73/295.29 [mark](x0) = x0 + 1, 622.73/295.29 622.73/295.29 [g](x0) = x0, 622.73/295.29 622.73/295.29 [active](x0) = x0, 622.73/295.29 622.73/295.29 [f](x0) = x0, 622.73/295.29 622.73/295.29 [a] = 11 622.73/295.29 orientation: 622.73/295.29 active(f(f(a()))) = 11 >= 12 = mark(f(g(f(a())))) 622.73/295.29 622.73/295.29 mark(f(X)) = X + 1 >= X = active(f(X)) 622.73/295.29 622.73/295.29 mark(a()) = 12 >= 11 = active(a()) 622.73/295.29 622.73/295.29 mark(g(X)) = X + 1 >= X + 1 = active(g(mark(X))) 622.73/295.29 622.73/295.29 f(mark(X)) = X + 1 >= X = f(X) 622.73/295.29 622.73/295.29 f(active(X)) = X >= X = f(X) 622.73/295.29 622.73/295.29 g(mark(X)) = X + 1 >= X = g(X) 622.73/295.29 622.73/295.29 g(active(X)) = X >= X = g(X) 622.73/295.29 problem: 622.73/295.29 strict: 622.73/295.29 active(f(f(a()))) -> mark(f(g(f(a())))) 622.73/295.29 mark(g(X)) -> active(g(mark(X))) 622.73/295.29 weak: 622.73/295.29 mark(f(X)) -> active(f(X)) 622.73/295.29 mark(a()) -> active(a()) 622.73/295.29 f(mark(X)) -> f(X) 622.73/295.29 f(active(X)) -> f(X) 622.73/295.29 g(mark(X)) -> g(X) 622.73/295.29 g(active(X)) -> g(X) 622.73/295.29 Splitting Processor: 622.73/295.29 strict: 622.73/295.29 mark(g(X)) -> active(g(mark(X))) 622.73/295.29 weak: 622.73/295.29 mark(f(X)) -> active(f(X)) 622.73/295.29 mark(a()) -> active(a()) 622.73/295.29 f(mark(X)) -> f(X) 622.73/295.29 f(active(X)) -> f(X) 622.73/295.29 g(mark(X)) -> g(X) 622.73/295.29 g(active(X)) -> g(X) 622.73/295.29 active(f(f(a()))) -> mark(f(g(f(a())))) 622.73/295.29 Arctic Interpretation Processor: 622.73/295.29 dimension: 2 622.73/295.29 interpretation: 622.73/295.29 622.73/295.29 [mark](x0) = x0, 622.73/295.29 622.73/295.29 [0 -&] 622.73/295.29 [g](x0) = [-& -&]x0, 622.73/295.29 622.73/295.29 622.73/295.29 [active](x0) = x0, 622.73/295.29 622.73/295.29 [0 6] 622.73/295.29 [f](x0) = [7 4]x0, 622.73/295.29 622.73/295.29 [1 ] 622.73/295.29 [a] = [-&] 622.73/295.29 orientation: 622.73/295.29 [14] [1] 622.73/295.29 active(f(f(a()))) = [12] >= [8] = mark(f(g(f(a())))) 622.73/295.29 622.73/295.29 [0 -&] [0 -&] 622.73/295.29 mark(g(X)) = [-& -&]X >= [-& -&]X = active(g(mark(X))) 622.73/295.29 622.73/295.29 [0 6] [0 6] 622.73/295.29 mark(f(X)) = [7 4]X >= [7 4]X = active(f(X)) 622.73/295.29 622.73/295.29 [1 ] [1 ] 622.73/295.29 mark(a()) = [-&] >= [-&] = active(a()) 622.73/295.29 622.73/295.29 [0 6] [0 6] 622.73/295.29 f(mark(X)) = [7 4]X >= [7 4]X = f(X) 622.73/295.29 622.73/295.29 [0 6] [0 6] 622.73/295.29 f(active(X)) = [7 4]X >= [7 4]X = f(X) 622.73/295.29 622.73/295.29 [0 -&] [0 -&] 622.73/295.29 g(mark(X)) = [-& -&]X >= [-& -&]X = g(X) 622.73/295.29 622.73/295.29 [0 -&] [0 -&] 622.73/295.29 g(active(X)) = [-& -&]X >= [-& -&]X = g(X) 622.73/295.29 problem: 622.73/295.29 strict: 622.73/295.29 622.73/295.29 weak: 622.73/295.29 active(f(f(a()))) -> mark(f(g(f(a())))) 622.73/295.29 mark(g(X)) -> active(g(mark(X))) 622.73/295.29 mark(f(X)) -> active(f(X)) 622.73/295.29 mark(a()) -> active(a()) 622.73/295.29 f(mark(X)) -> f(X) 622.73/295.29 f(active(X)) -> f(X) 622.73/295.29 g(mark(X)) -> g(X) 622.73/295.29 g(active(X)) -> g(X) 622.73/295.29 Qed 622.73/295.29 622.73/295.29 strict: 622.73/295.29 active(f(f(a()))) -> mark(f(g(f(a())))) 622.73/295.29 weak: 622.73/295.29 mark(g(X)) -> active(g(mark(X))) 622.73/295.29 mark(f(X)) -> active(f(X)) 622.73/295.29 mark(a()) -> active(a()) 622.73/295.29 f(mark(X)) -> f(X) 622.73/295.29 f(active(X)) -> f(X) 622.73/295.29 g(mark(X)) -> g(X) 622.73/295.29 g(active(X)) -> g(X) 622.73/295.29 Matrix Interpretation Processor: dim=4 622.73/295.29 622.73/295.29 max_matrix: 622.73/295.29 [1 0 0 1] 622.73/295.29 [0 0 1 0] 622.73/295.29 [0 0 0 1] 622.73/295.29 [0 0 0 1] 622.73/295.29 interpretation: 622.73/295.29 [1 0 0 1] [0] 622.73/295.29 [0 0 1 0] [0] 622.73/295.29 [mark](x0) = [0 0 0 0]x0 + [1] 622.73/295.29 [0 0 0 1] [0], 622.73/295.29 622.73/295.29 [1 0 0 0] [0] 622.73/295.29 [0 0 0 0] [0] 622.73/295.29 [g](x0) = [0 0 0 1]x0 + [0] 622.73/295.29 [0 0 0 1] [1], 622.73/295.29 622.73/295.29 [1 0 0 0] [0] 622.73/295.29 [0 0 0 0] [0] 622.73/295.29 [active](x0) = [0 0 0 0]x0 + [1] 622.73/295.29 [0 0 0 1] [0], 622.73/295.29 622.73/295.29 [1 0 0 0] [1] 622.73/295.29 [0 0 0 0] [0] 622.73/295.29 [f](x0) = [0 0 0 0]x0 + [0] 622.73/295.29 [0 0 0 0] [0], 622.73/295.29 622.73/295.29 [0] 622.73/295.29 [0] 622.73/295.29 [a] = [0] 622.73/295.29 [0] 622.73/295.29 orientation: 622.73/295.29 [1 0 0 1] [1] [1 0 0 1] [0] 622.73/295.29 [0 0 0 1] [0] [0 0 0 0] [0] 622.73/295.29 mark(g(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = active(g(mark(X))) 622.73/295.29 [0 0 0 1] [1] [0 0 0 1] [1] 622.73/295.29 622.73/295.29 [1 0 0 0] [1] [1 0 0 0] [1] 622.73/295.29 [0 0 0 0] [0] [0 0 0 0] [0] 622.73/295.29 mark(f(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = active(f(X)) 622.73/295.29 [0 0 0 0] [0] [0 0 0 0] [0] 622.73/295.29 622.73/295.29 [0] [0] 622.73/295.29 [0] [0] 622.73/295.29 mark(a()) = [1] >= [1] = active(a()) 622.73/295.29 [0] [0] 622.73/295.29 622.73/295.29 [1 0 0 1] [1] [1 0 0 0] [1] 622.73/295.29 [0 0 0 0] [0] [0 0 0 0] [0] 622.73/295.29 f(mark(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = f(X) 622.73/295.29 [0 0 0 0] [0] [0 0 0 0] [0] 622.73/295.29 622.73/295.29 [1 0 0 0] [1] [1 0 0 0] [1] 622.73/295.29 [0 0 0 0] [0] [0 0 0 0] [0] 622.73/295.29 f(active(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = f(X) 622.73/295.29 [0 0 0 0] [0] [0 0 0 0] [0] 622.73/295.29 622.73/295.29 [1 0 0 1] [0] [1 0 0 0] [0] 622.73/295.29 [0 0 0 0] [0] [0 0 0 0] [0] 622.73/295.29 g(mark(X)) = [0 0 0 1]X + [0] >= [0 0 0 1]X + [0] = g(X) 622.73/295.29 [0 0 0 1] [1] [0 0 0 1] [1] 622.73/295.29 622.73/295.29 [1 0 0 0] [0] [1 0 0 0] [0] 622.73/295.29 [0 0 0 0] [0] [0 0 0 0] [0] 622.73/295.29 g(active(X)) = [0 0 0 1]X + [0] >= [0 0 0 1]X + [0] = g(X) 622.73/295.29 [0 0 0 1] [1] [0 0 0 1] [1] 622.73/295.29 622.73/295.29 [2] [2] 622.73/295.29 [0] [0] 622.73/295.29 active(f(f(a()))) = [1] >= [1] = mark(f(g(f(a())))) 622.73/295.29 [0] [0] 622.73/295.29 problem: 622.73/295.29 strict: 622.73/295.29 622.73/295.29 weak: 622.73/295.29 mark(g(X)) -> active(g(mark(X))) 622.73/295.29 mark(f(X)) -> active(f(X)) 622.73/295.29 mark(a()) -> active(a()) 622.73/295.29 f(mark(X)) -> f(X) 622.73/295.29 f(active(X)) -> f(X) 622.73/295.29 g(mark(X)) -> g(X) 622.73/295.29 g(active(X)) -> g(X) 622.73/295.29 active(f(f(a()))) -> mark(f(g(f(a())))) 622.73/295.29 Qed 622.83/295.30 EOF