YES(?,O(n^2)) 650.31/295.35 YES(?,O(n^2)) 650.31/295.35 650.31/295.35 Problem: 650.31/295.35 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 650.31/295.35 mark(f(X)) -> active(f(mark(X))) 650.31/295.35 mark(a()) -> active(a()) 650.31/295.35 mark(c(X)) -> active(c(X)) 650.31/295.35 mark(g(X)) -> active(g(mark(X))) 650.31/295.35 f(mark(X)) -> f(X) 650.31/295.35 f(active(X)) -> f(X) 650.31/295.35 c(mark(X)) -> c(X) 650.31/295.35 c(active(X)) -> c(X) 650.31/295.35 g(mark(X)) -> g(X) 650.31/295.35 g(active(X)) -> g(X) 650.31/295.35 650.31/295.35 Proof: 650.31/295.35 Complexity Transformation Processor: 650.31/295.35 strict: 650.31/295.35 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 650.31/295.35 mark(f(X)) -> active(f(mark(X))) 650.31/295.35 mark(a()) -> active(a()) 650.31/295.35 mark(c(X)) -> active(c(X)) 650.31/295.35 mark(g(X)) -> active(g(mark(X))) 650.31/295.35 f(mark(X)) -> f(X) 650.31/295.35 f(active(X)) -> f(X) 650.31/295.35 c(mark(X)) -> c(X) 650.31/295.35 c(active(X)) -> c(X) 650.31/295.35 g(mark(X)) -> g(X) 650.31/295.35 g(active(X)) -> g(X) 650.31/295.35 weak: 650.31/295.35 650.31/295.35 Matrix Interpretation Processor: dim=1 650.31/295.35 650.31/295.35 max_matrix: 650.31/295.35 1 650.31/295.35 interpretation: 650.31/295.35 [mark](x0) = x0 + 6, 650.31/295.35 650.31/295.35 [c](x0) = x0 + 8, 650.31/295.35 650.31/295.35 [g](x0) = x0 + 2, 650.31/295.35 650.31/295.35 [active](x0) = x0 + 9, 650.31/295.35 650.31/295.35 [f](x0) = x0 + 3, 650.31/295.35 650.31/295.35 [a] = 8 650.31/295.35 orientation: 650.31/295.35 active(f(f(a()))) = 23 >= 30 = mark(c(f(g(f(a()))))) 650.31/295.35 650.31/295.35 mark(f(X)) = X + 9 >= X + 18 = active(f(mark(X))) 650.31/295.35 650.31/295.35 mark(a()) = 14 >= 17 = active(a()) 650.31/295.35 650.31/295.35 mark(c(X)) = X + 14 >= X + 17 = active(c(X)) 650.31/295.35 650.31/295.35 mark(g(X)) = X + 8 >= X + 17 = active(g(mark(X))) 650.31/295.35 650.31/295.35 f(mark(X)) = X + 9 >= X + 3 = f(X) 650.31/295.35 650.31/295.35 f(active(X)) = X + 12 >= X + 3 = f(X) 650.31/295.35 650.31/295.35 c(mark(X)) = X + 14 >= X + 8 = c(X) 650.31/295.35 650.31/295.35 c(active(X)) = X + 17 >= X + 8 = c(X) 650.31/295.35 650.31/295.35 g(mark(X)) = X + 8 >= X + 2 = g(X) 650.31/295.35 650.31/295.35 g(active(X)) = X + 11 >= X + 2 = g(X) 650.31/295.35 problem: 650.31/295.35 strict: 650.31/295.35 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 650.31/295.35 mark(f(X)) -> active(f(mark(X))) 650.31/295.35 mark(a()) -> active(a()) 650.31/295.35 mark(c(X)) -> active(c(X)) 650.31/295.35 mark(g(X)) -> active(g(mark(X))) 650.31/295.35 weak: 650.31/295.35 f(mark(X)) -> f(X) 650.31/295.35 f(active(X)) -> f(X) 650.31/295.35 c(mark(X)) -> c(X) 650.31/295.35 c(active(X)) -> c(X) 650.31/295.35 g(mark(X)) -> g(X) 650.31/295.35 g(active(X)) -> g(X) 650.31/295.35 Matrix Interpretation Processor: dim=1 650.31/295.35 650.31/295.35 max_matrix: 650.31/295.35 1 650.31/295.35 interpretation: 650.31/295.35 [mark](x0) = x0 + 2, 650.31/295.35 650.31/295.35 [c](x0) = x0, 650.31/295.35 650.31/295.35 [g](x0) = x0, 650.31/295.35 650.31/295.35 [active](x0) = x0 + 1, 650.31/295.35 650.31/295.35 [f](x0) = x0, 650.31/295.35 650.31/295.35 [a] = 0 650.31/295.35 orientation: 650.31/295.35 active(f(f(a()))) = 1 >= 2 = mark(c(f(g(f(a()))))) 650.31/295.35 650.31/295.35 mark(f(X)) = X + 2 >= X + 3 = active(f(mark(X))) 650.31/295.35 650.31/295.35 mark(a()) = 2 >= 1 = active(a()) 650.31/295.35 650.31/295.35 mark(c(X)) = X + 2 >= X + 1 = active(c(X)) 650.31/295.35 650.31/295.35 mark(g(X)) = X + 2 >= X + 3 = active(g(mark(X))) 650.31/295.35 650.31/295.35 f(mark(X)) = X + 2 >= X = f(X) 650.31/295.35 650.31/295.35 f(active(X)) = X + 1 >= X = f(X) 650.31/295.35 650.31/295.35 c(mark(X)) = X + 2 >= X = c(X) 650.31/295.35 650.31/295.35 c(active(X)) = X + 1 >= X = c(X) 650.31/295.35 650.31/295.35 g(mark(X)) = X + 2 >= X = g(X) 650.31/295.35 650.31/295.35 g(active(X)) = X + 1 >= X = g(X) 650.31/295.35 problem: 650.31/295.35 strict: 650.31/295.35 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 650.31/295.35 mark(f(X)) -> active(f(mark(X))) 650.31/295.35 mark(g(X)) -> active(g(mark(X))) 650.31/295.35 weak: 650.31/295.35 mark(a()) -> active(a()) 650.31/295.35 mark(c(X)) -> active(c(X)) 650.31/295.35 f(mark(X)) -> f(X) 650.31/295.35 f(active(X)) -> f(X) 650.31/295.35 c(mark(X)) -> c(X) 650.31/295.35 c(active(X)) -> c(X) 650.31/295.35 g(mark(X)) -> g(X) 650.31/295.35 g(active(X)) -> g(X) 650.31/295.35 Splitting Processor: 650.31/295.35 strict: 650.31/295.35 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 650.31/295.35 mark(f(X)) -> active(f(mark(X))) 650.31/295.35 weak: 650.31/295.35 mark(a()) -> active(a()) 650.31/295.35 mark(c(X)) -> active(c(X)) 650.31/295.35 f(mark(X)) -> f(X) 650.31/295.35 f(active(X)) -> f(X) 650.31/295.35 c(mark(X)) -> c(X) 650.31/295.35 c(active(X)) -> c(X) 650.31/295.35 g(mark(X)) -> g(X) 650.31/295.35 g(active(X)) -> g(X) 650.31/295.35 mark(g(X)) -> active(g(mark(X))) 650.31/295.35 Matrix Interpretation Processor: dim=3 650.31/295.35 650.31/295.35 max_matrix: 650.31/295.35 [1 0 1] 650.31/295.35 [0 0 1] 650.31/295.35 [0 0 1] 650.31/295.35 interpretation: 650.31/295.35 [1 0 1] 650.31/295.35 [mark](x0) = [0 0 0]x0 650.31/295.35 [0 0 1] , 650.31/295.35 650.31/295.35 [1 0 0] [0] 650.31/295.35 [c](x0) = [0 0 1]x0 + [1] 650.31/295.35 [0 0 0] [0], 650.31/295.35 650.31/295.35 [1 0 0] [0] 650.31/295.35 [g](x0) = [0 0 0]x0 + [0] 650.31/295.35 [0 0 1] [1], 650.31/295.35 650.31/295.35 [1 0 0] 650.31/295.35 [active](x0) = [0 0 0]x0 650.31/295.35 [0 0 1] , 650.31/295.35 650.31/295.35 [1 0 0] 650.31/295.35 [f](x0) = [0 0 1]x0 650.31/295.35 [0 0 1] , 650.31/295.35 650.31/295.35 [1] 650.31/295.35 [a] = [0] 650.31/295.36 [0] 650.31/295.36 orientation: 650.31/295.36 [1 0 1] [1] [1 0 1] [0] 650.31/295.36 mark(g(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(g(mark(X))) 650.31/295.36 [0 0 1] [1] [0 0 1] [1] 650.31/295.36 650.31/295.36 [1] [1] 650.31/295.36 active(f(f(a()))) = [0] >= [0] = mark(c(f(g(f(a()))))) 650.31/295.36 [0] [0] 650.31/295.36 650.31/295.36 [1 0 1] [1 0 1] 650.31/295.36 mark(f(X)) = [0 0 0]X >= [0 0 0]X = active(f(mark(X))) 650.31/295.36 [0 0 1] [0 0 1] 650.31/295.36 650.31/295.36 [1] [1] 650.31/295.36 mark(a()) = [0] >= [0] = active(a()) 650.31/295.36 [0] [0] 650.31/295.36 650.31/295.36 [1 0 0] [1 0 0] 650.31/295.36 mark(c(X)) = [0 0 0]X >= [0 0 0]X = active(c(X)) 650.31/295.36 [0 0 0] [0 0 0] 650.31/295.36 650.31/295.36 [1 0 1] [1 0 0] 650.31/295.36 f(mark(X)) = [0 0 1]X >= [0 0 1]X = f(X) 650.31/295.36 [0 0 1] [0 0 1] 650.31/295.36 650.31/295.36 [1 0 0] [1 0 0] 650.31/295.36 f(active(X)) = [0 0 1]X >= [0 0 1]X = f(X) 650.31/295.36 [0 0 1] [0 0 1] 650.31/295.36 650.31/295.36 [1 0 1] [0] [1 0 0] [0] 650.31/295.36 c(mark(X)) = [0 0 1]X + [1] >= [0 0 1]X + [1] = c(X) 650.31/295.36 [0 0 0] [0] [0 0 0] [0] 650.31/295.36 650.31/295.36 [1 0 0] [0] [1 0 0] [0] 650.31/295.36 c(active(X)) = [0 0 1]X + [1] >= [0 0 1]X + [1] = c(X) 650.31/295.36 [0 0 0] [0] [0 0 0] [0] 650.31/295.36 650.31/295.36 [1 0 1] [0] [1 0 0] [0] 650.31/295.36 g(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = g(X) 650.31/295.36 [0 0 1] [1] [0 0 1] [1] 650.31/295.36 650.31/295.36 [1 0 0] [0] [1 0 0] [0] 650.31/295.36 g(active(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = g(X) 650.31/295.36 [0 0 1] [1] [0 0 1] [1] 650.31/295.36 problem: 650.31/295.36 strict: 650.31/295.36 650.31/295.36 weak: 650.31/295.36 mark(g(X)) -> active(g(mark(X))) 650.31/295.36 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 650.31/295.36 mark(f(X)) -> active(f(mark(X))) 650.31/295.36 mark(a()) -> active(a()) 650.31/295.36 mark(c(X)) -> active(c(X)) 650.31/295.36 f(mark(X)) -> f(X) 650.31/295.36 f(active(X)) -> f(X) 650.31/295.36 c(mark(X)) -> c(X) 650.31/295.36 c(active(X)) -> c(X) 650.31/295.36 g(mark(X)) -> g(X) 650.31/295.36 g(active(X)) -> g(X) 650.31/295.36 Qed 650.31/295.36 650.31/295.36 strict: 650.31/295.36 mark(g(X)) -> active(g(mark(X))) 650.31/295.36 weak: 650.31/295.36 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 650.31/295.36 mark(f(X)) -> active(f(mark(X))) 650.31/295.36 mark(a()) -> active(a()) 650.31/295.36 mark(c(X)) -> active(c(X)) 650.31/295.36 f(mark(X)) -> f(X) 650.31/295.36 f(active(X)) -> f(X) 650.31/295.36 c(mark(X)) -> c(X) 650.31/295.36 c(active(X)) -> c(X) 650.31/295.36 g(mark(X)) -> g(X) 650.31/295.36 g(active(X)) -> g(X) 650.31/295.36 Splitting Processor: 650.31/295.36 strict: 650.31/295.36 mark(f(X)) -> active(f(mark(X))) 650.31/295.36 weak: 650.31/295.36 mark(a()) -> active(a()) 650.31/295.36 mark(c(X)) -> active(c(X)) 650.31/295.36 f(mark(X)) -> f(X) 650.31/295.36 f(active(X)) -> f(X) 650.31/295.36 c(mark(X)) -> c(X) 650.31/295.36 c(active(X)) -> c(X) 650.31/295.36 g(mark(X)) -> g(X) 650.31/295.36 g(active(X)) -> g(X) 650.31/295.36 mark(g(X)) -> active(g(mark(X))) 650.31/295.36 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 650.31/295.36 Matrix Interpretation Processor: dim=3 650.31/295.36 650.31/295.36 max_matrix: 650.31/295.36 [1 1 1] 650.31/295.36 [0 1 0] 650.31/295.36 [0 0 0] 650.31/295.36 interpretation: 650.31/295.36 [1 0 1] [0] 650.31/295.36 [mark](x0) = [0 0 0]x0 + [1] 650.31/295.36 [0 0 0] [0], 650.31/295.36 650.31/295.36 [1 0 0] 650.31/295.36 [c](x0) = [0 0 0]x0 650.31/295.36 [0 0 0] , 650.31/295.36 650.31/295.36 [1 0 1] 650.31/295.36 [g](x0) = [0 0 0]x0 650.31/295.36 [0 0 0] , 650.31/295.36 650.31/295.36 [1 1 1] [0] 650.31/295.36 [active](x0) = [0 1 0]x0 + [1] 650.31/295.36 [0 0 0] [0], 650.31/295.36 650.31/295.36 [1 0 1] [0] 650.31/295.36 [f](x0) = [0 0 0]x0 + [0] 650.31/295.36 [0 0 0] [1], 650.31/295.36 650.31/295.36 [1] 650.31/295.36 [a] = [0] 650.31/295.36 [0] 650.31/295.36 orientation: 650.31/295.36 [3] [2] 650.31/295.36 active(f(f(a()))) = [1] >= [1] = mark(c(f(g(f(a()))))) 650.31/295.36 [0] [0] 650.31/295.36 650.31/295.36 [1 0 1] [1] [1 0 1] [1] 650.31/295.36 mark(f(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = active(f(mark(X))) 650.31/295.36 [0 0 0] [0] [0 0 0] [0] 650.31/295.36 650.31/295.36 [1] [1] 650.31/295.36 mark(a()) = [1] >= [1] = active(a()) 650.31/295.36 [0] [0] 650.31/295.36 650.31/295.36 [1 0 0] [0] [1 0 0] [0] 650.31/295.36 mark(c(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = active(c(X)) 650.31/295.36 [0 0 0] [0] [0 0 0] [0] 650.31/295.36 650.31/295.36 [1 0 1] [0] [1 0 1] [0] 650.31/295.36 f(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(X) 650.31/295.36 [0 0 0] [1] [0 0 0] [1] 650.31/295.36 650.31/295.36 [1 1 1] [0] [1 0 1] [0] 650.31/295.36 f(active(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(X) 650.31/295.36 [0 0 0] [1] [0 0 0] [1] 650.31/295.36 650.31/295.36 [1 0 1] [1 0 0] 650.31/295.36 c(mark(X)) = [0 0 0]X >= [0 0 0]X = c(X) 650.31/295.36 [0 0 0] [0 0 0] 650.31/295.36 650.31/295.36 [1 1 1] [1 0 0] 650.31/295.36 c(active(X)) = [0 0 0]X >= [0 0 0]X = c(X) 650.31/295.36 [0 0 0] [0 0 0] 650.31/295.36 650.31/295.36 [1 0 1] [1 0 1] 650.31/295.36 g(mark(X)) = [0 0 0]X >= [0 0 0]X = g(X) 650.31/295.36 [0 0 0] [0 0 0] 650.31/295.36 650.31/295.36 [1 1 1] [1 0 1] 650.31/295.36 g(active(X)) = [0 0 0]X >= [0 0 0]X = g(X) 650.31/295.36 [0 0 0] [0 0 0] 650.31/295.36 650.31/295.36 [1 0 1] [0] [1 0 1] [0] 650.31/295.36 mark(g(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = active(g(mark(X))) 650.31/295.36 [0 0 0] [0] [0 0 0] [0] 650.31/295.36 problem: 650.31/295.36 strict: 650.31/295.36 650.31/295.36 weak: 650.31/295.36 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 650.31/295.36 mark(f(X)) -> active(f(mark(X))) 650.31/295.36 mark(a()) -> active(a()) 650.31/295.36 mark(c(X)) -> active(c(X)) 650.31/295.36 f(mark(X)) -> f(X) 650.31/295.36 f(active(X)) -> f(X) 650.31/295.36 c(mark(X)) -> c(X) 650.31/295.36 c(active(X)) -> c(X) 650.31/295.36 g(mark(X)) -> g(X) 650.31/295.36 g(active(X)) -> g(X) 650.31/295.36 mark(g(X)) -> active(g(mark(X))) 650.31/295.36 Qed 650.31/295.36 650.31/295.36 strict: 650.31/295.36 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 650.31/295.36 weak: 650.31/295.36 mark(f(X)) -> active(f(mark(X))) 650.31/295.36 mark(a()) -> active(a()) 650.31/295.36 mark(c(X)) -> active(c(X)) 650.31/295.36 f(mark(X)) -> f(X) 650.31/295.36 f(active(X)) -> f(X) 650.31/295.36 c(mark(X)) -> c(X) 650.31/295.36 c(active(X)) -> c(X) 650.31/295.36 g(mark(X)) -> g(X) 650.31/295.36 g(active(X)) -> g(X) 650.31/295.36 mark(g(X)) -> active(g(mark(X))) 650.31/295.36 Matrix Interpretation Processor: dim=3 650.31/295.36 650.31/295.36 max_matrix: 650.31/295.36 [1 1 0] 650.31/295.36 [0 1 0] 650.31/295.36 [0 0 0] 650.31/295.36 interpretation: 650.31/295.36 [1 1 0] 650.31/295.36 [mark](x0) = [0 1 0]x0 650.31/295.36 [0 0 0] , 650.31/295.36 650.31/295.36 [1 0 0] 650.31/295.36 [c](x0) = [0 0 0]x0 650.31/295.36 [0 0 0] , 650.31/295.36 650.31/295.36 [1 0 0] [0] 650.31/295.36 [g](x0) = [0 1 0]x0 + [1] 650.31/295.36 [0 0 0] [1], 650.31/295.36 650.31/295.36 [1 0 0] 650.31/295.36 [active](x0) = [0 1 0]x0 650.31/295.36 [0 0 0] , 650.31/295.36 650.31/295.36 [1 0 0] [0] 650.31/295.36 [f](x0) = [0 1 0]x0 + [1] 650.31/295.36 [0 0 0] [0], 650.31/295.36 650.31/295.36 [0] 650.31/295.36 [a] = [0] 650.31/295.36 [0] 650.31/295.36 orientation: 650.31/295.36 [1 1 0] [1] [1 1 0] [0] 650.31/295.36 mark(f(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = active(f(mark(X))) 650.31/295.36 [0 0 0] [0] [0 0 0] [0] 650.31/295.36 650.31/295.36 [0] [0] 650.31/295.36 mark(a()) = [0] >= [0] = active(a()) 650.31/295.36 [0] [0] 650.31/295.36 650.31/295.36 [1 0 0] [1 0 0] 650.31/295.36 mark(c(X)) = [0 0 0]X >= [0 0 0]X = active(c(X)) 650.31/295.36 [0 0 0] [0 0 0] 650.31/295.37 650.31/295.37 [1 1 0] [0] [1 0 0] [0] 650.31/295.37 f(mark(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = f(X) 650.31/295.37 [0 0 0] [0] [0 0 0] [0] 650.31/295.37 650.31/295.37 [1 0 0] [0] [1 0 0] [0] 650.31/295.37 f(active(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = f(X) 650.31/295.37 [0 0 0] [0] [0 0 0] [0] 650.31/295.37 650.31/295.37 [1 1 0] [1 0 0] 650.31/295.37 c(mark(X)) = [0 0 0]X >= [0 0 0]X = c(X) 650.31/295.37 [0 0 0] [0 0 0] 650.31/295.37 650.31/295.37 [1 0 0] [1 0 0] 650.31/295.37 c(active(X)) = [0 0 0]X >= [0 0 0]X = c(X) 650.31/295.37 [0 0 0] [0 0 0] 650.31/295.37 650.31/295.37 [1 1 0] [0] [1 0 0] [0] 650.31/295.37 g(mark(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = g(X) 650.31/295.37 [0 0 0] [1] [0 0 0] [1] 650.31/295.37 650.31/295.37 [1 0 0] [0] [1 0 0] [0] 650.31/295.37 g(active(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = g(X) 650.31/295.37 [0 0 0] [1] [0 0 0] [1] 650.31/295.37 650.31/295.37 [1 1 0] [1] [1 1 0] [0] 650.31/295.37 mark(g(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = active(g(mark(X))) 650.31/295.37 [0 0 0] [0] [0 0 0] [0] 650.31/295.37 650.31/295.37 [0] [0] 650.31/295.37 active(f(f(a()))) = [2] >= [0] = mark(c(f(g(f(a()))))) 650.31/295.37 [0] [0] 650.31/295.37 problem: 650.31/295.37 strict: 650.31/295.37 650.31/295.37 weak: 650.31/295.37 mark(f(X)) -> active(f(mark(X))) 650.31/295.37 mark(a()) -> active(a()) 650.31/295.37 mark(c(X)) -> active(c(X)) 650.31/295.37 f(mark(X)) -> f(X) 650.31/295.37 f(active(X)) -> f(X) 650.31/295.37 c(mark(X)) -> c(X) 650.31/295.37 c(active(X)) -> c(X) 650.31/295.37 g(mark(X)) -> g(X) 650.31/295.37 g(active(X)) -> g(X) 650.31/295.37 mark(g(X)) -> active(g(mark(X))) 650.31/295.37 active(f(f(a()))) -> mark(c(f(g(f(a()))))) 650.31/295.37 Qed 650.31/295.37 EOF