YES(?,O(n^2)) 654.57/295.40 YES(?,O(n^2)) 654.57/295.41 654.57/295.41 Problem: 654.57/295.41 active(f(X)) -> mark(g(h(f(X)))) 654.57/295.41 mark(f(X)) -> active(f(mark(X))) 654.57/295.41 mark(g(X)) -> active(g(X)) 654.57/295.41 mark(h(X)) -> active(h(mark(X))) 654.57/295.41 f(mark(X)) -> f(X) 654.57/295.41 f(active(X)) -> f(X) 654.57/295.41 g(mark(X)) -> g(X) 654.57/295.41 g(active(X)) -> g(X) 654.57/295.41 h(mark(X)) -> h(X) 654.57/295.41 h(active(X)) -> h(X) 654.57/295.41 654.57/295.41 Proof: 654.57/295.41 Complexity Transformation Processor: 654.57/295.41 strict: 654.57/295.41 active(f(X)) -> mark(g(h(f(X)))) 654.57/295.41 mark(f(X)) -> active(f(mark(X))) 654.57/295.41 mark(g(X)) -> active(g(X)) 654.57/295.41 mark(h(X)) -> active(h(mark(X))) 654.57/295.41 f(mark(X)) -> f(X) 654.57/295.41 f(active(X)) -> f(X) 654.57/295.41 g(mark(X)) -> g(X) 654.57/295.41 g(active(X)) -> g(X) 654.57/295.41 h(mark(X)) -> h(X) 654.57/295.41 h(active(X)) -> h(X) 654.57/295.41 weak: 654.57/295.41 654.57/295.41 Matrix Interpretation Processor: dim=1 654.57/295.41 654.57/295.41 max_matrix: 654.57/295.41 1 654.57/295.41 interpretation: 654.57/295.41 [mark](x0) = x0 + 32, 654.57/295.41 654.57/295.41 [g](x0) = x0, 654.57/295.41 654.57/295.41 [h](x0) = x0 + 224, 654.57/295.41 654.57/295.41 [active](x0) = x0 + 144, 654.57/295.41 654.57/295.41 [f](x0) = x0 + 241 654.57/295.41 orientation: 654.57/295.41 active(f(X)) = X + 385 >= X + 497 = mark(g(h(f(X)))) 654.57/295.41 654.57/295.41 mark(f(X)) = X + 273 >= X + 417 = active(f(mark(X))) 654.57/295.41 654.57/295.41 mark(g(X)) = X + 32 >= X + 144 = active(g(X)) 654.57/295.41 654.57/295.41 mark(h(X)) = X + 256 >= X + 400 = active(h(mark(X))) 654.57/295.41 654.57/295.41 f(mark(X)) = X + 273 >= X + 241 = f(X) 654.57/295.41 654.57/295.41 f(active(X)) = X + 385 >= X + 241 = f(X) 654.57/295.41 654.57/295.41 g(mark(X)) = X + 32 >= X = g(X) 654.57/295.41 654.57/295.41 g(active(X)) = X + 144 >= X = g(X) 654.57/295.41 654.57/295.41 h(mark(X)) = X + 256 >= X + 224 = h(X) 654.57/295.41 654.57/295.41 h(active(X)) = X + 368 >= X + 224 = h(X) 654.57/295.41 problem: 654.57/295.41 strict: 654.57/295.41 active(f(X)) -> mark(g(h(f(X)))) 654.57/295.41 mark(f(X)) -> active(f(mark(X))) 654.57/295.41 mark(g(X)) -> active(g(X)) 654.57/295.41 mark(h(X)) -> active(h(mark(X))) 654.57/295.41 weak: 654.57/295.41 f(mark(X)) -> f(X) 654.57/295.41 f(active(X)) -> f(X) 654.57/295.41 g(mark(X)) -> g(X) 654.57/295.41 g(active(X)) -> g(X) 654.57/295.41 h(mark(X)) -> h(X) 654.57/295.41 h(active(X)) -> h(X) 654.57/295.41 Matrix Interpretation Processor: dim=1 654.57/295.41 654.57/295.41 max_matrix: 654.57/295.41 1 654.57/295.41 interpretation: 654.57/295.41 [mark](x0) = x0 + 1, 654.57/295.41 654.57/295.41 [g](x0) = x0, 654.57/295.41 654.57/295.41 [h](x0) = x0 + 12, 654.57/295.41 654.57/295.41 [active](x0) = x0, 654.57/295.41 654.57/295.41 [f](x0) = x0 + 4 654.57/295.41 orientation: 654.57/295.41 active(f(X)) = X + 4 >= X + 17 = mark(g(h(f(X)))) 654.57/295.41 654.57/295.41 mark(f(X)) = X + 5 >= X + 5 = active(f(mark(X))) 654.57/295.41 654.57/295.41 mark(g(X)) = X + 1 >= X = active(g(X)) 654.57/295.41 654.57/295.41 mark(h(X)) = X + 13 >= X + 13 = active(h(mark(X))) 654.57/295.41 654.57/295.41 f(mark(X)) = X + 5 >= X + 4 = f(X) 654.57/295.41 654.57/295.41 f(active(X)) = X + 4 >= X + 4 = f(X) 654.57/295.41 654.57/295.41 g(mark(X)) = X + 1 >= X = g(X) 654.57/295.41 654.57/295.41 g(active(X)) = X >= X = g(X) 654.57/295.41 654.57/295.41 h(mark(X)) = X + 13 >= X + 12 = h(X) 654.57/295.41 654.57/295.41 h(active(X)) = X + 12 >= X + 12 = h(X) 654.57/295.41 problem: 654.57/295.41 strict: 654.57/295.41 active(f(X)) -> mark(g(h(f(X)))) 654.57/295.41 mark(f(X)) -> active(f(mark(X))) 654.57/295.41 mark(h(X)) -> active(h(mark(X))) 654.57/295.41 weak: 654.57/295.41 mark(g(X)) -> active(g(X)) 654.57/295.41 f(mark(X)) -> f(X) 654.57/295.41 f(active(X)) -> f(X) 654.57/295.41 g(mark(X)) -> g(X) 654.57/295.41 g(active(X)) -> g(X) 654.57/295.41 h(mark(X)) -> h(X) 654.57/295.41 h(active(X)) -> h(X) 654.57/295.41 Splitting Processor: 654.57/295.41 strict: 654.57/295.41 mark(h(X)) -> active(h(mark(X))) 654.57/295.41 weak: 654.57/295.41 mark(g(X)) -> active(g(X)) 654.57/295.41 f(mark(X)) -> f(X) 654.57/295.41 f(active(X)) -> f(X) 654.57/295.41 g(mark(X)) -> g(X) 654.57/295.41 g(active(X)) -> g(X) 654.57/295.41 h(mark(X)) -> h(X) 654.57/295.41 h(active(X)) -> h(X) 654.57/295.41 active(f(X)) -> mark(g(h(f(X)))) 654.57/295.41 mark(f(X)) -> active(f(mark(X))) 654.57/295.41 Matrix Interpretation Processor: dim=4 654.57/295.41 654.57/295.41 max_matrix: 654.57/295.41 [1 0 1 0] 654.57/295.41 [0 0 1 0] 654.57/295.41 [0 0 1 1] 654.57/295.41 [0 0 0 0] 654.57/295.41 interpretation: 654.57/295.41 [1 0 1 0] [0] 654.57/295.41 [0 0 1 0] [1] 654.57/295.41 [mark](x0) = [0 0 1 1]x0 + [0] 654.57/295.41 [0 0 0 0] [0], 654.57/295.41 654.57/295.41 [1 0 0 0] [0] 654.57/295.41 [0 0 0 0] [0] 654.57/295.41 [g](x0) = [0 0 0 0]x0 + [0] 654.57/295.41 [0 0 0 0] [1], 654.57/295.41 654.57/295.41 [1 0 0 0] [0] 654.57/295.41 [0 0 1 0] [1] 654.57/295.41 [h](x0) = [0 0 1 1]x0 + [0] 654.57/295.41 [0 0 0 0] [0], 654.57/295.41 654.57/295.41 [1 0 0 0] 654.57/295.41 [0 0 1 0] 654.57/295.41 [active](x0) = [0 0 1 1]x0 654.57/295.41 [0 0 0 0] , 654.57/295.41 654.57/295.41 [1 0 0 0] [1] 654.57/295.41 [0 0 0 0] [0] 654.57/295.41 [f](x0) = [0 0 1 1]x0 + [1] 654.57/295.41 [0 0 0 0] [0] 654.57/295.41 orientation: 654.57/295.41 [1 0 0 0] [1] [1 0 0 0] [1] 654.57/295.42 [0 0 1 1] [1] [0 0 0 0] [1] 654.57/295.42 active(f(X)) = [0 0 1 1]X + [1] >= [0 0 0 0]X + [1] = mark(g(h(f(X)))) 654.57/295.42 [0 0 0 0] [0] [0 0 0 0] [0] 654.57/295.42 654.57/295.42 [1 0 1 1] [2] [1 0 1 0] [1] 654.57/295.42 [0 0 1 1] [2] [0 0 1 1] [1] 654.57/295.42 mark(f(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = active(f(mark(X))) 654.57/295.42 [0 0 0 0] [0] [0 0 0 0] [0] 654.57/295.42 654.57/295.42 [1 0 1 1] [0] [1 0 1 0] 654.57/295.42 [0 0 1 1] [1] [0 0 1 1] 654.57/295.42 mark(h(X)) = [0 0 1 1]X + [0] >= [0 0 1 1]X = active(h(mark(X))) 654.57/295.42 [0 0 0 0] [0] [0 0 0 0] 654.57/295.42 654.57/295.42 [1 0 0 0] [0] [1 0 0 0] [0] 654.57/295.42 [0 0 0 0] [1] [0 0 0 0] [0] 654.57/295.42 mark(g(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = active(g(X)) 654.57/295.42 [0 0 0 0] [0] [0 0 0 0] [0] 654.57/295.42 654.57/295.42 [1 0 1 0] [1] [1 0 0 0] [1] 654.57/295.42 [0 0 0 0] [0] [0 0 0 0] [0] 654.57/295.42 f(mark(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = f(X) 654.57/295.42 [0 0 0 0] [0] [0 0 0 0] [0] 654.57/295.42 654.57/295.42 [1 0 0 0] [1] [1 0 0 0] [1] 654.57/295.42 [0 0 0 0] [0] [0 0 0 0] [0] 654.57/295.42 f(active(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = f(X) 654.57/295.42 [0 0 0 0] [0] [0 0 0 0] [0] 654.57/295.42 654.57/295.42 [1 0 1 0] [0] [1 0 0 0] [0] 654.57/295.42 [0 0 0 0] [0] [0 0 0 0] [0] 654.57/295.42 g(mark(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = g(X) 654.57/295.42 [0 0 0 0] [1] [0 0 0 0] [1] 654.57/295.42 654.57/295.42 [1 0 0 0] [0] [1 0 0 0] [0] 654.57/295.42 [0 0 0 0] [0] [0 0 0 0] [0] 654.57/295.42 g(active(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = g(X) 654.57/295.42 [0 0 0 0] [1] [0 0 0 0] [1] 654.57/295.42 654.57/295.42 [1 0 1 0] [0] [1 0 0 0] [0] 654.57/295.42 [0 0 1 1] [1] [0 0 1 0] [1] 654.57/295.42 h(mark(X)) = [0 0 1 1]X + [0] >= [0 0 1 1]X + [0] = h(X) 654.57/295.42 [0 0 0 0] [0] [0 0 0 0] [0] 654.57/295.42 654.57/295.42 [1 0 0 0] [0] [1 0 0 0] [0] 654.57/295.42 [0 0 1 1] [1] [0 0 1 0] [1] 654.57/295.42 h(active(X)) = [0 0 1 1]X + [0] >= [0 0 1 1]X + [0] = h(X) 654.57/295.42 [0 0 0 0] [0] [0 0 0 0] [0] 654.57/295.42 problem: 654.57/295.42 strict: 654.57/295.42 active(f(X)) -> mark(g(h(f(X)))) 654.57/295.42 weak: 654.57/295.42 mark(f(X)) -> active(f(mark(X))) 654.57/295.42 mark(h(X)) -> active(h(mark(X))) 654.57/295.42 mark(g(X)) -> active(g(X)) 654.57/295.42 f(mark(X)) -> f(X) 654.57/295.42 f(active(X)) -> f(X) 654.57/295.42 g(mark(X)) -> g(X) 654.57/295.42 g(active(X)) -> g(X) 654.57/295.42 h(mark(X)) -> h(X) 654.57/295.42 h(active(X)) -> h(X) 654.57/295.42 Matrix Interpretation Processor: dim=3 654.57/295.42 654.57/295.42 max_matrix: 654.57/295.42 [1 1 1] 654.57/295.42 [0 1 0] 654.57/295.42 [0 0 0] 654.57/295.42 interpretation: 654.57/295.42 [1 1 0] [0] 654.57/295.42 [mark](x0) = [0 1 0]x0 + [1] 654.57/295.42 [0 0 0] [1], 654.57/295.42 654.57/295.42 [1 0 0] 654.57/295.42 [g](x0) = [0 0 0]x0 654.57/295.42 [0 0 0] , 654.57/295.42 654.57/295.42 [1 0 0] [0] 654.57/295.42 [h](x0) = [0 1 0]x0 + [1] 654.57/295.42 [0 0 0] [0], 654.57/295.42 654.57/295.42 [1 0 1] [0] 654.57/295.42 [active](x0) = [0 1 0]x0 + [0] 654.57/295.42 [0 0 0] [1], 654.57/295.42 654.57/295.42 [1 0 0] [1] 654.57/295.42 [f](x0) = [0 1 0]x0 + [1] 654.57/295.42 [0 0 0] [1] 654.57/295.42 orientation: 654.57/295.42 [1 0 0] [2] [1 0 0] [1] 654.57/295.42 active(f(X)) = [0 1 0]X + [1] >= [0 0 0]X + [1] = mark(g(h(f(X)))) 654.57/295.42 [0 0 0] [1] [0 0 0] [1] 654.57/295.42 654.57/295.42 [1 1 0] [2] [1 1 0] [2] 654.57/295.42 mark(f(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = active(f(mark(X))) 654.57/295.42 [0 0 0] [1] [0 0 0] [1] 654.57/295.42 654.57/295.42 [1 1 0] [1] [1 1 0] [0] 654.57/295.42 mark(h(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = active(h(mark(X))) 654.57/295.42 [0 0 0] [1] [0 0 0] [1] 654.57/295.42 654.57/295.42 [1 0 0] [0] [1 0 0] [0] 654.57/295.42 mark(g(X)) = [0 0 0]X + [1] >= [0 0 0]X + [0] = active(g(X)) 654.57/295.42 [0 0 0] [1] [0 0 0] [1] 654.57/295.42 654.57/295.42 [1 1 0] [1] [1 0 0] [1] 654.57/295.42 f(mark(X)) = [0 1 0]X + [2] >= [0 1 0]X + [1] = f(X) 654.57/295.42 [0 0 0] [1] [0 0 0] [1] 654.57/295.42 654.57/295.42 [1 0 1] [1] [1 0 0] [1] 654.57/295.42 f(active(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = f(X) 654.57/295.42 [0 0 0] [1] [0 0 0] [1] 654.57/295.42 654.57/295.42 [1 1 0] [1 0 0] 654.57/295.42 g(mark(X)) = [0 0 0]X >= [0 0 0]X = g(X) 654.57/295.42 [0 0 0] [0 0 0] 654.57/295.42 654.57/295.42 [1 0 1] [1 0 0] 654.57/295.42 g(active(X)) = [0 0 0]X >= [0 0 0]X = g(X) 654.57/295.42 [0 0 0] [0 0 0] 654.57/295.42 654.57/295.42 [1 1 0] [0] [1 0 0] [0] 654.57/295.42 h(mark(X)) = [0 1 0]X + [2] >= [0 1 0]X + [1] = h(X) 654.57/295.42 [0 0 0] [0] [0 0 0] [0] 654.57/295.42 654.57/295.42 [1 0 1] [0] [1 0 0] [0] 654.57/295.42 h(active(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = h(X) 654.57/295.42 [0 0 0] [0] [0 0 0] [0] 654.57/295.42 problem: 654.57/295.42 strict: 654.57/295.42 654.57/295.42 weak: 654.57/295.42 active(f(X)) -> mark(g(h(f(X)))) 654.57/295.42 mark(f(X)) -> active(f(mark(X))) 654.57/295.42 mark(h(X)) -> active(h(mark(X))) 654.57/295.42 mark(g(X)) -> active(g(X)) 654.57/295.42 f(mark(X)) -> f(X) 654.57/295.42 f(active(X)) -> f(X) 654.57/295.42 g(mark(X)) -> g(X) 654.57/295.42 g(active(X)) -> g(X) 654.57/295.42 h(mark(X)) -> h(X) 654.57/295.42 h(active(X)) -> h(X) 654.57/295.42 Qed 654.57/295.42 654.57/295.42 strict: 654.57/295.42 active(f(X)) -> mark(g(h(f(X)))) 654.57/295.42 mark(f(X)) -> active(f(mark(X))) 654.57/295.42 weak: 654.57/295.42 mark(h(X)) -> active(h(mark(X))) 654.57/295.42 mark(g(X)) -> active(g(X)) 654.57/295.42 f(mark(X)) -> f(X) 654.57/295.42 f(active(X)) -> f(X) 654.57/295.42 g(mark(X)) -> g(X) 654.57/295.42 g(active(X)) -> g(X) 654.57/295.42 h(mark(X)) -> h(X) 654.57/295.42 h(active(X)) -> h(X) 654.57/295.42 Matrix Interpretation Processor: dim=3 654.57/295.42 654.57/295.42 max_matrix: 654.57/295.42 [1 1 1] 654.57/295.42 [0 1 1] 654.57/295.42 [0 0 0] 654.57/295.42 interpretation: 654.57/295.42 [1 1 1] [1] 654.57/295.42 [mark](x0) = [0 1 1]x0 + [1] 654.57/295.42 [0 0 0] [0], 654.57/295.42 654.57/295.42 [1 0 0] 654.57/295.42 [g](x0) = [0 0 0]x0 654.57/295.42 [0 0 0] , 654.57/295.42 654.57/295.42 [1 0 0] [0] 654.57/295.42 [h](x0) = [0 1 1]x0 + [1] 654.57/295.42 [0 0 0] [1], 654.57/295.42 654.57/295.42 [1 0 1] 654.57/295.42 [active](x0) = [0 1 1]x0 654.57/295.42 [0 0 0] , 654.57/295.42 654.57/295.42 [1 0 0] [0] 654.57/295.42 [f](x0) = [0 1 1]x0 + [1] 654.57/295.42 [0 0 0] [1] 654.57/295.42 orientation: 654.57/295.42 [1 1 1] [3] [1 1 1] [2] 654.57/295.42 mark(h(X)) = [0 1 1]X + [3] >= [0 1 1]X + [3] = active(h(mark(X))) 654.57/295.42 [0 0 0] [0] [0 0 0] [0] 654.57/295.42 654.57/295.42 [1 0 0] [1] [1 0 0] 654.57/295.42 mark(g(X)) = [0 0 0]X + [1] >= [0 0 0]X = active(g(X)) 654.57/295.42 [0 0 0] [0] [0 0 0] 654.57/295.42 654.57/295.42 [1 1 1] [1] [1 0 0] [0] 654.57/295.42 f(mark(X)) = [0 1 1]X + [2] >= [0 1 1]X + [1] = f(X) 654.57/295.42 [0 0 0] [1] [0 0 0] [1] 654.57/295.42 654.57/295.42 [1 0 1] [0] [1 0 0] [0] 654.57/295.42 f(active(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = f(X) 654.57/295.42 [0 0 0] [1] [0 0 0] [1] 654.57/295.42 654.57/295.42 [1 1 1] [1] [1 0 0] 654.57/295.42 g(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X = g(X) 654.57/295.42 [0 0 0] [0] [0 0 0] 654.57/295.42 654.57/295.42 [1 0 1] [1 0 0] 654.57/295.42 g(active(X)) = [0 0 0]X >= [0 0 0]X = g(X) 654.57/295.42 [0 0 0] [0 0 0] 654.57/295.42 654.57/295.42 [1 1 1] [1] [1 0 0] [0] 654.57/295.42 h(mark(X)) = [0 1 1]X + [2] >= [0 1 1]X + [1] = h(X) 654.57/295.42 [0 0 0] [1] [0 0 0] [1] 654.57/295.42 654.57/295.42 [1 0 1] [0] [1 0 0] [0] 654.57/295.42 h(active(X)) = [0 1 1]X + [1] >= [0 1 1]X + [1] = h(X) 654.57/295.42 [0 0 0] [1] [0 0 0] [1] 654.57/295.42 654.57/295.42 [1 0 0] [1] [1 0 0] [1] 654.57/295.42 active(f(X)) = [0 1 1]X + [2] >= [0 0 0]X + [1] = mark(g(h(f(X)))) 654.57/295.42 [0 0 0] [0] [0 0 0] [0] 654.57/295.42 654.57/295.42 [1 1 1] [3] [1 1 1] [2] 654.57/295.42 mark(f(X)) = [0 1 1]X + [3] >= [0 1 1]X + [3] = active(f(mark(X))) 654.57/295.42 [0 0 0] [0] [0 0 0] [0] 654.57/295.42 problem: 654.57/295.42 strict: 654.57/295.42 654.57/295.42 weak: 654.57/295.42 mark(h(X)) -> active(h(mark(X))) 654.57/295.42 mark(g(X)) -> active(g(X)) 654.57/295.42 f(mark(X)) -> f(X) 654.57/295.42 f(active(X)) -> f(X) 654.57/295.42 g(mark(X)) -> g(X) 654.57/295.42 g(active(X)) -> g(X) 654.57/295.42 h(mark(X)) -> h(X) 654.57/295.42 h(active(X)) -> h(X) 654.57/295.42 active(f(X)) -> mark(g(h(f(X)))) 654.57/295.42 mark(f(X)) -> active(f(mark(X))) 654.57/295.42 Qed 654.57/295.43 EOF