YES(?,O(n^2)) 732.95/295.36 YES(?,O(n^2)) 732.95/295.36 732.95/295.36 Problem: 732.95/295.36 active(f(f(X))) -> mark(c(f(g(f(X))))) 732.95/295.36 active(c(X)) -> mark(d(X)) 732.95/295.36 active(h(X)) -> mark(c(d(X))) 732.95/295.36 mark(f(X)) -> active(f(mark(X))) 732.95/295.36 mark(c(X)) -> active(c(X)) 732.95/295.36 mark(g(X)) -> active(g(X)) 732.95/295.36 mark(d(X)) -> active(d(X)) 732.95/295.36 mark(h(X)) -> active(h(mark(X))) 732.95/295.36 f(mark(X)) -> f(X) 732.95/295.36 f(active(X)) -> f(X) 732.95/295.36 c(mark(X)) -> c(X) 732.95/295.36 c(active(X)) -> c(X) 732.95/295.36 g(mark(X)) -> g(X) 732.95/295.36 g(active(X)) -> g(X) 732.95/295.36 d(mark(X)) -> d(X) 732.95/295.36 d(active(X)) -> d(X) 732.95/295.36 h(mark(X)) -> h(X) 732.95/295.36 h(active(X)) -> h(X) 732.95/295.36 732.95/295.36 Proof: 732.95/295.36 Complexity Transformation Processor: 732.95/295.36 strict: 732.95/295.36 active(f(f(X))) -> mark(c(f(g(f(X))))) 732.95/295.36 active(c(X)) -> mark(d(X)) 732.95/295.36 active(h(X)) -> mark(c(d(X))) 732.95/295.36 mark(f(X)) -> active(f(mark(X))) 732.95/295.36 mark(c(X)) -> active(c(X)) 732.95/295.36 mark(g(X)) -> active(g(X)) 732.95/295.36 mark(d(X)) -> active(d(X)) 732.95/295.36 mark(h(X)) -> active(h(mark(X))) 732.95/295.36 f(mark(X)) -> f(X) 732.95/295.36 f(active(X)) -> f(X) 732.95/295.36 c(mark(X)) -> c(X) 732.95/295.36 c(active(X)) -> c(X) 732.95/295.36 g(mark(X)) -> g(X) 732.95/295.36 g(active(X)) -> g(X) 732.95/295.36 d(mark(X)) -> d(X) 732.95/295.36 d(active(X)) -> d(X) 732.95/295.36 h(mark(X)) -> h(X) 732.95/295.36 h(active(X)) -> h(X) 732.95/295.36 weak: 732.95/295.36 732.95/295.36 Matrix Interpretation Processor: dim=1 732.95/295.36 732.95/295.36 max_matrix: 732.95/295.36 1 732.95/295.36 interpretation: 732.95/295.36 [h](x0) = x0 + 6, 732.95/295.36 732.95/295.36 [d](x0) = x0, 732.95/295.36 732.95/295.36 [mark](x0) = x0 + 1, 732.95/295.36 732.95/295.36 [c](x0) = x0, 732.95/295.36 732.95/295.36 [g](x0) = x0 + 10, 732.95/295.36 732.95/295.36 [active](x0) = x0 + 20, 732.95/295.36 732.95/295.36 [f](x0) = x0 + 4 732.95/295.36 orientation: 732.95/295.36 active(f(f(X))) = X + 28 >= X + 19 = mark(c(f(g(f(X))))) 732.95/295.36 732.95/295.36 active(c(X)) = X + 20 >= X + 1 = mark(d(X)) 732.95/295.36 732.95/295.36 active(h(X)) = X + 26 >= X + 1 = mark(c(d(X))) 732.95/295.36 732.95/295.36 mark(f(X)) = X + 5 >= X + 25 = active(f(mark(X))) 732.95/295.36 732.95/295.36 mark(c(X)) = X + 1 >= X + 20 = active(c(X)) 732.95/295.36 732.95/295.36 mark(g(X)) = X + 11 >= X + 30 = active(g(X)) 732.95/295.36 732.95/295.36 mark(d(X)) = X + 1 >= X + 20 = active(d(X)) 732.95/295.36 732.95/295.36 mark(h(X)) = X + 7 >= X + 27 = active(h(mark(X))) 732.95/295.36 732.95/295.36 f(mark(X)) = X + 5 >= X + 4 = f(X) 732.95/295.36 732.95/295.36 f(active(X)) = X + 24 >= X + 4 = f(X) 732.95/295.36 732.95/295.36 c(mark(X)) = X + 1 >= X = c(X) 732.95/295.36 732.95/295.36 c(active(X)) = X + 20 >= X = c(X) 732.95/295.36 732.95/295.36 g(mark(X)) = X + 11 >= X + 10 = g(X) 732.95/295.36 732.95/295.36 g(active(X)) = X + 30 >= X + 10 = g(X) 732.95/295.36 732.95/295.36 d(mark(X)) = X + 1 >= X = d(X) 732.95/295.36 732.95/295.36 d(active(X)) = X + 20 >= X = d(X) 732.95/295.36 732.95/295.36 h(mark(X)) = X + 7 >= X + 6 = h(X) 732.95/295.36 732.95/295.36 h(active(X)) = X + 26 >= X + 6 = h(X) 732.95/295.36 problem: 732.95/295.36 strict: 732.95/295.36 mark(f(X)) -> active(f(mark(X))) 732.95/295.36 mark(c(X)) -> active(c(X)) 732.95/295.36 mark(g(X)) -> active(g(X)) 732.95/295.36 mark(d(X)) -> active(d(X)) 732.95/295.36 mark(h(X)) -> active(h(mark(X))) 732.95/295.36 weak: 732.95/295.36 active(f(f(X))) -> mark(c(f(g(f(X))))) 732.95/295.36 active(c(X)) -> mark(d(X)) 732.95/295.36 active(h(X)) -> mark(c(d(X))) 732.95/295.36 f(mark(X)) -> f(X) 732.95/295.36 f(active(X)) -> f(X) 732.95/295.36 c(mark(X)) -> c(X) 732.95/295.36 c(active(X)) -> c(X) 732.95/295.36 g(mark(X)) -> g(X) 732.95/295.36 g(active(X)) -> g(X) 732.95/295.36 d(mark(X)) -> d(X) 732.95/295.36 d(active(X)) -> d(X) 732.95/295.36 h(mark(X)) -> h(X) 732.95/295.36 h(active(X)) -> h(X) 732.95/295.36 Matrix Interpretation Processor: dim=3 732.95/295.36 732.95/295.36 max_matrix: 732.95/295.36 [1 0 1] 732.95/295.36 [0 0 0] 732.95/295.36 [0 0 0] 732.95/295.36 interpretation: 732.95/295.36 [1 0 1] [1] 732.95/295.36 [h](x0) = [0 0 0]x0 + [0] 732.95/295.36 [0 0 0] [1], 732.95/295.36 732.95/295.36 [1 0 0] 732.95/295.36 [d](x0) = [0 0 0]x0 732.95/295.36 [0 0 0] , 732.95/295.36 732.95/295.36 [1 0 1] [1] 732.95/295.36 [mark](x0) = [0 0 0]x0 + [0] 732.95/295.36 [0 0 0] [0], 732.95/295.36 732.95/295.36 [1 0 0] [0] 732.95/295.36 [c](x0) = [0 0 0]x0 + [0] 732.95/295.36 [0 0 0] [1], 732.95/295.36 732.95/295.36 [1 0 0] 732.95/295.36 [g](x0) = [0 0 0]x0 732.95/295.36 [0 0 0] , 732.95/295.36 732.95/295.36 [1 0 1] 732.95/295.36 [active](x0) = [0 0 0]x0 732.95/295.36 [0 0 0] , 732.95/295.36 732.95/295.36 [1 0 1] [0] 732.95/295.36 [f](x0) = [0 0 0]x0 + [0] 732.95/295.36 [0 0 0] [1] 732.95/295.36 orientation: 732.95/295.36 [1 0 1] [2] [1 0 1] [2] 732.95/295.36 mark(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(f(mark(X))) 732.95/295.36 [0 0 0] [0] [0 0 0] [0] 732.95/295.36 732.95/295.36 [1 0 0] [2] [1 0 0] [1] 732.95/295.36 mark(c(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(c(X)) 732.95/295.36 [0 0 0] [0] [0 0 0] [0] 732.95/295.36 732.95/295.36 [1 0 0] [1] [1 0 0] 732.95/295.36 mark(g(X)) = [0 0 0]X + [0] >= [0 0 0]X = active(g(X)) 732.95/295.37 [0 0 0] [0] [0 0 0] 732.95/295.37 732.95/295.37 [1 0 0] [1] [1 0 0] 732.95/295.37 mark(d(X)) = [0 0 0]X + [0] >= [0 0 0]X = active(d(X)) 732.95/295.37 [0 0 0] [0] [0 0 0] 732.95/295.37 732.95/295.37 [1 0 1] [3] [1 0 1] [3] 732.95/295.37 mark(h(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(h(mark(X))) 732.95/295.37 [0 0 0] [0] [0 0 0] [0] 732.95/295.37 732.95/295.37 [1 0 1] [2] [1 0 1] [2] 732.95/295.37 active(f(f(X))) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(c(f(g(f(X))))) 732.95/295.37 [0 0 0] [0] [0 0 0] [0] 732.95/295.37 732.95/295.37 [1 0 0] [1] [1 0 0] [1] 732.95/295.37 active(c(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(d(X)) 732.95/295.37 [0 0 0] [0] [0 0 0] [0] 732.95/295.37 732.95/295.37 [1 0 1] [2] [1 0 0] [2] 732.95/295.37 active(h(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(c(d(X))) 732.95/295.37 [0 0 0] [0] [0 0 0] [0] 732.95/295.37 732.95/295.37 [1 0 1] [1] [1 0 1] [0] 732.95/295.37 f(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(X) 732.95/295.37 [0 0 0] [1] [0 0 0] [1] 732.95/295.37 732.95/295.37 [1 0 1] [0] [1 0 1] [0] 732.95/295.37 f(active(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(X) 732.95/295.37 [0 0 0] [1] [0 0 0] [1] 732.95/295.37 732.95/295.37 [1 0 1] [1] [1 0 0] [0] 732.95/295.37 c(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = c(X) 732.95/295.37 [0 0 0] [1] [0 0 0] [1] 732.95/295.37 732.95/295.37 [1 0 1] [0] [1 0 0] [0] 732.95/295.37 c(active(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = c(X) 732.95/295.37 [0 0 0] [1] [0 0 0] [1] 732.95/295.37 732.95/295.37 [1 0 1] [1] [1 0 0] 732.95/295.37 g(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X = g(X) 732.95/295.37 [0 0 0] [0] [0 0 0] 732.95/295.37 732.95/295.37 [1 0 1] [1 0 0] 732.95/295.37 g(active(X)) = [0 0 0]X >= [0 0 0]X = g(X) 732.95/295.37 [0 0 0] [0 0 0] 732.95/295.37 732.95/295.37 [1 0 1] [1] [1 0 0] 732.95/295.37 d(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X = d(X) 732.95/295.37 [0 0 0] [0] [0 0 0] 732.95/295.37 732.95/295.37 [1 0 1] [1 0 0] 732.95/295.37 d(active(X)) = [0 0 0]X >= [0 0 0]X = d(X) 732.95/295.37 [0 0 0] [0 0 0] 732.95/295.37 732.95/295.37 [1 0 1] [2] [1 0 1] [1] 732.95/295.37 h(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = h(X) 732.95/295.37 [0 0 0] [1] [0 0 0] [1] 732.95/295.37 732.95/295.37 [1 0 1] [1] [1 0 1] [1] 732.95/295.37 h(active(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = h(X) 732.95/295.37 [0 0 0] [1] [0 0 0] [1] 732.95/295.37 problem: 732.95/295.37 strict: 732.95/295.37 mark(f(X)) -> active(f(mark(X))) 732.95/295.37 mark(h(X)) -> active(h(mark(X))) 732.95/295.37 weak: 732.95/295.37 mark(c(X)) -> active(c(X)) 732.95/295.37 mark(g(X)) -> active(g(X)) 732.95/295.37 mark(d(X)) -> active(d(X)) 732.95/295.37 active(f(f(X))) -> mark(c(f(g(f(X))))) 732.95/295.37 active(c(X)) -> mark(d(X)) 732.95/295.37 active(h(X)) -> mark(c(d(X))) 732.95/295.37 f(mark(X)) -> f(X) 732.95/295.37 f(active(X)) -> f(X) 732.95/295.37 c(mark(X)) -> c(X) 732.95/295.37 c(active(X)) -> c(X) 732.95/295.37 g(mark(X)) -> g(X) 732.95/295.37 g(active(X)) -> g(X) 732.95/295.37 d(mark(X)) -> d(X) 732.95/295.37 d(active(X)) -> d(X) 732.95/295.37 h(mark(X)) -> h(X) 732.95/295.37 h(active(X)) -> h(X) 732.95/295.37 Splitting Processor: 732.95/295.37 strict: 732.95/295.37 mark(h(X)) -> active(h(mark(X))) 732.95/295.37 weak: 732.95/295.37 mark(c(X)) -> active(c(X)) 732.95/295.37 mark(g(X)) -> active(g(X)) 732.95/295.37 mark(d(X)) -> active(d(X)) 732.95/295.37 active(f(f(X))) -> mark(c(f(g(f(X))))) 732.95/295.37 active(c(X)) -> mark(d(X)) 732.95/295.37 active(h(X)) -> mark(c(d(X))) 732.95/295.37 f(mark(X)) -> f(X) 732.95/295.37 f(active(X)) -> f(X) 732.95/295.37 c(mark(X)) -> c(X) 732.95/295.37 c(active(X)) -> c(X) 732.95/295.37 g(mark(X)) -> g(X) 732.95/295.37 g(active(X)) -> g(X) 732.95/295.37 d(mark(X)) -> d(X) 732.95/295.37 d(active(X)) -> d(X) 732.95/295.37 h(mark(X)) -> h(X) 732.95/295.37 h(active(X)) -> h(X) 732.95/295.37 mark(f(X)) -> active(f(mark(X))) 732.95/295.37 Matrix Interpretation Processor: dim=3 732.95/295.38 732.95/295.38 max_matrix: 732.95/295.38 [1 1 1] 732.95/295.38 [0 1 1] 732.95/295.38 [0 0 0] 732.95/295.38 interpretation: 732.95/295.38 [1 0 1] [1] 732.95/295.38 [h](x0) = [0 1 0]x0 + [1] 732.95/295.38 [0 0 0] [0], 732.95/295.38 732.95/295.38 [1 0 1] 732.95/295.38 [d](x0) = [0 0 0]x0 732.95/295.38 [0 0 0] , 732.95/295.38 732.95/295.38 [1 1 1] 732.95/295.38 [mark](x0) = [0 1 0]x0 732.95/295.38 [0 0 0] , 732.95/295.38 732.95/295.38 [1 0 1] 732.95/295.38 [c](x0) = [0 0 0]x0 732.95/295.38 [0 0 0] , 732.95/295.38 732.95/295.38 [1 0 1] 732.95/295.38 [g](x0) = [0 0 0]x0 732.95/295.38 [0 0 0] , 732.95/295.38 732.95/295.38 [1 0 1] 732.95/295.38 [active](x0) = [0 1 1]x0 732.95/295.38 [0 0 0] , 732.95/295.38 732.95/295.38 [1 0 1] [0] 732.95/295.38 [f](x0) = [0 1 0]x0 + [1] 732.95/295.38 [0 0 0] [0] 732.95/295.38 orientation: 732.95/295.38 [1 1 1] [1] [1 1 1] [0] 732.95/295.38 mark(f(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = active(f(mark(X))) 732.95/295.38 [0 0 0] [0] [0 0 0] [0] 732.95/295.38 732.95/295.38 [1 1 1] [2] [1 1 1] [1] 732.95/295.38 mark(h(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = active(h(mark(X))) 732.95/295.38 [0 0 0] [0] [0 0 0] [0] 732.95/295.38 732.95/295.38 [1 0 1] [1 0 1] 732.95/295.38 mark(c(X)) = [0 0 0]X >= [0 0 0]X = active(c(X)) 732.95/295.38 [0 0 0] [0 0 0] 732.95/295.38 732.95/295.38 [1 0 1] [1 0 1] 732.95/295.38 mark(g(X)) = [0 0 0]X >= [0 0 0]X = active(g(X)) 732.95/295.38 [0 0 0] [0 0 0] 732.95/295.38 732.95/295.38 [1 0 1] [1 0 1] 732.95/295.38 mark(d(X)) = [0 0 0]X >= [0 0 0]X = active(d(X)) 732.95/295.38 [0 0 0] [0 0 0] 732.95/295.38 732.95/295.38 [1 0 1] [0] [1 0 1] 732.95/295.38 active(f(f(X))) = [0 1 0]X + [2] >= [0 0 0]X = mark(c(f(g(f(X))))) 732.95/295.38 [0 0 0] [0] [0 0 0] 732.95/295.38 732.95/295.38 [1 0 1] [1 0 1] 732.95/295.38 active(c(X)) = [0 0 0]X >= [0 0 0]X = mark(d(X)) 732.95/295.38 [0 0 0] [0 0 0] 732.95/295.38 732.95/295.38 [1 0 1] [1] [1 0 1] 732.95/295.38 active(h(X)) = [0 1 0]X + [1] >= [0 0 0]X = mark(c(d(X))) 732.95/295.38 [0 0 0] [0] [0 0 0] 732.95/295.38 732.95/295.38 [1 1 1] [0] [1 0 1] [0] 732.95/295.38 f(mark(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = f(X) 732.95/295.38 [0 0 0] [0] [0 0 0] [0] 732.95/295.38 732.95/295.38 [1 0 1] [0] [1 0 1] [0] 732.95/295.38 f(active(X)) = [0 1 1]X + [1] >= [0 1 0]X + [1] = f(X) 732.95/295.38 [0 0 0] [0] [0 0 0] [0] 732.95/295.38 732.95/295.38 [1 1 1] [1 0 1] 732.95/295.38 c(mark(X)) = [0 0 0]X >= [0 0 0]X = c(X) 732.95/295.38 [0 0 0] [0 0 0] 732.95/295.38 732.95/295.38 [1 0 1] [1 0 1] 732.95/295.38 c(active(X)) = [0 0 0]X >= [0 0 0]X = c(X) 732.95/295.38 [0 0 0] [0 0 0] 732.95/295.38 732.95/295.38 [1 1 1] [1 0 1] 732.95/295.38 g(mark(X)) = [0 0 0]X >= [0 0 0]X = g(X) 732.95/295.38 [0 0 0] [0 0 0] 732.95/295.38 732.95/295.38 [1 0 1] [1 0 1] 732.95/295.38 g(active(X)) = [0 0 0]X >= [0 0 0]X = g(X) 732.95/295.38 [0 0 0] [0 0 0] 732.95/295.38 732.95/295.38 [1 1 1] [1 0 1] 732.95/295.38 d(mark(X)) = [0 0 0]X >= [0 0 0]X = d(X) 732.95/295.38 [0 0 0] [0 0 0] 732.95/295.38 732.95/295.38 [1 0 1] [1 0 1] 732.95/295.38 d(active(X)) = [0 0 0]X >= [0 0 0]X = d(X) 732.95/295.38 [0 0 0] [0 0 0] 732.95/295.38 732.95/295.38 [1 1 1] [1] [1 0 1] [1] 732.95/295.38 h(mark(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = h(X) 732.95/295.38 [0 0 0] [0] [0 0 0] [0] 732.95/295.38 732.95/295.38 [1 0 1] [1] [1 0 1] [1] 732.95/295.38 h(active(X)) = [0 1 1]X + [1] >= [0 1 0]X + [1] = h(X) 732.95/295.38 [0 0 0] [0] [0 0 0] [0] 732.95/295.38 problem: 732.95/295.38 strict: 732.95/295.38 732.95/295.38 weak: 732.95/295.38 mark(f(X)) -> active(f(mark(X))) 732.95/295.38 mark(h(X)) -> active(h(mark(X))) 732.95/295.38 mark(c(X)) -> active(c(X)) 732.95/295.38 mark(g(X)) -> active(g(X)) 732.95/295.38 mark(d(X)) -> active(d(X)) 732.95/295.38 active(f(f(X))) -> mark(c(f(g(f(X))))) 732.95/295.38 active(c(X)) -> mark(d(X)) 732.95/295.38 active(h(X)) -> mark(c(d(X))) 732.95/295.38 f(mark(X)) -> f(X) 732.95/295.38 f(active(X)) -> f(X) 732.95/295.38 c(mark(X)) -> c(X) 732.95/295.38 c(active(X)) -> c(X) 732.95/295.38 g(mark(X)) -> g(X) 732.95/295.38 g(active(X)) -> g(X) 732.95/295.38 d(mark(X)) -> d(X) 732.95/295.38 d(active(X)) -> d(X) 732.95/295.38 h(mark(X)) -> h(X) 732.95/295.38 h(active(X)) -> h(X) 732.95/295.38 Qed 732.95/295.38 732.95/295.38 strict: 732.95/295.38 mark(f(X)) -> active(f(mark(X))) 732.95/295.38 weak: 732.95/295.38 mark(h(X)) -> active(h(mark(X))) 732.95/295.38 mark(c(X)) -> active(c(X)) 732.95/295.38 mark(g(X)) -> active(g(X)) 732.95/295.38 mark(d(X)) -> active(d(X)) 732.95/295.38 active(f(f(X))) -> mark(c(f(g(f(X))))) 732.95/295.38 active(c(X)) -> mark(d(X)) 732.95/295.38 active(h(X)) -> mark(c(d(X))) 732.95/295.38 f(mark(X)) -> f(X) 732.95/295.38 f(active(X)) -> f(X) 732.95/295.38 c(mark(X)) -> c(X) 732.95/295.38 c(active(X)) -> c(X) 732.95/295.38 g(mark(X)) -> g(X) 732.95/295.38 g(active(X)) -> g(X) 732.95/295.38 d(mark(X)) -> d(X) 732.95/295.38 d(active(X)) -> d(X) 732.95/295.38 h(mark(X)) -> h(X) 732.95/295.38 h(active(X)) -> h(X) 732.95/295.38 Matrix Interpretation Processor: dim=3 732.95/295.38 732.95/295.38 max_matrix: 732.95/295.38 [1 1 1] 732.95/295.38 [0 0 0] 732.95/295.38 [0 0 1] 732.95/295.38 interpretation: 732.95/295.38 [1 0 0] [1] 732.95/295.38 [h](x0) = [0 0 0]x0 + [0] 732.95/295.38 [0 0 1] [1], 732.95/295.38 732.95/295.38 [1 0 0] [0] 732.95/295.38 [d](x0) = [0 0 0]x0 + [1] 732.95/295.38 [0 0 0] [0], 732.95/295.38 732.95/295.38 [1 0 1] [1] 732.95/295.38 [mark](x0) = [0 0 0]x0 + [0] 732.95/295.38 [0 0 1] [0], 732.95/295.38 732.95/295.38 [1 0 0] [0] 732.95/295.38 [c](x0) = [0 0 0]x0 + [1] 732.95/295.38 [0 0 0] [0], 732.95/295.38 732.95/295.38 [1 0 0] 732.95/295.38 [g](x0) = [0 0 0]x0 732.95/295.38 [0 0 0] , 732.95/295.38 732.95/295.38 [1 1 0] 732.95/295.38 [active](x0) = [0 0 0]x0 732.95/295.38 [0 0 1] , 732.95/295.38 732.95/295.38 [1 0 0] [0] 732.95/295.38 [f](x0) = [0 0 0]x0 + [1] 732.95/295.38 [0 0 1] [1] 732.95/295.38 orientation: 732.95/295.38 [1 0 1] [3] [1 0 1] [2] 732.95/295.38 mark(h(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(h(mark(X))) 732.95/295.38 [0 0 1] [1] [0 0 1] [1] 732.95/295.38 732.95/295.38 [1 0 0] [1] [1 0 0] [1] 732.95/295.38 mark(c(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(c(X)) 732.95/295.38 [0 0 0] [0] [0 0 0] [0] 732.95/295.38 732.95/295.38 [1 0 0] [1] [1 0 0] 732.95/295.38 mark(g(X)) = [0 0 0]X + [0] >= [0 0 0]X = active(g(X)) 732.95/295.38 [0 0 0] [0] [0 0 0] 732.95/295.38 732.95/295.38 [1 0 0] [1] [1 0 0] [1] 732.95/295.38 mark(d(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(d(X)) 732.95/295.38 [0 0 0] [0] [0 0 0] [0] 732.95/295.38 732.95/295.38 [1 0 0] [1] [1 0 0] [1] 732.95/295.38 active(f(f(X))) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(c(f(g(f(X))))) 732.95/295.38 [0 0 1] [2] [0 0 0] [0] 732.95/295.38 732.95/295.38 [1 0 0] [1] [1 0 0] [1] 732.95/295.38 active(c(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(d(X)) 732.95/295.38 [0 0 0] [0] [0 0 0] [0] 732.95/295.38 732.95/295.38 [1 0 0] [1] [1 0 0] [1] 732.95/295.38 active(h(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(c(d(X))) 732.95/295.38 [0 0 1] [1] [0 0 0] [0] 732.95/295.38 732.95/295.38 [1 0 1] [1] [1 0 0] [0] 732.95/295.38 f(mark(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = f(X) 732.95/295.38 [0 0 1] [1] [0 0 1] [1] 732.95/295.38 732.95/295.38 [1 1 0] [0] [1 0 0] [0] 732.95/295.38 f(active(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = f(X) 732.95/295.38 [0 0 1] [1] [0 0 1] [1] 732.95/295.38 732.95/295.38 [1 0 1] [1] [1 0 0] [0] 732.95/295.38 c(mark(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = c(X) 732.95/295.39 [0 0 0] [0] [0 0 0] [0] 732.95/295.39 732.95/295.39 [1 1 0] [0] [1 0 0] [0] 732.95/295.39 c(active(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = c(X) 732.95/295.39 [0 0 0] [0] [0 0 0] [0] 732.95/295.39 732.95/295.39 [1 0 1] [1] [1 0 0] 732.95/295.39 g(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X = g(X) 732.95/295.39 [0 0 0] [0] [0 0 0] 732.95/295.39 732.95/295.39 [1 1 0] [1 0 0] 732.95/295.39 g(active(X)) = [0 0 0]X >= [0 0 0]X = g(X) 732.95/295.39 [0 0 0] [0 0 0] 732.95/295.39 732.95/295.39 [1 0 1] [1] [1 0 0] [0] 732.95/295.39 d(mark(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = d(X) 732.95/295.39 [0 0 0] [0] [0 0 0] [0] 732.95/295.39 732.95/295.39 [1 1 0] [0] [1 0 0] [0] 732.95/295.39 d(active(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = d(X) 732.95/295.39 [0 0 0] [0] [0 0 0] [0] 732.95/295.39 732.95/295.39 [1 0 1] [2] [1 0 0] [1] 732.95/295.39 h(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = h(X) 732.95/295.39 [0 0 1] [1] [0 0 1] [1] 732.95/295.39 732.95/295.39 [1 1 0] [1] [1 0 0] [1] 732.95/295.39 h(active(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = h(X) 732.95/295.39 [0 0 1] [1] [0 0 1] [1] 732.95/295.39 732.95/295.39 [1 0 1] [2] [1 0 1] [2] 732.95/295.39 mark(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(f(mark(X))) 732.95/295.39 [0 0 1] [1] [0 0 1] [1] 732.95/295.39 problem: 732.95/295.39 strict: 732.95/295.39 732.95/295.39 weak: 732.95/295.39 mark(h(X)) -> active(h(mark(X))) 732.95/295.39 mark(c(X)) -> active(c(X)) 732.95/295.39 mark(g(X)) -> active(g(X)) 732.95/295.39 mark(d(X)) -> active(d(X)) 732.95/295.39 active(f(f(X))) -> mark(c(f(g(f(X))))) 732.95/295.39 active(c(X)) -> mark(d(X)) 732.95/295.39 active(h(X)) -> mark(c(d(X))) 732.95/295.39 f(mark(X)) -> f(X) 732.95/295.39 f(active(X)) -> f(X) 732.95/295.39 c(mark(X)) -> c(X) 732.95/295.39 c(active(X)) -> c(X) 732.95/295.39 g(mark(X)) -> g(X) 732.95/295.39 g(active(X)) -> g(X) 732.95/295.39 d(mark(X)) -> d(X) 732.95/295.39 d(active(X)) -> d(X) 732.95/295.39 h(mark(X)) -> h(X) 732.95/295.39 h(active(X)) -> h(X) 732.95/295.39 mark(f(X)) -> active(f(mark(X))) 732.95/295.39 Qed 732.95/295.39 EOF