YES(?,O(n^2)) 553.53/176.46 YES(?,O(n^2)) 553.53/176.46 553.53/176.46 Problem: 553.53/176.46 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.53/176.46 active(c(X)) -> mark(d(X)) 553.53/176.46 active(h(X)) -> mark(c(d(X))) 553.53/176.46 active(f(X)) -> f(active(X)) 553.53/176.46 active(h(X)) -> h(active(X)) 553.53/176.46 f(mark(X)) -> mark(f(X)) 553.53/176.46 h(mark(X)) -> mark(h(X)) 553.53/176.46 proper(f(X)) -> f(proper(X)) 553.53/176.46 proper(c(X)) -> c(proper(X)) 553.53/176.46 proper(g(X)) -> g(proper(X)) 553.53/176.46 proper(d(X)) -> d(proper(X)) 553.53/176.46 proper(h(X)) -> h(proper(X)) 553.53/176.46 f(ok(X)) -> ok(f(X)) 553.53/176.46 c(ok(X)) -> ok(c(X)) 553.53/176.46 g(ok(X)) -> ok(g(X)) 553.53/176.46 d(ok(X)) -> ok(d(X)) 553.53/176.46 h(ok(X)) -> ok(h(X)) 553.53/176.46 top(mark(X)) -> top(proper(X)) 553.53/176.46 top(ok(X)) -> top(active(X)) 553.53/176.46 553.53/176.46 Proof: 553.53/176.46 Complexity Transformation Processor: 553.53/176.46 strict: 553.53/176.46 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.53/176.46 active(c(X)) -> mark(d(X)) 553.53/176.46 active(h(X)) -> mark(c(d(X))) 553.53/176.46 active(f(X)) -> f(active(X)) 553.53/176.46 active(h(X)) -> h(active(X)) 553.53/176.46 f(mark(X)) -> mark(f(X)) 553.53/176.46 h(mark(X)) -> mark(h(X)) 553.53/176.46 proper(f(X)) -> f(proper(X)) 553.53/176.46 proper(c(X)) -> c(proper(X)) 553.53/176.46 proper(g(X)) -> g(proper(X)) 553.53/176.46 proper(d(X)) -> d(proper(X)) 553.53/176.46 proper(h(X)) -> h(proper(X)) 553.53/176.46 f(ok(X)) -> ok(f(X)) 553.53/176.46 c(ok(X)) -> ok(c(X)) 553.53/176.46 g(ok(X)) -> ok(g(X)) 553.53/176.46 d(ok(X)) -> ok(d(X)) 553.53/176.46 h(ok(X)) -> ok(h(X)) 553.53/176.46 top(mark(X)) -> top(proper(X)) 553.53/176.46 top(ok(X)) -> top(active(X)) 553.53/176.46 weak: 553.53/176.46 553.53/176.46 Matrix Interpretation Processor: dim=1 553.53/176.46 553.53/176.46 max_matrix: 553.53/176.46 1 553.53/176.46 interpretation: 553.53/176.46 [top](x0) = x0 + 202, 553.53/176.46 553.53/176.46 [ok](x0) = x0 + 229, 553.53/176.46 553.53/176.46 [proper](x0) = x0 + 45, 553.53/176.46 553.53/176.46 [h](x0) = x0 + 176, 553.53/176.46 553.53/176.46 [d](x0) = x0 + 32, 553.53/176.46 553.53/176.46 [mark](x0) = x0 + 80, 553.53/176.46 553.53/176.46 [c](x0) = x0 + 146, 553.53/176.46 553.53/176.46 [g](x0) = x0 + 33, 553.53/176.46 553.53/176.46 [active](x0) = x0 + 216, 553.53/176.46 553.53/176.46 [f](x0) = x0 + 24 553.53/176.46 orientation: 553.53/176.46 active(f(f(X))) = X + 264 >= X + 307 = mark(c(f(g(f(X))))) 553.53/176.46 553.53/176.46 active(c(X)) = X + 362 >= X + 112 = mark(d(X)) 553.53/176.46 553.53/176.46 active(h(X)) = X + 392 >= X + 258 = mark(c(d(X))) 553.53/176.46 553.53/176.46 active(f(X)) = X + 240 >= X + 240 = f(active(X)) 553.53/176.46 553.53/176.46 active(h(X)) = X + 392 >= X + 392 = h(active(X)) 553.53/176.46 553.53/176.46 f(mark(X)) = X + 104 >= X + 104 = mark(f(X)) 553.53/176.46 553.53/176.46 h(mark(X)) = X + 256 >= X + 256 = mark(h(X)) 553.53/176.46 553.53/176.46 proper(f(X)) = X + 69 >= X + 69 = f(proper(X)) 553.53/176.46 553.53/176.46 proper(c(X)) = X + 191 >= X + 191 = c(proper(X)) 553.53/176.46 553.53/176.46 proper(g(X)) = X + 78 >= X + 78 = g(proper(X)) 553.53/176.46 553.53/176.46 proper(d(X)) = X + 77 >= X + 77 = d(proper(X)) 553.53/176.46 553.53/176.46 proper(h(X)) = X + 221 >= X + 221 = h(proper(X)) 553.53/176.46 553.53/176.46 f(ok(X)) = X + 253 >= X + 253 = ok(f(X)) 553.53/176.46 553.53/176.46 c(ok(X)) = X + 375 >= X + 375 = ok(c(X)) 553.53/176.46 553.53/176.46 g(ok(X)) = X + 262 >= X + 262 = ok(g(X)) 553.53/176.46 553.53/176.46 d(ok(X)) = X + 261 >= X + 261 = ok(d(X)) 553.53/176.46 553.53/176.46 h(ok(X)) = X + 405 >= X + 405 = ok(h(X)) 553.53/176.46 553.53/176.46 top(mark(X)) = X + 282 >= X + 247 = top(proper(X)) 553.53/176.46 553.53/176.46 top(ok(X)) = X + 431 >= X + 418 = top(active(X)) 553.53/176.46 problem: 553.53/176.46 strict: 553.53/176.46 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.53/176.46 active(f(X)) -> f(active(X)) 553.53/176.46 active(h(X)) -> h(active(X)) 553.53/176.46 f(mark(X)) -> mark(f(X)) 553.53/176.46 h(mark(X)) -> mark(h(X)) 553.53/176.46 proper(f(X)) -> f(proper(X)) 553.53/176.46 proper(c(X)) -> c(proper(X)) 553.53/176.46 proper(g(X)) -> g(proper(X)) 553.53/176.46 proper(d(X)) -> d(proper(X)) 553.53/176.46 proper(h(X)) -> h(proper(X)) 553.53/176.46 f(ok(X)) -> ok(f(X)) 553.53/176.46 c(ok(X)) -> ok(c(X)) 553.53/176.46 g(ok(X)) -> ok(g(X)) 553.53/176.46 d(ok(X)) -> ok(d(X)) 553.53/176.46 h(ok(X)) -> ok(h(X)) 553.53/176.46 weak: 553.53/176.46 active(c(X)) -> mark(d(X)) 553.53/176.46 active(h(X)) -> mark(c(d(X))) 553.53/176.46 top(mark(X)) -> top(proper(X)) 553.53/176.46 top(ok(X)) -> top(active(X)) 553.53/176.46 Matrix Interpretation Processor: dim=1 553.53/176.46 553.53/176.46 max_matrix: 553.53/176.46 1 553.53/176.46 interpretation: 553.53/176.46 [top](x0) = x0, 553.53/176.46 553.53/176.46 [ok](x0) = x0 + 4, 553.53/176.46 553.53/176.46 [proper](x0) = x0, 553.53/176.46 553.53/176.46 [h](x0) = x0, 553.53/176.46 553.53/176.46 [d](x0) = x0 + 2, 553.53/176.46 553.53/176.46 [mark](x0) = x0, 553.53/176.46 553.53/176.46 [c](x0) = x0 + 2, 553.53/176.46 553.53/176.46 [g](x0) = x0, 553.53/176.46 553.53/176.46 [active](x0) = x0 + 4, 553.53/176.46 553.53/176.46 [f](x0) = x0 553.53/176.46 orientation: 553.53/176.46 active(f(f(X))) = X + 4 >= X + 2 = mark(c(f(g(f(X))))) 553.53/176.46 553.53/176.46 active(f(X)) = X + 4 >= X + 4 = f(active(X)) 553.53/176.46 553.53/176.46 active(h(X)) = X + 4 >= X + 4 = h(active(X)) 553.53/176.46 553.53/176.46 f(mark(X)) = X >= X = mark(f(X)) 553.53/176.46 553.53/176.46 h(mark(X)) = X >= X = mark(h(X)) 553.53/176.46 553.53/176.46 proper(f(X)) = X >= X = f(proper(X)) 553.53/176.46 553.53/176.46 proper(c(X)) = X + 2 >= X + 2 = c(proper(X)) 553.53/176.46 553.53/176.46 proper(g(X)) = X >= X = g(proper(X)) 553.53/176.46 553.53/176.46 proper(d(X)) = X + 2 >= X + 2 = d(proper(X)) 553.53/176.47 553.53/176.47 proper(h(X)) = X >= X = h(proper(X)) 553.53/176.47 553.53/176.47 f(ok(X)) = X + 4 >= X + 4 = ok(f(X)) 553.53/176.47 553.53/176.47 c(ok(X)) = X + 6 >= X + 6 = ok(c(X)) 553.53/176.47 553.53/176.47 g(ok(X)) = X + 4 >= X + 4 = ok(g(X)) 553.53/176.47 553.53/176.47 d(ok(X)) = X + 6 >= X + 6 = ok(d(X)) 553.53/176.47 553.53/176.47 h(ok(X)) = X + 4 >= X + 4 = ok(h(X)) 553.53/176.47 553.53/176.47 active(c(X)) = X + 6 >= X + 2 = mark(d(X)) 553.53/176.47 553.53/176.47 active(h(X)) = X + 4 >= X + 4 = mark(c(d(X))) 553.53/176.47 553.53/176.47 top(mark(X)) = X >= X = top(proper(X)) 553.53/176.47 553.53/176.47 top(ok(X)) = X + 4 >= X + 4 = top(active(X)) 553.53/176.47 problem: 553.53/176.47 strict: 553.53/176.47 active(f(X)) -> f(active(X)) 553.53/176.47 active(h(X)) -> h(active(X)) 553.53/176.47 f(mark(X)) -> mark(f(X)) 553.53/176.47 h(mark(X)) -> mark(h(X)) 553.53/176.47 proper(f(X)) -> f(proper(X)) 553.53/176.47 proper(c(X)) -> c(proper(X)) 553.53/176.47 proper(g(X)) -> g(proper(X)) 553.53/176.47 proper(d(X)) -> d(proper(X)) 553.53/176.47 proper(h(X)) -> h(proper(X)) 553.53/176.47 f(ok(X)) -> ok(f(X)) 553.53/176.47 c(ok(X)) -> ok(c(X)) 553.53/176.47 g(ok(X)) -> ok(g(X)) 553.53/176.47 d(ok(X)) -> ok(d(X)) 553.53/176.47 h(ok(X)) -> ok(h(X)) 553.53/176.47 weak: 553.53/176.47 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.53/176.47 active(c(X)) -> mark(d(X)) 553.53/176.47 active(h(X)) -> mark(c(d(X))) 553.53/176.47 top(mark(X)) -> top(proper(X)) 553.53/176.47 top(ok(X)) -> top(active(X)) 553.53/176.47 Splitting Processor: 553.53/176.47 strict: 553.53/176.47 h(ok(X)) -> ok(h(X)) 553.53/176.47 weak: 553.53/176.47 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.53/176.47 active(c(X)) -> mark(d(X)) 553.53/176.47 active(h(X)) -> mark(c(d(X))) 553.53/176.47 top(mark(X)) -> top(proper(X)) 553.53/176.47 top(ok(X)) -> top(active(X)) 553.53/176.47 active(f(X)) -> f(active(X)) 553.53/176.47 active(h(X)) -> h(active(X)) 553.53/176.47 f(mark(X)) -> mark(f(X)) 553.53/176.47 h(mark(X)) -> mark(h(X)) 553.53/176.47 proper(f(X)) -> f(proper(X)) 553.53/176.47 proper(c(X)) -> c(proper(X)) 553.53/176.47 proper(g(X)) -> g(proper(X)) 553.53/176.47 proper(d(X)) -> d(proper(X)) 553.53/176.47 proper(h(X)) -> h(proper(X)) 553.53/176.47 f(ok(X)) -> ok(f(X)) 553.53/176.47 c(ok(X)) -> ok(c(X)) 553.53/176.47 g(ok(X)) -> ok(g(X)) 553.53/176.47 d(ok(X)) -> ok(d(X)) 553.53/176.47 Splitting Processor: 553.53/176.47 strict: 553.53/176.47 d(ok(X)) -> ok(d(X)) 553.53/176.47 weak: 553.53/176.47 h(ok(X)) -> ok(h(X)) 553.53/176.47 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.53/176.47 active(c(X)) -> mark(d(X)) 553.53/176.47 active(h(X)) -> mark(c(d(X))) 553.53/176.47 top(mark(X)) -> top(proper(X)) 553.53/176.47 top(ok(X)) -> top(active(X)) 553.53/176.47 active(f(X)) -> f(active(X)) 553.53/176.47 active(h(X)) -> h(active(X)) 553.53/176.47 f(mark(X)) -> mark(f(X)) 553.53/176.47 h(mark(X)) -> mark(h(X)) 553.53/176.47 proper(f(X)) -> f(proper(X)) 553.53/176.47 proper(c(X)) -> c(proper(X)) 553.53/176.47 proper(g(X)) -> g(proper(X)) 553.53/176.47 proper(d(X)) -> d(proper(X)) 553.53/176.47 proper(h(X)) -> h(proper(X)) 553.53/176.47 f(ok(X)) -> ok(f(X)) 553.53/176.47 c(ok(X)) -> ok(c(X)) 553.53/176.47 g(ok(X)) -> ok(g(X)) 553.53/176.47 Matrix Interpretation Processor: dim=3 553.53/176.47 553.53/176.47 max_matrix: 553.53/176.47 [1 1 0] 553.53/176.47 [0 1 0] 553.53/176.47 [0 0 0] 553.53/176.47 interpretation: 553.53/176.47 [1 1 0] [1] 553.53/176.47 [top](x0) = [0 1 0]x0 + [0] 553.53/176.47 [0 0 0] [0], 553.53/176.47 553.53/176.47 [1 0 0] [0] 553.53/176.47 [ok](x0) = [0 1 0]x0 + [1] 553.53/176.47 [0 0 0] [0], 553.53/176.47 553.53/176.47 [1 0 0] [0] 553.53/176.47 [proper](x0) = [0 0 0]x0 + [0] 553.53/176.47 [0 0 0] [1], 553.53/176.47 553.53/176.47 [1 0 0] [0] 553.53/176.47 [h](x0) = [0 1 0]x0 + [0] 553.53/176.47 [0 0 0] [1], 553.53/176.47 553.53/176.47 [1 1 0] 553.53/176.47 [d](x0) = [0 1 0]x0 553.53/176.47 [0 0 0] , 553.53/176.47 553.53/176.47 [1 0 0] 553.53/176.47 [mark](x0) = [0 0 0]x0 553.53/176.47 [0 0 0] , 553.53/176.47 553.53/176.47 [1 0 0] [1] 553.53/176.47 [c](x0) = [0 1 0]x0 + [0] 553.53/176.47 [0 0 0] [0], 553.53/176.47 553.53/176.47 [1 0 0] [0] 553.53/176.47 [g](x0) = [0 1 0]x0 + [0] 553.53/176.47 [0 0 0] [1], 553.53/176.47 553.53/176.47 [1 1 0] [1] 553.53/176.47 [active](x0) = [0 0 0]x0 + [0] 553.53/176.47 [0 0 0] [1], 553.53/176.47 553.53/176.47 [1 0 0] 553.53/176.47 [f](x0) = [0 1 0]x0 553.53/176.47 [0 0 0] 553.53/176.47 orientation: 553.53/176.47 [1 1 0] [1] [1 1 0] [0] 553.53/176.47 d(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(d(X)) 553.53/176.47 [0 0 0] [0] [0 0 0] [0] 553.53/176.47 553.53/176.47 [1 0 0] [0] [1 0 0] [0] 553.53/176.47 h(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(h(X)) 553.53/176.47 [0 0 0] [1] [0 0 0] [0] 553.53/176.47 553.53/176.47 [1 1 0] [1] [1 0 0] [1] 553.53/176.47 active(f(f(X))) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(c(f(g(f(X))))) 553.53/176.47 [0 0 0] [1] [0 0 0] [0] 553.53/176.47 553.53/176.47 [1 1 0] [2] [1 1 0] 553.53/176.47 active(c(X)) = [0 0 0]X + [0] >= [0 0 0]X = mark(d(X)) 553.53/176.47 [0 0 0] [1] [0 0 0] 553.53/176.47 553.53/176.47 [1 1 0] [1] [1 1 0] [1] 553.53/176.47 active(h(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(c(d(X))) 553.53/176.47 [0 0 0] [1] [0 0 0] [0] 553.53/176.47 553.53/176.47 [1 0 0] [1] [1 0 0] [1] 553.53/176.47 top(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = top(proper(X)) 553.53/176.47 [0 0 0] [0] [0 0 0] [0] 553.53/176.47 553.53/176.47 [1 1 0] [2] [1 1 0] [2] 553.53/176.47 top(ok(X)) = [0 1 0]X + [1] >= [0 0 0]X + [0] = top(active(X)) 553.53/176.47 [0 0 0] [0] [0 0 0] [0] 553.53/176.47 553.53/176.47 [1 1 0] [1] [1 1 0] [1] 553.53/176.47 active(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(active(X)) 553.53/176.47 [0 0 0] [1] [0 0 0] [0] 553.53/176.47 553.53/176.47 [1 1 0] [1] [1 1 0] [1] 553.53/176.47 active(h(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = h(active(X)) 553.53/176.47 [0 0 0] [1] [0 0 0] [1] 553.53/176.47 553.53/176.47 [1 0 0] [1 0 0] 553.53/176.47 f(mark(X)) = [0 0 0]X >= [0 0 0]X = mark(f(X)) 553.53/176.47 [0 0 0] [0 0 0] 553.53/176.47 553.53/176.47 [1 0 0] [0] [1 0 0] 553.53/176.47 h(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X = mark(h(X)) 553.53/176.47 [0 0 0] [1] [0 0 0] 553.53/176.47 553.53/176.47 [1 0 0] [0] [1 0 0] 553.53/176.47 proper(f(X)) = [0 0 0]X + [0] >= [0 0 0]X = f(proper(X)) 553.53/176.47 [0 0 0] [1] [0 0 0] 553.53/176.47 553.53/176.47 [1 0 0] [1] [1 0 0] [1] 553.53/176.47 proper(c(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = c(proper(X)) 553.53/176.47 [0 0 0] [1] [0 0 0] [0] 553.53/176.47 553.53/176.47 [1 0 0] [0] [1 0 0] [0] 553.53/176.47 proper(g(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = g(proper(X)) 553.53/176.47 [0 0 0] [1] [0 0 0] [1] 553.53/176.47 553.53/176.47 [1 1 0] [0] [1 0 0] 553.53/176.47 proper(d(X)) = [0 0 0]X + [0] >= [0 0 0]X = d(proper(X)) 553.53/176.47 [0 0 0] [1] [0 0 0] 553.53/176.47 553.53/176.47 [1 0 0] [0] [1 0 0] [0] 553.53/176.47 proper(h(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = h(proper(X)) 553.53/176.47 [0 0 0] [1] [0 0 0] [1] 553.53/176.47 553.53/176.47 [1 0 0] [0] [1 0 0] [0] 553.53/176.47 f(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(f(X)) 553.53/176.47 [0 0 0] [0] [0 0 0] [0] 553.53/176.47 553.53/176.47 [1 0 0] [1] [1 0 0] [1] 553.53/176.47 c(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(c(X)) 553.53/176.47 [0 0 0] [0] [0 0 0] [0] 553.53/176.47 553.53/176.47 [1 0 0] [0] [1 0 0] [0] 553.53/176.47 g(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(g(X)) 553.53/176.47 [0 0 0] [1] [0 0 0] [0] 553.53/176.47 problem: 553.53/176.47 strict: 553.53/176.47 553.53/176.47 weak: 553.53/176.47 d(ok(X)) -> ok(d(X)) 553.53/176.47 h(ok(X)) -> ok(h(X)) 553.53/176.47 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.53/176.47 active(c(X)) -> mark(d(X)) 553.53/176.47 active(h(X)) -> mark(c(d(X))) 553.53/176.47 top(mark(X)) -> top(proper(X)) 553.53/176.47 top(ok(X)) -> top(active(X)) 553.53/176.47 active(f(X)) -> f(active(X)) 553.53/176.47 active(h(X)) -> h(active(X)) 553.53/176.48 f(mark(X)) -> mark(f(X)) 553.53/176.48 h(mark(X)) -> mark(h(X)) 553.53/176.48 proper(f(X)) -> f(proper(X)) 553.53/176.48 proper(c(X)) -> c(proper(X)) 553.53/176.48 proper(g(X)) -> g(proper(X)) 553.53/176.48 proper(d(X)) -> d(proper(X)) 553.53/176.48 proper(h(X)) -> h(proper(X)) 553.53/176.48 f(ok(X)) -> ok(f(X)) 553.53/176.48 c(ok(X)) -> ok(c(X)) 553.53/176.48 g(ok(X)) -> ok(g(X)) 553.53/176.48 Qed 553.53/176.48 553.53/176.48 strict: 553.53/176.48 active(f(X)) -> f(active(X)) 553.53/176.48 active(h(X)) -> h(active(X)) 553.53/176.48 f(mark(X)) -> mark(f(X)) 553.53/176.48 h(mark(X)) -> mark(h(X)) 553.53/176.48 proper(f(X)) -> f(proper(X)) 553.53/176.48 proper(c(X)) -> c(proper(X)) 553.53/176.48 proper(g(X)) -> g(proper(X)) 553.53/176.48 proper(d(X)) -> d(proper(X)) 553.53/176.48 proper(h(X)) -> h(proper(X)) 553.53/176.48 f(ok(X)) -> ok(f(X)) 553.53/176.48 c(ok(X)) -> ok(c(X)) 553.53/176.48 g(ok(X)) -> ok(g(X)) 553.53/176.48 weak: 553.53/176.48 d(ok(X)) -> ok(d(X)) 553.53/176.48 h(ok(X)) -> ok(h(X)) 553.53/176.48 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.53/176.48 active(c(X)) -> mark(d(X)) 553.53/176.48 active(h(X)) -> mark(c(d(X))) 553.53/176.48 top(mark(X)) -> top(proper(X)) 553.53/176.48 top(ok(X)) -> top(active(X)) 553.53/176.48 Splitting Processor: 553.53/176.48 strict: 553.53/176.48 g(ok(X)) -> ok(g(X)) 553.53/176.48 weak: 553.53/176.48 d(ok(X)) -> ok(d(X)) 553.53/176.48 h(ok(X)) -> ok(h(X)) 553.53/176.48 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.53/176.48 active(c(X)) -> mark(d(X)) 553.53/176.48 active(h(X)) -> mark(c(d(X))) 553.53/176.48 top(mark(X)) -> top(proper(X)) 553.53/176.48 top(ok(X)) -> top(active(X)) 553.53/176.48 active(f(X)) -> f(active(X)) 553.53/176.48 active(h(X)) -> h(active(X)) 553.53/176.48 f(mark(X)) -> mark(f(X)) 553.53/176.48 h(mark(X)) -> mark(h(X)) 553.53/176.48 proper(f(X)) -> f(proper(X)) 553.53/176.48 proper(c(X)) -> c(proper(X)) 553.53/176.48 proper(g(X)) -> g(proper(X)) 553.53/176.48 proper(d(X)) -> d(proper(X)) 553.53/176.48 proper(h(X)) -> h(proper(X)) 553.53/176.48 f(ok(X)) -> ok(f(X)) 553.53/176.48 c(ok(X)) -> ok(c(X)) 553.53/176.48 Splitting Processor: 553.53/176.48 strict: 553.53/176.48 c(ok(X)) -> ok(c(X)) 553.53/176.48 weak: 553.53/176.48 g(ok(X)) -> ok(g(X)) 553.53/176.48 d(ok(X)) -> ok(d(X)) 553.53/176.48 h(ok(X)) -> ok(h(X)) 553.53/176.48 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.53/176.48 active(c(X)) -> mark(d(X)) 553.53/176.48 active(h(X)) -> mark(c(d(X))) 553.53/176.48 top(mark(X)) -> top(proper(X)) 553.53/176.48 top(ok(X)) -> top(active(X)) 553.53/176.48 active(f(X)) -> f(active(X)) 553.53/176.48 active(h(X)) -> h(active(X)) 553.53/176.48 f(mark(X)) -> mark(f(X)) 553.53/176.48 h(mark(X)) -> mark(h(X)) 553.53/176.48 proper(f(X)) -> f(proper(X)) 553.53/176.48 proper(c(X)) -> c(proper(X)) 553.53/176.48 proper(g(X)) -> g(proper(X)) 553.53/176.48 proper(d(X)) -> d(proper(X)) 553.53/176.48 proper(h(X)) -> h(proper(X)) 553.53/176.48 f(ok(X)) -> ok(f(X)) 553.53/176.48 Matrix Interpretation Processor: dim=3 553.53/176.48 553.53/176.48 max_matrix: 553.53/176.48 [1 1 1] 553.53/176.48 [0 0 0] 553.53/176.48 [0 0 1] 553.53/176.48 interpretation: 553.53/176.48 [1 0 1] [0] 553.53/176.48 [top](x0) = [0 0 0]x0 + [1] 553.53/176.48 [0 0 0] [0], 553.53/176.48 553.53/176.48 [1 0 0] [0] 553.53/176.48 [ok](x0) = [0 0 0]x0 + [0] 553.53/176.48 [0 0 1] [1], 553.53/176.48 553.53/176.48 [1 0 0] 553.53/176.48 [proper](x0) = [0 0 0]x0 553.53/176.48 [0 0 0] , 553.53/176.48 553.53/176.48 [1 0 0] 553.53/176.48 [h](x0) = [0 0 0]x0 553.53/176.48 [0 0 1] , 553.53/176.48 553.53/176.48 [1 0 0] 553.53/176.48 [d](x0) = [0 0 0]x0 553.53/176.48 [0 0 1] , 553.53/176.48 553.53/176.48 [1 1 0] 553.53/176.48 [mark](x0) = [0 0 0]x0 553.53/176.48 [0 0 0] , 553.53/176.48 553.53/176.48 [1 0 1] 553.53/176.48 [c](x0) = [0 0 0]x0 553.53/176.48 [0 0 1] , 553.53/176.48 553.53/176.48 [1 0 0] 553.53/176.48 [g](x0) = [0 0 0]x0 553.53/176.48 [0 0 1] , 553.53/176.48 553.53/176.48 [1 0 1] 553.53/176.48 [active](x0) = [0 0 0]x0 553.53/176.48 [0 0 0] , 553.53/176.48 553.53/176.48 [1 0 0] 553.53/176.48 [f](x0) = [0 0 0]x0 553.53/176.48 [0 0 1] 553.53/176.48 orientation: 553.53/176.48 [1 0 1] [1] [1 0 1] [0] 553.53/176.48 c(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(c(X)) 553.53/176.48 [0 0 1] [1] [0 0 1] [1] 553.53/176.48 553.53/176.48 [1 0 0] [0] [1 0 0] [0] 553.53/176.48 g(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(g(X)) 553.53/176.48 [0 0 1] [1] [0 0 1] [1] 553.53/176.48 553.53/176.48 [1 0 0] [0] [1 0 0] [0] 553.53/176.48 d(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(d(X)) 553.53/176.48 [0 0 1] [1] [0 0 1] [1] 553.53/176.48 553.53/176.48 [1 0 0] [0] [1 0 0] [0] 553.53/176.48 h(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(h(X)) 553.53/176.48 [0 0 1] [1] [0 0 1] [1] 553.53/176.48 553.53/176.48 [1 0 1] [1 0 1] 553.53/176.48 active(f(f(X))) = [0 0 0]X >= [0 0 0]X = mark(c(f(g(f(X))))) 553.53/176.48 [0 0 0] [0 0 0] 553.53/176.48 553.53/176.48 [1 0 2] [1 0 0] 553.53/176.48 active(c(X)) = [0 0 0]X >= [0 0 0]X = mark(d(X)) 553.53/176.48 [0 0 0] [0 0 0] 553.53/176.48 553.53/176.48 [1 0 1] [1 0 1] 553.53/176.48 active(h(X)) = [0 0 0]X >= [0 0 0]X = mark(c(d(X))) 553.53/176.48 [0 0 0] [0 0 0] 553.53/176.48 553.53/176.48 [1 1 0] [0] [1 0 0] [0] 553.53/176.48 top(mark(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = top(proper(X)) 553.53/176.48 [0 0 0] [0] [0 0 0] [0] 553.53/176.48 553.53/176.48 [1 0 1] [1] [1 0 1] [0] 553.53/176.48 top(ok(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = top(active(X)) 553.53/176.48 [0 0 0] [0] [0 0 0] [0] 553.53/176.48 553.53/176.48 [1 0 1] [1 0 1] 553.53/176.48 active(f(X)) = [0 0 0]X >= [0 0 0]X = f(active(X)) 553.53/176.48 [0 0 0] [0 0 0] 553.53/176.48 553.53/176.48 [1 0 1] [1 0 1] 553.53/176.48 active(h(X)) = [0 0 0]X >= [0 0 0]X = h(active(X)) 553.53/176.48 [0 0 0] [0 0 0] 553.53/176.48 553.53/176.48 [1 1 0] [1 0 0] 553.53/176.48 f(mark(X)) = [0 0 0]X >= [0 0 0]X = mark(f(X)) 553.53/176.48 [0 0 0] [0 0 0] 553.53/176.48 553.53/176.48 [1 1 0] [1 0 0] 553.53/176.48 h(mark(X)) = [0 0 0]X >= [0 0 0]X = mark(h(X)) 553.53/176.48 [0 0 0] [0 0 0] 553.53/176.48 553.53/176.48 [1 0 0] [1 0 0] 553.53/176.48 proper(f(X)) = [0 0 0]X >= [0 0 0]X = f(proper(X)) 553.53/176.48 [0 0 0] [0 0 0] 553.53/176.48 553.53/176.48 [1 0 1] [1 0 0] 553.53/176.48 proper(c(X)) = [0 0 0]X >= [0 0 0]X = c(proper(X)) 553.53/176.48 [0 0 0] [0 0 0] 553.53/176.48 553.53/176.48 [1 0 0] [1 0 0] 553.53/176.48 proper(g(X)) = [0 0 0]X >= [0 0 0]X = g(proper(X)) 553.53/176.48 [0 0 0] [0 0 0] 553.53/176.48 553.53/176.48 [1 0 0] [1 0 0] 553.53/176.48 proper(d(X)) = [0 0 0]X >= [0 0 0]X = d(proper(X)) 553.53/176.48 [0 0 0] [0 0 0] 553.53/176.48 553.53/176.48 [1 0 0] [1 0 0] 553.53/176.48 proper(h(X)) = [0 0 0]X >= [0 0 0]X = h(proper(X)) 553.53/176.48 [0 0 0] [0 0 0] 553.53/176.48 553.53/176.48 [1 0 0] [0] [1 0 0] [0] 553.53/176.48 f(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(f(X)) 553.53/176.48 [0 0 1] [1] [0 0 1] [1] 553.53/176.48 problem: 553.53/176.48 strict: 553.53/176.48 553.53/176.48 weak: 553.53/176.48 c(ok(X)) -> ok(c(X)) 553.53/176.48 g(ok(X)) -> ok(g(X)) 553.53/176.48 d(ok(X)) -> ok(d(X)) 553.53/176.48 h(ok(X)) -> ok(h(X)) 553.53/176.48 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.53/176.48 active(c(X)) -> mark(d(X)) 553.53/176.48 active(h(X)) -> mark(c(d(X))) 553.53/176.48 top(mark(X)) -> top(proper(X)) 553.53/176.48 top(ok(X)) -> top(active(X)) 553.53/176.48 active(f(X)) -> f(active(X)) 553.53/176.48 active(h(X)) -> h(active(X)) 553.53/176.48 f(mark(X)) -> mark(f(X)) 553.53/176.48 h(mark(X)) -> mark(h(X)) 553.53/176.48 proper(f(X)) -> f(proper(X)) 553.53/176.49 proper(c(X)) -> c(proper(X)) 553.53/176.49 proper(g(X)) -> g(proper(X)) 553.53/176.49 proper(d(X)) -> d(proper(X)) 553.53/176.49 proper(h(X)) -> h(proper(X)) 553.53/176.49 f(ok(X)) -> ok(f(X)) 553.53/176.49 Qed 553.53/176.49 553.53/176.49 strict: 553.53/176.49 active(f(X)) -> f(active(X)) 553.53/176.49 active(h(X)) -> h(active(X)) 553.53/176.49 f(mark(X)) -> mark(f(X)) 553.53/176.49 h(mark(X)) -> mark(h(X)) 553.53/176.49 proper(f(X)) -> f(proper(X)) 553.53/176.49 proper(c(X)) -> c(proper(X)) 553.53/176.49 proper(g(X)) -> g(proper(X)) 553.53/176.49 proper(d(X)) -> d(proper(X)) 553.53/176.49 proper(h(X)) -> h(proper(X)) 553.53/176.49 f(ok(X)) -> ok(f(X)) 553.53/176.49 weak: 553.53/176.49 c(ok(X)) -> ok(c(X)) 553.53/176.49 g(ok(X)) -> ok(g(X)) 553.53/176.49 d(ok(X)) -> ok(d(X)) 553.53/176.49 h(ok(X)) -> ok(h(X)) 553.53/176.49 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.53/176.49 active(c(X)) -> mark(d(X)) 553.53/176.49 active(h(X)) -> mark(c(d(X))) 553.53/176.49 top(mark(X)) -> top(proper(X)) 553.53/176.49 top(ok(X)) -> top(active(X)) 553.53/176.49 Matrix Interpretation Processor: dim=3 553.53/176.49 553.53/176.49 max_matrix: 553.53/176.49 [1 1 0] 553.53/176.49 [0 1 0] 553.53/176.49 [0 0 0] 553.53/176.49 interpretation: 553.53/176.49 [1 0 0] [0] 553.53/176.49 [top](x0) = [0 0 0]x0 + [1] 553.53/176.49 [0 0 0] [0], 553.53/176.49 553.53/176.49 [1 0 0] [1] 553.53/176.49 [ok](x0) = [0 1 0]x0 + [1] 553.53/176.49 [0 0 0] [0], 553.53/176.49 553.53/176.49 [1 0 0] 553.53/176.49 [proper](x0) = [0 0 0]x0 553.53/176.49 [0 0 0] , 553.53/176.49 553.53/176.49 [1 0 0] 553.53/176.49 [h](x0) = [0 1 0]x0 553.53/176.49 [0 0 0] , 553.53/176.49 553.53/176.49 [1 0 0] 553.53/176.49 [d](x0) = [0 1 0]x0 553.53/176.49 [0 0 0] , 553.53/176.49 553.53/176.49 [1 0 0] 553.53/176.49 [mark](x0) = [0 1 0]x0 553.53/176.49 [0 0 0] , 553.53/176.49 553.53/176.49 [1 0 0] 553.53/176.49 [c](x0) = [0 1 0]x0 553.53/176.49 [0 0 0] , 553.53/176.49 553.53/176.49 [1 0 0] 553.53/176.49 [g](x0) = [0 1 0]x0 553.53/176.49 [0 0 0] , 553.53/176.49 553.53/176.49 [1 0 0] 553.53/176.49 [active](x0) = [0 1 0]x0 553.53/176.49 [0 0 0] , 553.53/176.49 553.53/176.49 [1 1 0] 553.53/176.49 [f](x0) = [0 1 0]x0 553.53/176.49 [0 0 0] 553.53/176.49 orientation: 553.53/176.49 [1 1 0] [1 1 0] 553.53/176.49 active(f(X)) = [0 1 0]X >= [0 1 0]X = f(active(X)) 553.53/176.49 [0 0 0] [0 0 0] 553.53/176.49 553.53/176.49 [1 0 0] [1 0 0] 553.53/176.49 active(h(X)) = [0 1 0]X >= [0 1 0]X = h(active(X)) 553.53/176.49 [0 0 0] [0 0 0] 553.53/176.49 553.53/176.49 [1 1 0] [1 1 0] 553.53/176.49 f(mark(X)) = [0 1 0]X >= [0 1 0]X = mark(f(X)) 553.53/176.49 [0 0 0] [0 0 0] 553.53/176.49 553.53/176.49 [1 0 0] [1 0 0] 553.53/176.49 h(mark(X)) = [0 1 0]X >= [0 1 0]X = mark(h(X)) 553.53/176.49 [0 0 0] [0 0 0] 553.53/176.49 553.53/176.49 [1 1 0] [1 0 0] 553.53/176.49 proper(f(X)) = [0 0 0]X >= [0 0 0]X = f(proper(X)) 553.53/176.49 [0 0 0] [0 0 0] 553.53/176.49 553.53/176.49 [1 0 0] [1 0 0] 553.53/176.49 proper(c(X)) = [0 0 0]X >= [0 0 0]X = c(proper(X)) 553.53/176.49 [0 0 0] [0 0 0] 553.53/176.49 553.53/176.49 [1 0 0] [1 0 0] 553.53/176.49 proper(g(X)) = [0 0 0]X >= [0 0 0]X = g(proper(X)) 553.53/176.49 [0 0 0] [0 0 0] 553.53/176.49 553.53/176.49 [1 0 0] [1 0 0] 553.53/176.49 proper(d(X)) = [0 0 0]X >= [0 0 0]X = d(proper(X)) 553.53/176.49 [0 0 0] [0 0 0] 553.53/176.49 553.53/176.49 [1 0 0] [1 0 0] 553.53/176.49 proper(h(X)) = [0 0 0]X >= [0 0 0]X = h(proper(X)) 553.53/176.49 [0 0 0] [0 0 0] 553.53/176.49 553.53/176.49 [1 1 0] [2] [1 1 0] [1] 553.53/176.49 f(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(f(X)) 553.53/176.49 [0 0 0] [0] [0 0 0] [0] 553.53/176.49 553.53/176.49 [1 0 0] [1] [1 0 0] [1] 553.53/176.49 c(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(c(X)) 553.53/176.49 [0 0 0] [0] [0 0 0] [0] 553.53/176.49 553.53/176.49 [1 0 0] [1] [1 0 0] [1] 553.53/176.49 g(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(g(X)) 553.53/176.49 [0 0 0] [0] [0 0 0] [0] 553.53/176.49 553.53/176.49 [1 0 0] [1] [1 0 0] [1] 553.53/176.49 d(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(d(X)) 553.53/176.49 [0 0 0] [0] [0 0 0] [0] 553.53/176.49 553.53/176.49 [1 0 0] [1] [1 0 0] [1] 553.53/176.49 h(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(h(X)) 553.53/176.49 [0 0 0] [0] [0 0 0] [0] 553.53/176.49 553.53/176.49 [1 2 0] [1 2 0] 553.53/176.49 active(f(f(X))) = [0 1 0]X >= [0 1 0]X = mark(c(f(g(f(X))))) 553.53/176.49 [0 0 0] [0 0 0] 553.53/176.49 553.53/176.49 [1 0 0] [1 0 0] 553.53/176.49 active(c(X)) = [0 1 0]X >= [0 1 0]X = mark(d(X)) 553.53/176.49 [0 0 0] [0 0 0] 553.53/176.49 553.53/176.49 [1 0 0] [1 0 0] 553.53/176.49 active(h(X)) = [0 1 0]X >= [0 1 0]X = mark(c(d(X))) 553.53/176.49 [0 0 0] [0 0 0] 553.53/176.49 553.53/176.49 [1 0 0] [0] [1 0 0] [0] 553.53/176.49 top(mark(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = top(proper(X)) 553.53/176.49 [0 0 0] [0] [0 0 0] [0] 553.53/176.49 553.53/176.49 [1 0 0] [1] [1 0 0] [0] 553.53/176.49 top(ok(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = top(active(X)) 553.53/176.49 [0 0 0] [0] [0 0 0] [0] 553.53/176.49 problem: 553.53/176.49 strict: 553.53/176.49 active(f(X)) -> f(active(X)) 553.53/176.49 active(h(X)) -> h(active(X)) 553.53/176.49 f(mark(X)) -> mark(f(X)) 553.53/176.49 h(mark(X)) -> mark(h(X)) 553.53/176.49 proper(f(X)) -> f(proper(X)) 553.53/176.49 proper(c(X)) -> c(proper(X)) 553.53/176.49 proper(g(X)) -> g(proper(X)) 553.53/176.49 proper(d(X)) -> d(proper(X)) 553.53/176.49 proper(h(X)) -> h(proper(X)) 553.53/176.49 weak: 553.53/176.49 f(ok(X)) -> ok(f(X)) 553.53/176.49 c(ok(X)) -> ok(c(X)) 553.53/176.49 g(ok(X)) -> ok(g(X)) 553.53/176.49 d(ok(X)) -> ok(d(X)) 553.53/176.49 h(ok(X)) -> ok(h(X)) 553.53/176.49 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.53/176.49 active(c(X)) -> mark(d(X)) 553.53/176.49 active(h(X)) -> mark(c(d(X))) 553.53/176.49 top(mark(X)) -> top(proper(X)) 553.53/176.49 top(ok(X)) -> top(active(X)) 553.53/176.49 Splitting Processor: 553.53/176.49 strict: 553.53/176.49 active(f(X)) -> f(active(X)) 553.53/176.49 weak: 553.53/176.49 f(ok(X)) -> ok(f(X)) 553.53/176.49 c(ok(X)) -> ok(c(X)) 553.53/176.49 g(ok(X)) -> ok(g(X)) 553.53/176.49 d(ok(X)) -> ok(d(X)) 553.53/176.49 h(ok(X)) -> ok(h(X)) 553.53/176.49 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.53/176.49 active(c(X)) -> mark(d(X)) 553.53/176.49 active(h(X)) -> mark(c(d(X))) 553.53/176.49 top(mark(X)) -> top(proper(X)) 553.53/176.49 top(ok(X)) -> top(active(X)) 553.53/176.49 active(h(X)) -> h(active(X)) 553.53/176.49 f(mark(X)) -> mark(f(X)) 553.53/176.49 h(mark(X)) -> mark(h(X)) 553.53/176.49 proper(f(X)) -> f(proper(X)) 553.53/176.49 proper(c(X)) -> c(proper(X)) 553.53/176.49 proper(g(X)) -> g(proper(X)) 553.53/176.49 proper(d(X)) -> d(proper(X)) 553.53/176.49 proper(h(X)) -> h(proper(X)) 553.53/176.49 Splitting Processor: 553.53/176.49 strict: 553.53/176.49 proper(h(X)) -> h(proper(X)) 553.53/176.49 weak: 553.53/176.49 active(f(X)) -> f(active(X)) 553.53/176.49 f(ok(X)) -> ok(f(X)) 553.53/176.49 c(ok(X)) -> ok(c(X)) 553.53/176.49 g(ok(X)) -> ok(g(X)) 553.53/176.49 d(ok(X)) -> ok(d(X)) 553.53/176.49 h(ok(X)) -> ok(h(X)) 553.53/176.49 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.53/176.49 active(c(X)) -> mark(d(X)) 553.53/176.49 active(h(X)) -> mark(c(d(X))) 553.53/176.49 top(mark(X)) -> top(proper(X)) 553.53/176.49 top(ok(X)) -> top(active(X)) 553.53/176.49 active(h(X)) -> h(active(X)) 553.53/176.49 f(mark(X)) -> mark(f(X)) 553.63/176.50 h(mark(X)) -> mark(h(X)) 553.63/176.50 proper(f(X)) -> f(proper(X)) 553.63/176.50 proper(c(X)) -> c(proper(X)) 553.63/176.50 proper(g(X)) -> g(proper(X)) 553.63/176.50 proper(d(X)) -> d(proper(X)) 553.63/176.50 Matrix Interpretation Processor: dim=3 553.63/176.50 553.63/176.50 max_matrix: 553.63/176.50 [1 1 1] 553.63/176.50 [0 0 1] 553.63/176.50 [0 0 1] 553.63/176.50 interpretation: 553.63/176.50 [1 1 0] 553.63/176.50 [top](x0) = [0 0 0]x0 553.63/176.50 [0 0 1] , 553.63/176.50 553.63/176.50 [1 0 1] [1] 553.63/176.50 [ok](x0) = [0 0 1]x0 + [0] 553.63/176.50 [0 0 1] [1], 553.63/176.50 553.63/176.50 [1 0 1] 553.63/176.50 [proper](x0) = [0 0 1]x0 553.63/176.50 [0 0 1] , 553.63/176.50 553.63/176.50 [1 0 1] [0] 553.63/176.50 [h](x0) = [0 0 1]x0 + [0] 553.63/176.50 [0 0 1] [1], 553.63/176.50 553.63/176.50 [1 0 0] 553.63/176.50 [d](x0) = [0 0 1]x0 553.63/176.50 [0 0 1] , 553.63/176.50 553.63/176.50 [1 0 1] [0] 553.63/176.50 [mark](x0) = [0 0 1]x0 + [0] 553.63/176.50 [0 0 1] [1], 553.63/176.50 553.63/176.50 [1 0 0] 553.63/176.50 [c](x0) = [0 0 1]x0 553.63/176.50 [0 0 1] , 553.63/176.50 553.63/176.50 [1 0 0] 553.63/176.50 [g](x0) = [0 0 1]x0 553.63/176.50 [0 0 1] , 553.63/176.50 553.63/176.50 [1 0 1] [0] 553.63/176.50 [active](x0) = [0 0 1]x0 + [1] 553.63/176.50 [0 0 1] [1], 553.63/176.50 553.63/176.50 [1 0 0] 553.63/176.50 [f](x0) = [0 0 1]x0 553.63/176.50 [0 0 1] 553.63/176.50 orientation: 553.63/176.50 [1 0 2] [1] [1 0 2] [0] 553.63/176.50 proper(h(X)) = [0 0 1]X + [1] >= [0 0 1]X + [0] = h(proper(X)) 553.63/176.50 [0 0 1] [1] [0 0 1] [1] 553.63/176.50 553.63/176.50 [1 0 1] [0] [1 0 1] [0] 553.63/176.50 active(f(X)) = [0 0 1]X + [1] >= [0 0 1]X + [1] = f(active(X)) 553.63/176.50 [0 0 1] [1] [0 0 1] [1] 553.63/176.50 553.63/176.50 [1 0 1] [1] [1 0 1] [1] 553.63/176.50 f(ok(X)) = [0 0 1]X + [1] >= [0 0 1]X + [0] = ok(f(X)) 553.63/176.50 [0 0 1] [1] [0 0 1] [1] 553.63/176.50 553.63/176.50 [1 0 1] [1] [1 0 1] [1] 553.63/176.50 c(ok(X)) = [0 0 1]X + [1] >= [0 0 1]X + [0] = ok(c(X)) 553.63/176.50 [0 0 1] [1] [0 0 1] [1] 553.63/176.50 553.63/176.50 [1 0 1] [1] [1 0 1] [1] 553.63/176.50 g(ok(X)) = [0 0 1]X + [1] >= [0 0 1]X + [0] = ok(g(X)) 553.63/176.50 [0 0 1] [1] [0 0 1] [1] 553.63/176.50 553.63/176.50 [1 0 1] [1] [1 0 1] [1] 553.63/176.50 d(ok(X)) = [0 0 1]X + [1] >= [0 0 1]X + [0] = ok(d(X)) 553.63/176.50 [0 0 1] [1] [0 0 1] [1] 553.63/176.50 553.63/176.50 [1 0 2] [2] [1 0 2] [2] 553.63/176.50 h(ok(X)) = [0 0 1]X + [1] >= [0 0 1]X + [1] = ok(h(X)) 553.63/176.50 [0 0 1] [2] [0 0 1] [2] 553.63/176.50 553.63/176.50 [1 0 1] [0] [1 0 1] [0] 553.63/176.50 active(f(f(X))) = [0 0 1]X + [1] >= [0 0 1]X + [0] = mark(c(f(g(f(X))))) 553.63/176.50 [0 0 1] [1] [0 0 1] [1] 553.63/176.50 553.63/176.50 [1 0 1] [0] [1 0 1] [0] 553.63/176.50 active(c(X)) = [0 0 1]X + [1] >= [0 0 1]X + [0] = mark(d(X)) 553.63/176.50 [0 0 1] [1] [0 0 1] [1] 553.63/176.50 553.63/176.50 [1 0 2] [1] [1 0 1] [0] 553.63/176.50 active(h(X)) = [0 0 1]X + [2] >= [0 0 1]X + [0] = mark(c(d(X))) 553.63/176.50 [0 0 1] [2] [0 0 1] [1] 553.63/176.50 553.63/176.50 [1 0 2] [0] [1 0 2] 553.63/176.50 top(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X = top(proper(X)) 553.63/176.50 [0 0 1] [1] [0 0 1] 553.63/176.50 553.63/176.50 [1 0 2] [1] [1 0 2] [1] 553.63/176.50 top(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = top(active(X)) 553.63/176.50 [0 0 1] [1] [0 0 1] [1] 553.63/176.50 553.63/176.50 [1 0 2] [1] [1 0 2] [1] 553.63/176.50 active(h(X)) = [0 0 1]X + [2] >= [0 0 1]X + [1] = h(active(X)) 553.63/176.50 [0 0 1] [2] [0 0 1] [2] 553.63/176.50 553.63/176.50 [1 0 1] [0] [1 0 1] [0] 553.63/176.50 f(mark(X)) = [0 0 1]X + [1] >= [0 0 1]X + [0] = mark(f(X)) 553.63/176.50 [0 0 1] [1] [0 0 1] [1] 553.63/176.50 553.63/176.50 [1 0 2] [1] [1 0 2] [1] 553.63/176.50 h(mark(X)) = [0 0 1]X + [1] >= [0 0 1]X + [1] = mark(h(X)) 553.63/176.50 [0 0 1] [2] [0 0 1] [2] 553.63/176.50 553.63/176.50 [1 0 1] [1 0 1] 553.63/176.50 proper(f(X)) = [0 0 1]X >= [0 0 1]X = f(proper(X)) 553.63/176.50 [0 0 1] [0 0 1] 553.63/176.50 553.63/176.50 [1 0 1] [1 0 1] 553.63/176.50 proper(c(X)) = [0 0 1]X >= [0 0 1]X = c(proper(X)) 553.63/176.50 [0 0 1] [0 0 1] 553.63/176.50 553.63/176.50 [1 0 1] [1 0 1] 553.63/176.50 proper(g(X)) = [0 0 1]X >= [0 0 1]X = g(proper(X)) 553.63/176.50 [0 0 1] [0 0 1] 553.63/176.50 553.63/176.50 [1 0 1] [1 0 1] 553.63/176.50 proper(d(X)) = [0 0 1]X >= [0 0 1]X = d(proper(X)) 553.63/176.50 [0 0 1] [0 0 1] 553.63/176.50 problem: 553.63/176.50 strict: 553.63/176.50 553.63/176.50 weak: 553.63/176.50 proper(h(X)) -> h(proper(X)) 553.63/176.50 active(f(X)) -> f(active(X)) 553.63/176.50 f(ok(X)) -> ok(f(X)) 553.63/176.50 c(ok(X)) -> ok(c(X)) 553.63/176.50 g(ok(X)) -> ok(g(X)) 553.63/176.50 d(ok(X)) -> ok(d(X)) 553.63/176.50 h(ok(X)) -> ok(h(X)) 553.63/176.50 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.50 active(c(X)) -> mark(d(X)) 553.63/176.50 active(h(X)) -> mark(c(d(X))) 553.63/176.50 top(mark(X)) -> top(proper(X)) 553.63/176.50 top(ok(X)) -> top(active(X)) 553.63/176.50 active(h(X)) -> h(active(X)) 553.63/176.50 f(mark(X)) -> mark(f(X)) 553.63/176.50 h(mark(X)) -> mark(h(X)) 553.63/176.50 proper(f(X)) -> f(proper(X)) 553.63/176.50 proper(c(X)) -> c(proper(X)) 553.63/176.50 proper(g(X)) -> g(proper(X)) 553.63/176.50 proper(d(X)) -> d(proper(X)) 553.63/176.50 Qed 553.63/176.50 553.63/176.50 strict: 553.63/176.50 active(h(X)) -> h(active(X)) 553.63/176.50 f(mark(X)) -> mark(f(X)) 553.63/176.50 h(mark(X)) -> mark(h(X)) 553.63/176.50 proper(f(X)) -> f(proper(X)) 553.63/176.50 proper(c(X)) -> c(proper(X)) 553.63/176.50 proper(g(X)) -> g(proper(X)) 553.63/176.50 proper(d(X)) -> d(proper(X)) 553.63/176.50 weak: 553.63/176.50 proper(h(X)) -> h(proper(X)) 553.63/176.50 active(f(X)) -> f(active(X)) 553.63/176.50 f(ok(X)) -> ok(f(X)) 553.63/176.50 c(ok(X)) -> ok(c(X)) 553.63/176.50 g(ok(X)) -> ok(g(X)) 553.63/176.50 d(ok(X)) -> ok(d(X)) 553.63/176.50 h(ok(X)) -> ok(h(X)) 553.63/176.50 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.50 active(c(X)) -> mark(d(X)) 553.63/176.50 active(h(X)) -> mark(c(d(X))) 553.63/176.50 top(mark(X)) -> top(proper(X)) 553.63/176.50 top(ok(X)) -> top(active(X)) 553.63/176.50 Splitting Processor: 553.63/176.50 strict: 553.63/176.50 proper(f(X)) -> f(proper(X)) 553.63/176.50 weak: 553.63/176.50 proper(h(X)) -> h(proper(X)) 553.63/176.50 active(f(X)) -> f(active(X)) 553.63/176.50 f(ok(X)) -> ok(f(X)) 553.63/176.50 c(ok(X)) -> ok(c(X)) 553.63/176.50 g(ok(X)) -> ok(g(X)) 553.63/176.50 d(ok(X)) -> ok(d(X)) 553.63/176.50 h(ok(X)) -> ok(h(X)) 553.63/176.50 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.50 active(c(X)) -> mark(d(X)) 553.63/176.50 active(h(X)) -> mark(c(d(X))) 553.63/176.50 top(mark(X)) -> top(proper(X)) 553.63/176.50 top(ok(X)) -> top(active(X)) 553.63/176.51 active(h(X)) -> h(active(X)) 553.63/176.51 f(mark(X)) -> mark(f(X)) 553.63/176.51 h(mark(X)) -> mark(h(X)) 553.63/176.51 proper(c(X)) -> c(proper(X)) 553.63/176.51 proper(g(X)) -> g(proper(X)) 553.63/176.51 proper(d(X)) -> d(proper(X)) 553.63/176.51 Splitting Processor: 553.63/176.51 strict: 553.63/176.51 h(mark(X)) -> mark(h(X)) 553.63/176.51 weak: 553.63/176.51 proper(f(X)) -> f(proper(X)) 553.63/176.51 proper(h(X)) -> h(proper(X)) 553.63/176.51 active(f(X)) -> f(active(X)) 553.63/176.51 f(ok(X)) -> ok(f(X)) 553.63/176.51 c(ok(X)) -> ok(c(X)) 553.63/176.51 g(ok(X)) -> ok(g(X)) 553.63/176.51 d(ok(X)) -> ok(d(X)) 553.63/176.51 h(ok(X)) -> ok(h(X)) 553.63/176.51 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.51 active(c(X)) -> mark(d(X)) 553.63/176.51 active(h(X)) -> mark(c(d(X))) 553.63/176.51 top(mark(X)) -> top(proper(X)) 553.63/176.51 top(ok(X)) -> top(active(X)) 553.63/176.51 active(h(X)) -> h(active(X)) 553.63/176.51 f(mark(X)) -> mark(f(X)) 553.63/176.51 proper(c(X)) -> c(proper(X)) 553.63/176.51 proper(g(X)) -> g(proper(X)) 553.63/176.51 proper(d(X)) -> d(proper(X)) 553.63/176.51 Matrix Interpretation Processor: dim=3 553.63/176.51 553.63/176.51 max_matrix: 553.63/176.51 [1 0 1] 553.63/176.51 [0 0 0] 553.63/176.51 [0 0 1] 553.63/176.51 interpretation: 553.63/176.51 [1 0 0] 553.63/176.51 [top](x0) = [0 0 0]x0 553.63/176.51 [0 0 0] , 553.63/176.51 553.63/176.51 [1 0 1] [0] 553.63/176.51 [ok](x0) = [0 0 0]x0 + [0] 553.63/176.51 [0 0 1] [1], 553.63/176.51 553.63/176.51 [1 0 0] 553.63/176.51 [proper](x0) = [0 0 0]x0 553.63/176.51 [0 0 1] , 553.63/176.51 553.63/176.51 [1 0 1] [0] 553.63/176.51 [h](x0) = [0 0 0]x0 + [0] 553.63/176.51 [0 0 1] [1], 553.63/176.51 553.63/176.51 [1 0 0] 553.63/176.51 [d](x0) = [0 0 0]x0 553.63/176.51 [0 0 1] , 553.63/176.51 553.63/176.51 [1 0 0] [0] 553.63/176.51 [mark](x0) = [0 0 0]x0 + [0] 553.63/176.51 [0 0 1] [1], 553.63/176.51 553.63/176.51 [1 0 0] 553.63/176.51 [c](x0) = [0 0 0]x0 553.63/176.51 [0 0 1] , 553.63/176.51 553.63/176.51 [1 0 1] 553.63/176.51 [g](x0) = [0 0 0]x0 553.63/176.51 [0 0 1] , 553.63/176.51 553.63/176.51 [1 0 1] [0] 553.63/176.51 [active](x0) = [0 0 0]x0 + [0] 553.63/176.51 [0 0 1] [1], 553.63/176.51 553.63/176.51 [1 0 0] 553.63/176.51 [f](x0) = [0 0 0]x0 553.63/176.51 [0 0 1] 553.63/176.51 orientation: 553.63/176.51 [1 0 1] [1] [1 0 1] [0] 553.63/176.51 h(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(h(X)) 553.63/176.51 [0 0 1] [2] [0 0 1] [2] 553.63/176.51 553.63/176.51 [1 0 0] [1 0 0] 553.63/176.51 proper(f(X)) = [0 0 0]X >= [0 0 0]X = f(proper(X)) 553.63/176.51 [0 0 1] [0 0 1] 553.63/176.51 553.63/176.51 [1 0 1] [0] [1 0 1] [0] 553.63/176.51 proper(h(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = h(proper(X)) 553.63/176.51 [0 0 1] [1] [0 0 1] [1] 553.63/176.51 553.63/176.51 [1 0 1] [0] [1 0 1] [0] 553.63/176.51 active(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(active(X)) 553.63/176.51 [0 0 1] [1] [0 0 1] [1] 553.63/176.51 553.63/176.51 [1 0 1] [0] [1 0 1] [0] 553.63/176.51 f(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(f(X)) 553.63/176.51 [0 0 1] [1] [0 0 1] [1] 553.63/176.51 553.63/176.51 [1 0 1] [0] [1 0 1] [0] 553.63/176.51 c(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(c(X)) 553.63/176.51 [0 0 1] [1] [0 0 1] [1] 553.63/176.51 553.63/176.51 [1 0 2] [1] [1 0 2] [0] 553.63/176.51 g(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(g(X)) 553.63/176.51 [0 0 1] [1] [0 0 1] [1] 553.63/176.51 553.63/176.51 [1 0 1] [0] [1 0 1] [0] 553.63/176.51 d(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(d(X)) 553.63/176.51 [0 0 1] [1] [0 0 1] [1] 553.63/176.51 553.63/176.51 [1 0 2] [1] [1 0 2] [1] 553.63/176.51 h(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(h(X)) 553.63/176.51 [0 0 1] [2] [0 0 1] [2] 553.63/176.51 553.63/176.51 [1 0 1] [0] [1 0 1] [0] 553.63/176.51 active(f(f(X))) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(c(f(g(f(X))))) 553.63/176.51 [0 0 1] [1] [0 0 1] [1] 553.63/176.51 553.63/176.51 [1 0 1] [0] [1 0 0] [0] 553.63/176.51 active(c(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(d(X)) 553.63/176.51 [0 0 1] [1] [0 0 1] [1] 553.63/176.51 553.63/176.51 [1 0 2] [1] [1 0 0] [0] 553.63/176.51 active(h(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(c(d(X))) 553.63/176.51 [0 0 1] [2] [0 0 1] [1] 553.63/176.51 553.63/176.51 [1 0 0] [1 0 0] 553.63/176.51 top(mark(X)) = [0 0 0]X >= [0 0 0]X = top(proper(X)) 553.63/176.51 [0 0 0] [0 0 0] 553.63/176.51 553.63/176.51 [1 0 1] [1 0 1] 553.63/176.51 top(ok(X)) = [0 0 0]X >= [0 0 0]X = top(active(X)) 553.63/176.51 [0 0 0] [0 0 0] 553.63/176.51 553.63/176.51 [1 0 2] [1] [1 0 2] [1] 553.63/176.51 active(h(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = h(active(X)) 553.63/176.51 [0 0 1] [2] [0 0 1] [2] 553.63/176.51 553.63/176.51 [1 0 0] [0] [1 0 0] [0] 553.63/176.51 f(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(f(X)) 553.63/176.51 [0 0 1] [1] [0 0 1] [1] 553.63/176.51 553.63/176.51 [1 0 0] [1 0 0] 553.63/176.51 proper(c(X)) = [0 0 0]X >= [0 0 0]X = c(proper(X)) 553.63/176.51 [0 0 1] [0 0 1] 553.63/176.51 553.63/176.51 [1 0 1] [1 0 1] 553.63/176.51 proper(g(X)) = [0 0 0]X >= [0 0 0]X = g(proper(X)) 553.63/176.51 [0 0 1] [0 0 1] 553.63/176.51 553.63/176.51 [1 0 0] [1 0 0] 553.63/176.51 proper(d(X)) = [0 0 0]X >= [0 0 0]X = d(proper(X)) 553.63/176.51 [0 0 1] [0 0 1] 553.63/176.51 problem: 553.63/176.51 strict: 553.63/176.51 553.63/176.51 weak: 553.63/176.51 h(mark(X)) -> mark(h(X)) 553.63/176.51 proper(f(X)) -> f(proper(X)) 553.63/176.51 proper(h(X)) -> h(proper(X)) 553.63/176.51 active(f(X)) -> f(active(X)) 553.63/176.51 f(ok(X)) -> ok(f(X)) 553.63/176.51 c(ok(X)) -> ok(c(X)) 553.63/176.51 g(ok(X)) -> ok(g(X)) 553.63/176.51 d(ok(X)) -> ok(d(X)) 553.63/176.51 h(ok(X)) -> ok(h(X)) 553.63/176.51 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.51 active(c(X)) -> mark(d(X)) 553.63/176.51 active(h(X)) -> mark(c(d(X))) 553.63/176.51 top(mark(X)) -> top(proper(X)) 553.63/176.51 top(ok(X)) -> top(active(X)) 553.63/176.51 active(h(X)) -> h(active(X)) 553.63/176.51 f(mark(X)) -> mark(f(X)) 553.63/176.51 proper(c(X)) -> c(proper(X)) 553.63/176.51 proper(g(X)) -> g(proper(X)) 553.63/176.51 proper(d(X)) -> d(proper(X)) 553.63/176.51 Qed 553.63/176.51 553.63/176.51 strict: 553.63/176.51 active(h(X)) -> h(active(X)) 553.63/176.51 f(mark(X)) -> mark(f(X)) 553.63/176.51 proper(c(X)) -> c(proper(X)) 553.63/176.51 proper(g(X)) -> g(proper(X)) 553.63/176.52 proper(d(X)) -> d(proper(X)) 553.63/176.52 weak: 553.63/176.52 h(mark(X)) -> mark(h(X)) 553.63/176.52 proper(f(X)) -> f(proper(X)) 553.63/176.52 proper(h(X)) -> h(proper(X)) 553.63/176.52 active(f(X)) -> f(active(X)) 553.63/176.52 f(ok(X)) -> ok(f(X)) 553.63/176.52 c(ok(X)) -> ok(c(X)) 553.63/176.52 g(ok(X)) -> ok(g(X)) 553.63/176.52 d(ok(X)) -> ok(d(X)) 553.63/176.52 h(ok(X)) -> ok(h(X)) 553.63/176.52 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.52 active(c(X)) -> mark(d(X)) 553.63/176.52 active(h(X)) -> mark(c(d(X))) 553.63/176.52 top(mark(X)) -> top(proper(X)) 553.63/176.52 top(ok(X)) -> top(active(X)) 553.63/176.52 Splitting Processor: 553.63/176.52 strict: 553.63/176.52 f(mark(X)) -> mark(f(X)) 553.63/176.52 weak: 553.63/176.52 h(mark(X)) -> mark(h(X)) 553.63/176.52 proper(f(X)) -> f(proper(X)) 553.63/176.52 proper(h(X)) -> h(proper(X)) 553.63/176.52 active(f(X)) -> f(active(X)) 553.63/176.52 f(ok(X)) -> ok(f(X)) 553.63/176.52 c(ok(X)) -> ok(c(X)) 553.63/176.52 g(ok(X)) -> ok(g(X)) 553.63/176.52 d(ok(X)) -> ok(d(X)) 553.63/176.52 h(ok(X)) -> ok(h(X)) 553.63/176.52 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.52 active(c(X)) -> mark(d(X)) 553.63/176.52 active(h(X)) -> mark(c(d(X))) 553.63/176.52 top(mark(X)) -> top(proper(X)) 553.63/176.52 top(ok(X)) -> top(active(X)) 553.63/176.52 active(h(X)) -> h(active(X)) 553.63/176.52 proper(c(X)) -> c(proper(X)) 553.63/176.52 proper(g(X)) -> g(proper(X)) 553.63/176.52 proper(d(X)) -> d(proper(X)) 553.63/176.52 Splitting Processor: 553.63/176.52 strict: 553.63/176.52 active(h(X)) -> h(active(X)) 553.63/176.52 weak: 553.63/176.52 f(mark(X)) -> mark(f(X)) 553.63/176.52 h(mark(X)) -> mark(h(X)) 553.63/176.52 proper(f(X)) -> f(proper(X)) 553.63/176.52 proper(h(X)) -> h(proper(X)) 553.63/176.52 active(f(X)) -> f(active(X)) 553.63/176.52 f(ok(X)) -> ok(f(X)) 553.63/176.52 c(ok(X)) -> ok(c(X)) 553.63/176.52 g(ok(X)) -> ok(g(X)) 553.63/176.52 d(ok(X)) -> ok(d(X)) 553.63/176.52 h(ok(X)) -> ok(h(X)) 553.63/176.52 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.52 active(c(X)) -> mark(d(X)) 553.63/176.52 active(h(X)) -> mark(c(d(X))) 553.63/176.52 top(mark(X)) -> top(proper(X)) 553.63/176.52 top(ok(X)) -> top(active(X)) 553.63/176.52 proper(c(X)) -> c(proper(X)) 553.63/176.52 proper(g(X)) -> g(proper(X)) 553.63/176.52 proper(d(X)) -> d(proper(X)) 553.63/176.52 Matrix Interpretation Processor: dim=3 553.63/176.52 553.63/176.52 max_matrix: 553.63/176.52 [1 1 1] 553.63/176.52 [0 0 0] 553.63/176.52 [0 0 1] 553.63/176.52 interpretation: 553.63/176.52 [1 0 0] [0] 553.63/176.52 [top](x0) = [0 0 0]x0 + [1] 553.63/176.52 [0 0 0] [0], 553.63/176.52 553.63/176.52 [1 1 1] [1] 553.63/176.52 [ok](x0) = [0 0 0]x0 + [0] 553.63/176.52 [0 0 1] [1], 553.63/176.52 553.63/176.52 [1 0 0] [0] 553.63/176.52 [proper](x0) = [0 0 0]x0 + [1] 553.63/176.52 [0 0 1] [0], 553.63/176.52 553.63/176.52 [1 0 1] [1] 553.63/176.52 [h](x0) = [0 0 0]x0 + [0] 553.63/176.52 [0 0 1] [1], 553.63/176.52 553.63/176.52 [1 0 1] 553.63/176.52 [d](x0) = [0 0 0]x0 553.63/176.52 [0 0 1] , 553.63/176.52 553.63/176.52 [1 0 0] 553.63/176.52 [mark](x0) = [0 0 0]x0 553.63/176.52 [0 0 1] , 553.63/176.52 553.63/176.52 [1 0 1] [0] 553.63/176.52 [c](x0) = [0 0 0]x0 + [1] 553.63/176.52 [0 0 1] [0], 553.63/176.52 553.63/176.52 [1 0 0] 553.63/176.52 [g](x0) = [0 0 0]x0 553.63/176.52 [0 0 1] , 553.63/176.52 553.63/176.52 [1 0 1] [1] 553.63/176.52 [active](x0) = [0 0 0]x0 + [0] 553.63/176.52 [0 0 1] [0], 553.63/176.52 553.63/176.52 [1 0 0] 553.63/176.52 [f](x0) = [0 0 0]x0 553.63/176.52 [0 0 1] 553.63/176.52 orientation: 553.63/176.52 [1 0 2] [3] [1 0 2] [2] 553.63/176.52 active(h(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = h(active(X)) 553.63/176.52 [0 0 1] [1] [0 0 1] [1] 553.63/176.52 553.63/176.52 [1 0 0] [1 0 0] 553.63/176.52 f(mark(X)) = [0 0 0]X >= [0 0 0]X = mark(f(X)) 553.63/176.52 [0 0 1] [0 0 1] 553.63/176.52 553.63/176.52 [1 0 1] [1] [1 0 1] [1] 553.63/176.52 h(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(h(X)) 553.63/176.52 [0 0 1] [1] [0 0 1] [1] 553.63/176.52 553.63/176.52 [1 0 0] [0] [1 0 0] 553.63/176.52 proper(f(X)) = [0 0 0]X + [1] >= [0 0 0]X = f(proper(X)) 553.63/176.52 [0 0 1] [0] [0 0 1] 553.63/176.52 553.63/176.52 [1 0 1] [1] [1 0 1] [1] 553.63/176.52 proper(h(X)) = [0 0 0]X + [1] >= [0 0 0]X + [0] = h(proper(X)) 553.63/176.52 [0 0 1] [1] [0 0 1] [1] 553.63/176.52 553.63/176.52 [1 0 1] [1] [1 0 1] [1] 553.63/176.52 active(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(active(X)) 553.63/176.52 [0 0 1] [0] [0 0 1] [0] 553.63/176.52 553.63/176.52 [1 1 1] [1] [1 0 1] [1] 553.63/176.52 f(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(f(X)) 553.63/176.52 [0 0 1] [1] [0 0 1] [1] 553.63/176.52 553.63/176.52 [1 1 2] [2] [1 0 2] [2] 553.63/176.52 c(ok(X)) = [0 0 0]X + [1] >= [0 0 0]X + [0] = ok(c(X)) 553.63/176.52 [0 0 1] [1] [0 0 1] [1] 553.63/176.52 553.63/176.52 [1 1 1] [1] [1 0 1] [1] 553.63/176.52 g(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(g(X)) 553.63/176.52 [0 0 1] [1] [0 0 1] [1] 553.63/176.52 553.63/176.52 [1 1 2] [2] [1 0 2] [1] 553.63/176.52 d(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(d(X)) 553.63/176.52 [0 0 1] [1] [0 0 1] [1] 553.63/176.52 553.63/176.52 [1 1 2] [3] [1 0 2] [3] 553.63/176.52 h(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(h(X)) 553.63/176.52 [0 0 1] [2] [0 0 1] [2] 553.63/176.52 553.63/176.52 [1 0 1] [1] [1 0 1] 553.63/176.52 active(f(f(X))) = [0 0 0]X + [0] >= [0 0 0]X = mark(c(f(g(f(X))))) 553.63/176.52 [0 0 1] [0] [0 0 1] 553.63/176.52 553.63/176.52 [1 0 2] [1] [1 0 1] 553.63/176.52 active(c(X)) = [0 0 0]X + [0] >= [0 0 0]X = mark(d(X)) 553.63/176.52 [0 0 1] [0] [0 0 1] 553.63/176.52 553.63/176.52 [1 0 2] [3] [1 0 2] 553.63/176.52 active(h(X)) = [0 0 0]X + [0] >= [0 0 0]X = mark(c(d(X))) 553.63/176.52 [0 0 1] [1] [0 0 1] 553.63/176.52 553.63/176.52 [1 0 0] [0] [1 0 0] [0] 553.63/176.52 top(mark(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = top(proper(X)) 553.63/176.52 [0 0 0] [0] [0 0 0] [0] 553.63/176.52 553.63/176.52 [1 1 1] [1] [1 0 1] [1] 553.63/176.52 top(ok(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = top(active(X)) 553.63/176.52 [0 0 0] [0] [0 0 0] [0] 553.63/176.52 553.63/176.52 [1 0 1] [0] [1 0 1] [0] 553.63/176.52 proper(c(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = c(proper(X)) 553.63/176.52 [0 0 1] [0] [0 0 1] [0] 553.63/176.52 553.63/176.52 [1 0 0] [0] [1 0 0] 553.63/176.52 proper(g(X)) = [0 0 0]X + [1] >= [0 0 0]X = g(proper(X)) 553.63/176.52 [0 0 1] [0] [0 0 1] 553.63/176.52 553.63/176.52 [1 0 1] [0] [1 0 1] 553.63/176.52 proper(d(X)) = [0 0 0]X + [1] >= [0 0 0]X = d(proper(X)) 553.63/176.52 [0 0 1] [0] [0 0 1] 553.63/176.52 problem: 553.63/176.52 strict: 553.63/176.52 553.63/176.52 weak: 553.63/176.52 active(h(X)) -> h(active(X)) 553.63/176.52 f(mark(X)) -> mark(f(X)) 553.63/176.52 h(mark(X)) -> mark(h(X)) 553.63/176.52 proper(f(X)) -> f(proper(X)) 553.63/176.52 proper(h(X)) -> h(proper(X)) 553.63/176.52 active(f(X)) -> f(active(X)) 553.63/176.52 f(ok(X)) -> ok(f(X)) 553.63/176.52 c(ok(X)) -> ok(c(X)) 553.63/176.52 g(ok(X)) -> ok(g(X)) 553.63/176.52 d(ok(X)) -> ok(d(X)) 553.63/176.52 h(ok(X)) -> ok(h(X)) 553.63/176.52 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.52 active(c(X)) -> mark(d(X)) 553.63/176.52 active(h(X)) -> mark(c(d(X))) 553.63/176.52 top(mark(X)) -> top(proper(X)) 553.63/176.52 top(ok(X)) -> top(active(X)) 553.63/176.52 proper(c(X)) -> c(proper(X)) 553.63/176.52 proper(g(X)) -> g(proper(X)) 553.63/176.52 proper(d(X)) -> d(proper(X)) 553.63/176.52 Qed 553.63/176.52 553.63/176.52 strict: 553.63/176.52 proper(c(X)) -> c(proper(X)) 553.63/176.52 proper(g(X)) -> g(proper(X)) 553.63/176.52 proper(d(X)) -> d(proper(X)) 553.63/176.52 weak: 553.63/176.52 active(h(X)) -> h(active(X)) 553.63/176.52 f(mark(X)) -> mark(f(X)) 553.63/176.52 h(mark(X)) -> mark(h(X)) 553.63/176.52 proper(f(X)) -> f(proper(X)) 553.63/176.52 proper(h(X)) -> h(proper(X)) 553.63/176.52 active(f(X)) -> f(active(X)) 553.63/176.52 f(ok(X)) -> ok(f(X)) 553.63/176.52 c(ok(X)) -> ok(c(X)) 553.63/176.52 g(ok(X)) -> ok(g(X)) 553.63/176.52 d(ok(X)) -> ok(d(X)) 553.63/176.52 h(ok(X)) -> ok(h(X)) 553.63/176.52 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.52 active(c(X)) -> mark(d(X)) 553.63/176.52 active(h(X)) -> mark(c(d(X))) 553.63/176.52 top(mark(X)) -> top(proper(X)) 553.63/176.52 top(ok(X)) -> top(active(X)) 553.63/176.52 Splitting Processor: 553.63/176.52 strict: 553.63/176.52 proper(g(X)) -> g(proper(X)) 553.63/176.52 weak: 553.63/176.52 active(h(X)) -> h(active(X)) 553.63/176.52 f(mark(X)) -> mark(f(X)) 553.63/176.52 h(mark(X)) -> mark(h(X)) 553.63/176.52 proper(f(X)) -> f(proper(X)) 553.63/176.52 proper(h(X)) -> h(proper(X)) 553.63/176.52 active(f(X)) -> f(active(X)) 553.63/176.52 f(ok(X)) -> ok(f(X)) 553.63/176.52 c(ok(X)) -> ok(c(X)) 553.63/176.52 g(ok(X)) -> ok(g(X)) 553.63/176.52 d(ok(X)) -> ok(d(X)) 553.63/176.52 h(ok(X)) -> ok(h(X)) 553.63/176.52 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.52 active(c(X)) -> mark(d(X)) 553.63/176.52 active(h(X)) -> mark(c(d(X))) 553.63/176.52 top(mark(X)) -> top(proper(X)) 553.63/176.52 top(ok(X)) -> top(active(X)) 553.63/176.52 proper(c(X)) -> c(proper(X)) 553.63/176.52 proper(d(X)) -> d(proper(X)) 553.63/176.52 Splitting Processor: 553.63/176.52 strict: 553.63/176.52 proper(d(X)) -> d(proper(X)) 553.63/176.52 weak: 553.63/176.52 proper(g(X)) -> g(proper(X)) 553.63/176.52 active(h(X)) -> h(active(X)) 553.63/176.52 f(mark(X)) -> mark(f(X)) 553.63/176.52 h(mark(X)) -> mark(h(X)) 553.63/176.52 proper(f(X)) -> f(proper(X)) 553.63/176.52 proper(h(X)) -> h(proper(X)) 553.63/176.52 active(f(X)) -> f(active(X)) 553.63/176.52 f(ok(X)) -> ok(f(X)) 553.63/176.52 c(ok(X)) -> ok(c(X)) 553.63/176.52 g(ok(X)) -> ok(g(X)) 553.63/176.52 d(ok(X)) -> ok(d(X)) 553.63/176.52 h(ok(X)) -> ok(h(X)) 553.63/176.52 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.52 active(c(X)) -> mark(d(X)) 553.63/176.52 active(h(X)) -> mark(c(d(X))) 553.63/176.52 top(mark(X)) -> top(proper(X)) 553.63/176.53 top(ok(X)) -> top(active(X)) 553.63/176.53 proper(c(X)) -> c(proper(X)) 553.63/176.53 Matrix Interpretation Processor: dim=2 553.63/176.53 553.63/176.53 max_matrix: 553.63/176.53 [1 3] 553.63/176.53 [0 1] 553.63/176.53 interpretation: 553.63/176.53 [1 1] [1] 553.63/176.53 [top](x0) = [0 0]x0 + [0], 553.63/176.53 553.63/176.53 [1 2] [0] 553.63/176.53 [ok](x0) = [0 1]x0 + [2], 553.63/176.53 553.63/176.53 [1 1] 553.63/176.53 [proper](x0) = [0 1]x0, 553.63/176.53 553.63/176.53 [2] 553.63/176.53 [h](x0) = x0 + [0], 553.63/176.53 553.63/176.53 [1 1] [0] 553.63/176.53 [d](x0) = [0 1]x0 + [1], 553.63/176.53 553.63/176.53 [1 2] 553.63/176.53 [mark](x0) = [0 0]x0, 553.63/176.53 553.63/176.53 [1] 553.63/176.53 [c](x0) = x0 + [0], 553.63/176.53 553.63/176.53 [1 1] 553.63/176.53 [g](x0) = [0 1]x0, 553.63/176.53 553.63/176.53 [1 3] [1] 553.63/176.53 [active](x0) = [0 0]x0 + [0], 553.63/176.53 553.63/176.53 [1] 553.63/176.53 [f](x0) = x0 + [0] 553.63/176.53 orientation: 553.63/176.53 [1 2] [1] [1 2] [0] 553.63/176.53 proper(d(X)) = [0 1]X + [1] >= [0 1]X + [1] = d(proper(X)) 553.63/176.53 553.63/176.53 [1 2] [1 2] 553.63/176.53 proper(g(X)) = [0 1]X >= [0 1]X = g(proper(X)) 553.63/176.53 553.63/176.53 [1 3] [3] [1 3] [3] 553.63/176.53 active(h(X)) = [0 0]X + [0] >= [0 0]X + [0] = h(active(X)) 553.63/176.53 553.63/176.53 [1 2] [1] [1 2] [1] 553.63/176.53 f(mark(X)) = [0 0]X + [0] >= [0 0]X + [0] = mark(f(X)) 553.63/176.53 553.63/176.53 [1 2] [2] [1 2] [2] 553.63/176.53 h(mark(X)) = [0 0]X + [0] >= [0 0]X + [0] = mark(h(X)) 553.63/176.53 553.63/176.53 [1 1] [1] [1 1] [1] 553.63/176.53 proper(f(X)) = [0 1]X + [0] >= [0 1]X + [0] = f(proper(X)) 553.63/176.53 553.63/176.53 [1 1] [2] [1 1] [2] 553.63/176.53 proper(h(X)) = [0 1]X + [0] >= [0 1]X + [0] = h(proper(X)) 553.63/176.53 553.63/176.53 [1 3] [2] [1 3] [2] 553.63/176.53 active(f(X)) = [0 0]X + [0] >= [0 0]X + [0] = f(active(X)) 553.63/176.53 553.63/176.53 [1 2] [1] [1 2] [1] 553.63/176.53 f(ok(X)) = [0 1]X + [2] >= [0 1]X + [2] = ok(f(X)) 553.63/176.53 553.63/176.53 [1 2] [1] [1 2] [1] 553.63/176.53 c(ok(X)) = [0 1]X + [2] >= [0 1]X + [2] = ok(c(X)) 553.63/176.53 553.63/176.53 [1 3] [2] [1 3] [0] 553.63/176.53 g(ok(X)) = [0 1]X + [2] >= [0 1]X + [2] = ok(g(X)) 553.63/176.53 553.63/176.53 [1 3] [2] [1 3] [2] 553.63/176.53 d(ok(X)) = [0 1]X + [3] >= [0 1]X + [3] = ok(d(X)) 553.63/176.53 553.63/176.53 [1 2] [2] [1 2] [2] 553.63/176.53 h(ok(X)) = [0 1]X + [2] >= [0 1]X + [2] = ok(h(X)) 553.63/176.53 553.63/176.53 [1 3] [3] [1 3] [3] 553.63/176.53 active(f(f(X))) = [0 0]X + [0] >= [0 0]X + [0] = mark(c(f(g(f(X))))) 553.63/176.53 553.63/176.53 [1 3] [2] [1 3] [2] 553.63/176.53 active(c(X)) = [0 0]X + [0] >= [0 0]X + [0] = mark(d(X)) 553.63/176.53 553.63/176.53 [1 3] [3] [1 3] [3] 553.63/176.53 active(h(X)) = [0 0]X + [0] >= [0 0]X + [0] = mark(c(d(X))) 553.63/176.53 553.63/176.53 [1 2] [1] [1 2] [1] 553.63/176.53 top(mark(X)) = [0 0]X + [0] >= [0 0]X + [0] = top(proper(X)) 553.63/176.53 553.63/176.53 [1 3] [3] [1 3] [2] 553.63/176.53 top(ok(X)) = [0 0]X + [0] >= [0 0]X + [0] = top(active(X)) 553.63/176.53 553.63/176.53 [1 1] [1] [1 1] [1] 553.63/176.53 proper(c(X)) = [0 1]X + [0] >= [0 1]X + [0] = c(proper(X)) 553.63/176.53 problem: 553.63/176.53 strict: 553.63/176.53 553.63/176.53 weak: 553.63/176.53 proper(d(X)) -> d(proper(X)) 553.63/176.53 proper(g(X)) -> g(proper(X)) 553.63/176.53 active(h(X)) -> h(active(X)) 553.63/176.53 f(mark(X)) -> mark(f(X)) 553.63/176.53 h(mark(X)) -> mark(h(X)) 553.63/176.53 proper(f(X)) -> f(proper(X)) 553.63/176.53 proper(h(X)) -> h(proper(X)) 553.63/176.53 active(f(X)) -> f(active(X)) 553.63/176.53 f(ok(X)) -> ok(f(X)) 553.63/176.53 c(ok(X)) -> ok(c(X)) 553.63/176.53 g(ok(X)) -> ok(g(X)) 553.63/176.53 d(ok(X)) -> ok(d(X)) 553.63/176.53 h(ok(X)) -> ok(h(X)) 553.63/176.53 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.53 active(c(X)) -> mark(d(X)) 553.63/176.53 active(h(X)) -> mark(c(d(X))) 553.63/176.53 top(mark(X)) -> top(proper(X)) 553.63/176.53 top(ok(X)) -> top(active(X)) 553.63/176.53 proper(c(X)) -> c(proper(X)) 553.63/176.53 Qed 553.63/176.53 553.63/176.53 strict: 553.63/176.53 proper(c(X)) -> c(proper(X)) 553.63/176.53 weak: 553.63/176.53 proper(d(X)) -> d(proper(X)) 553.63/176.53 proper(g(X)) -> g(proper(X)) 553.63/176.53 active(h(X)) -> h(active(X)) 553.63/176.53 f(mark(X)) -> mark(f(X)) 553.63/176.53 h(mark(X)) -> mark(h(X)) 553.63/176.53 proper(f(X)) -> f(proper(X)) 553.63/176.53 proper(h(X)) -> h(proper(X)) 553.63/176.53 active(f(X)) -> f(active(X)) 553.63/176.53 f(ok(X)) -> ok(f(X)) 553.63/176.53 c(ok(X)) -> ok(c(X)) 553.63/176.53 g(ok(X)) -> ok(g(X)) 553.63/176.53 d(ok(X)) -> ok(d(X)) 553.63/176.53 h(ok(X)) -> ok(h(X)) 553.63/176.53 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.53 active(c(X)) -> mark(d(X)) 553.63/176.53 active(h(X)) -> mark(c(d(X))) 553.63/176.53 top(mark(X)) -> top(proper(X)) 553.63/176.53 top(ok(X)) -> top(active(X)) 553.63/176.53 Matrix Interpretation Processor: dim=2 553.63/176.53 553.63/176.53 max_matrix: 553.63/176.53 [1 2] 553.63/176.53 [0 1] 553.63/176.53 interpretation: 553.63/176.53 [1 0] 553.63/176.53 [top](x0) = [0 0]x0, 553.63/176.53 553.63/176.53 [1 2] [1] 553.63/176.53 [ok](x0) = [0 1]x0 + [2], 553.63/176.53 553.63/176.53 [1 1] 553.63/176.53 [proper](x0) = [0 1]x0, 553.63/176.53 553.63/176.53 553.63/176.53 [h](x0) = x0, 553.63/176.53 553.63/176.53 553.63/176.53 [d](x0) = x0, 553.63/176.53 553.63/176.53 [1 1] 553.63/176.53 [mark](x0) = [0 0]x0, 553.63/176.53 553.63/176.53 [1 1] [0] 553.63/176.53 [c](x0) = [0 1]x0 + [1], 553.63/176.53 553.63/176.53 553.63/176.53 [g](x0) = x0, 553.63/176.53 553.63/176.53 [1 2] [1] 553.63/176.53 [active](x0) = [0 0]x0 + [0], 553.63/176.53 553.63/176.53 553.63/176.53 [f](x0) = x0 553.63/176.53 orientation: 553.63/176.53 [1 2] [1] [1 2] [0] 553.63/176.53 proper(c(X)) = [0 1]X + [1] >= [0 1]X + [1] = c(proper(X)) 553.63/176.53 553.63/176.53 [1 1] [1 1] 553.63/176.53 proper(d(X)) = [0 1]X >= [0 1]X = d(proper(X)) 553.63/176.53 553.63/176.53 [1 1] [1 1] 553.63/176.53 proper(g(X)) = [0 1]X >= [0 1]X = g(proper(X)) 553.63/176.53 553.63/176.54 [1 2] [1] [1 2] [1] 553.63/176.54 active(h(X)) = [0 0]X + [0] >= [0 0]X + [0] = h(active(X)) 553.63/176.54 553.63/176.54 [1 1] [1 1] 553.63/176.54 f(mark(X)) = [0 0]X >= [0 0]X = mark(f(X)) 553.63/176.54 553.63/176.54 [1 1] [1 1] 553.63/176.54 h(mark(X)) = [0 0]X >= [0 0]X = mark(h(X)) 553.63/176.54 553.63/176.54 [1 1] [1 1] 553.63/176.54 proper(f(X)) = [0 1]X >= [0 1]X = f(proper(X)) 553.63/176.54 553.63/176.54 [1 1] [1 1] 553.63/176.54 proper(h(X)) = [0 1]X >= [0 1]X = h(proper(X)) 553.63/176.54 553.63/176.54 [1 2] [1] [1 2] [1] 553.63/176.54 active(f(X)) = [0 0]X + [0] >= [0 0]X + [0] = f(active(X)) 553.63/176.54 553.63/176.54 [1 2] [1] [1 2] [1] 553.63/176.54 f(ok(X)) = [0 1]X + [2] >= [0 1]X + [2] = ok(f(X)) 553.63/176.54 553.63/176.54 [1 3] [3] [1 3] [3] 553.63/176.54 c(ok(X)) = [0 1]X + [3] >= [0 1]X + [3] = ok(c(X)) 553.63/176.54 553.63/176.54 [1 2] [1] [1 2] [1] 553.63/176.54 g(ok(X)) = [0 1]X + [2] >= [0 1]X + [2] = ok(g(X)) 553.63/176.54 553.63/176.54 [1 2] [1] [1 2] [1] 553.63/176.54 d(ok(X)) = [0 1]X + [2] >= [0 1]X + [2] = ok(d(X)) 553.63/176.54 553.63/176.54 [1 2] [1] [1 2] [1] 553.63/176.54 h(ok(X)) = [0 1]X + [2] >= [0 1]X + [2] = ok(h(X)) 553.63/176.54 553.63/176.54 [1 2] [1] [1 2] [1] 553.63/176.54 active(f(f(X))) = [0 0]X + [0] >= [0 0]X + [0] = mark(c(f(g(f(X))))) 553.63/176.54 553.63/176.54 [1 3] [3] [1 1] 553.63/176.54 active(c(X)) = [0 0]X + [0] >= [0 0]X = mark(d(X)) 553.63/176.54 553.63/176.54 [1 2] [1] [1 2] [1] 553.63/176.54 active(h(X)) = [0 0]X + [0] >= [0 0]X + [0] = mark(c(d(X))) 553.63/176.54 553.63/176.54 [1 1] [1 1] 553.63/176.54 top(mark(X)) = [0 0]X >= [0 0]X = top(proper(X)) 553.63/176.54 553.63/176.54 [1 2] [1] [1 2] [1] 553.63/176.54 top(ok(X)) = [0 0]X + [0] >= [0 0]X + [0] = top(active(X)) 553.63/176.54 problem: 553.63/176.54 strict: 553.63/176.54 553.63/176.54 weak: 553.63/176.54 proper(c(X)) -> c(proper(X)) 553.63/176.54 proper(d(X)) -> d(proper(X)) 553.63/176.54 proper(g(X)) -> g(proper(X)) 553.63/176.54 active(h(X)) -> h(active(X)) 553.63/176.54 f(mark(X)) -> mark(f(X)) 553.63/176.54 h(mark(X)) -> mark(h(X)) 553.63/176.54 proper(f(X)) -> f(proper(X)) 553.63/176.54 proper(h(X)) -> h(proper(X)) 553.63/176.54 active(f(X)) -> f(active(X)) 553.63/176.54 f(ok(X)) -> ok(f(X)) 553.63/176.54 c(ok(X)) -> ok(c(X)) 553.63/176.54 g(ok(X)) -> ok(g(X)) 553.63/176.54 d(ok(X)) -> ok(d(X)) 553.63/176.54 h(ok(X)) -> ok(h(X)) 553.63/176.54 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.54 active(c(X)) -> mark(d(X)) 553.63/176.54 active(h(X)) -> mark(c(d(X))) 553.63/176.54 top(mark(X)) -> top(proper(X)) 553.63/176.54 top(ok(X)) -> top(active(X)) 553.63/176.54 Qed 553.63/176.54 553.63/176.54 strict: 553.63/176.54 proper(c(X)) -> c(proper(X)) 553.63/176.54 proper(d(X)) -> d(proper(X)) 553.63/176.54 weak: 553.63/176.54 proper(g(X)) -> g(proper(X)) 553.63/176.54 active(h(X)) -> h(active(X)) 553.63/176.54 f(mark(X)) -> mark(f(X)) 553.63/176.54 h(mark(X)) -> mark(h(X)) 553.63/176.54 proper(f(X)) -> f(proper(X)) 553.63/176.54 proper(h(X)) -> h(proper(X)) 553.63/176.54 active(f(X)) -> f(active(X)) 553.63/176.54 f(ok(X)) -> ok(f(X)) 553.63/176.54 c(ok(X)) -> ok(c(X)) 553.63/176.54 g(ok(X)) -> ok(g(X)) 553.63/176.54 d(ok(X)) -> ok(d(X)) 553.63/176.54 h(ok(X)) -> ok(h(X)) 553.63/176.54 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.54 active(c(X)) -> mark(d(X)) 553.63/176.54 active(h(X)) -> mark(c(d(X))) 553.63/176.54 top(mark(X)) -> top(proper(X)) 553.63/176.54 top(ok(X)) -> top(active(X)) 553.63/176.54 Matrix Interpretation Processor: dim=2 553.63/176.54 553.63/176.54 max_matrix: 553.63/176.54 [1 3] 553.63/176.54 [0 1] 553.63/176.54 interpretation: 553.63/176.54 [1 1] 553.63/176.54 [top](x0) = [0 0]x0, 553.63/176.54 553.63/176.54 [1 3] [0] 553.63/176.54 [ok](x0) = [0 1]x0 + [3], 553.63/176.54 553.63/176.54 [1 1] 553.63/176.54 [proper](x0) = [0 1]x0, 553.63/176.54 553.63/176.54 [1] 553.63/176.54 [h](x0) = x0 + [0], 553.63/176.54 553.63/176.54 [2] 553.63/176.54 [d](x0) = x0 + [0], 553.63/176.54 553.63/176.54 [1 2] [0] 553.63/176.54 [mark](x0) = [0 0]x0 + [1], 553.63/176.54 553.63/176.54 553.63/176.54 [c](x0) = x0, 553.63/176.54 553.63/176.54 [1 1] [0] 553.63/176.54 [g](x0) = [0 1]x0 + [1], 553.63/176.54 553.63/176.54 [1 3] [2] 553.63/176.54 [active](x0) = [0 1]x0 + [1], 553.63/176.54 553.63/176.54 553.63/176.54 [f](x0) = x0 553.63/176.54 orientation: 553.63/176.54 [1 2] [1] [1 2] [0] 553.63/176.54 proper(g(X)) = [0 1]X + [1] >= [0 1]X + [1] = g(proper(X)) 553.63/176.54 553.63/176.54 [1 3] [3] [1 3] [3] 553.63/176.54 active(h(X)) = [0 1]X + [1] >= [0 1]X + [1] = h(active(X)) 553.63/176.54 553.63/176.54 [1 2] [0] [1 2] [0] 553.63/176.54 f(mark(X)) = [0 0]X + [1] >= [0 0]X + [1] = mark(f(X)) 553.63/176.54 553.63/176.54 [1 2] [1] [1 2] [1] 553.63/176.54 h(mark(X)) = [0 0]X + [1] >= [0 0]X + [1] = mark(h(X)) 553.63/176.54 553.63/176.54 [1 1] [1 1] 553.63/176.54 proper(f(X)) = [0 1]X >= [0 1]X = f(proper(X)) 553.63/176.54 553.63/176.54 [1 1] [1] [1 1] [1] 553.63/176.54 proper(h(X)) = [0 1]X + [0] >= [0 1]X + [0] = h(proper(X)) 553.63/176.54 553.63/176.54 [1 3] [2] [1 3] [2] 553.63/176.54 active(f(X)) = [0 1]X + [1] >= [0 1]X + [1] = f(active(X)) 553.63/176.54 553.63/176.54 [1 3] [0] [1 3] [0] 553.63/176.54 f(ok(X)) = [0 1]X + [3] >= [0 1]X + [3] = ok(f(X)) 553.63/176.54 553.63/176.54 [1 3] [0] [1 3] [0] 553.63/176.54 c(ok(X)) = [0 1]X + [3] >= [0 1]X + [3] = ok(c(X)) 553.63/176.54 553.63/176.54 [1 4] [3] [1 4] [3] 553.63/176.54 g(ok(X)) = [0 1]X + [4] >= [0 1]X + [4] = ok(g(X)) 553.63/176.54 553.63/176.54 [1 3] [2] [1 3] [2] 553.63/176.54 d(ok(X)) = [0 1]X + [3] >= [0 1]X + [3] = ok(d(X)) 553.63/176.54 553.63/176.54 [1 3] [1] [1 3] [1] 553.63/176.54 h(ok(X)) = [0 1]X + [3] >= [0 1]X + [3] = ok(h(X)) 553.63/176.54 553.63/176.54 [1 3] [2] [1 3] [2] 553.63/176.54 active(f(f(X))) = [0 1]X + [1] >= [0 0]X + [1] = mark(c(f(g(f(X))))) 553.63/176.54 553.63/176.54 [1 3] [2] [1 2] [2] 553.63/176.54 active(c(X)) = [0 1]X + [1] >= [0 0]X + [1] = mark(d(X)) 553.63/176.54 553.63/176.54 [1 3] [3] [1 2] [2] 553.63/176.54 active(h(X)) = [0 1]X + [1] >= [0 0]X + [1] = mark(c(d(X))) 553.63/176.54 553.63/176.54 [1 2] [1] [1 2] 553.63/176.54 top(mark(X)) = [0 0]X + [0] >= [0 0]X = top(proper(X)) 553.63/176.54 553.63/176.54 [1 4] [3] [1 4] [3] 553.63/176.54 top(ok(X)) = [0 0]X + [0] >= [0 0]X + [0] = top(active(X)) 553.63/176.54 553.63/176.54 [1 1] [1 1] 553.63/176.54 proper(c(X)) = [0 1]X >= [0 1]X = c(proper(X)) 553.63/176.54 553.63/176.54 [1 1] [2] [1 1] [2] 553.63/176.54 proper(d(X)) = [0 1]X + [0] >= [0 1]X + [0] = d(proper(X)) 553.63/176.54 problem: 553.63/176.54 strict: 553.63/176.54 553.63/176.54 weak: 553.63/176.54 proper(g(X)) -> g(proper(X)) 553.63/176.54 active(h(X)) -> h(active(X)) 553.63/176.54 f(mark(X)) -> mark(f(X)) 553.63/176.54 h(mark(X)) -> mark(h(X)) 553.63/176.54 proper(f(X)) -> f(proper(X)) 553.63/176.54 proper(h(X)) -> h(proper(X)) 553.63/176.54 active(f(X)) -> f(active(X)) 553.63/176.54 f(ok(X)) -> ok(f(X)) 553.63/176.54 c(ok(X)) -> ok(c(X)) 553.63/176.54 g(ok(X)) -> ok(g(X)) 553.63/176.54 d(ok(X)) -> ok(d(X)) 553.63/176.54 h(ok(X)) -> ok(h(X)) 553.63/176.54 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.54 active(c(X)) -> mark(d(X)) 553.63/176.54 active(h(X)) -> mark(c(d(X))) 553.63/176.54 top(mark(X)) -> top(proper(X)) 553.63/176.54 top(ok(X)) -> top(active(X)) 553.63/176.54 proper(c(X)) -> c(proper(X)) 553.63/176.54 proper(d(X)) -> d(proper(X)) 553.63/176.54 Qed 553.63/176.54 553.63/176.54 strict: 553.63/176.54 active(h(X)) -> h(active(X)) 553.63/176.54 proper(c(X)) -> c(proper(X)) 553.63/176.54 proper(g(X)) -> g(proper(X)) 553.63/176.54 proper(d(X)) -> d(proper(X)) 553.63/176.54 weak: 553.63/176.54 f(mark(X)) -> mark(f(X)) 553.63/176.54 h(mark(X)) -> mark(h(X)) 553.63/176.54 proper(f(X)) -> f(proper(X)) 553.63/176.54 proper(h(X)) -> h(proper(X)) 553.63/176.54 active(f(X)) -> f(active(X)) 553.63/176.54 f(ok(X)) -> ok(f(X)) 553.63/176.54 c(ok(X)) -> ok(c(X)) 553.63/176.54 g(ok(X)) -> ok(g(X)) 553.63/176.54 d(ok(X)) -> ok(d(X)) 553.63/176.54 h(ok(X)) -> ok(h(X)) 553.63/176.54 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.54 active(c(X)) -> mark(d(X)) 553.63/176.54 active(h(X)) -> mark(c(d(X))) 553.63/176.54 top(mark(X)) -> top(proper(X)) 553.63/176.54 top(ok(X)) -> top(active(X)) 553.63/176.54 Matrix Interpretation Processor: dim=3 553.63/176.54 553.63/176.54 max_matrix: 553.63/176.54 [1 1 0] 553.63/176.54 [0 1 1] 553.63/176.54 [0 0 0] 553.63/176.54 interpretation: 553.63/176.54 [1 1 0] [1] 553.63/176.54 [top](x0) = [0 0 0]x0 + [0] 553.63/176.54 [0 0 0] [0], 553.63/176.54 553.63/176.54 [1 1 0] [1] 553.63/176.54 [ok](x0) = [0 1 1]x0 + [1] 553.63/176.54 [0 0 0] [0], 553.63/176.54 553.63/176.54 [1 0 0] [0] 553.63/176.54 [proper](x0) = [0 1 0]x0 + [0] 553.63/176.54 [0 0 0] [1], 553.63/176.54 553.63/176.54 [1 0 0] 553.63/176.54 [h](x0) = [0 1 0]x0 553.63/176.54 [0 0 0] , 553.63/176.54 553.63/176.54 [1 0 0] 553.63/176.54 [d](x0) = [0 1 0]x0 553.63/176.54 [0 0 0] , 553.63/176.54 553.63/176.54 [1 0 0] [0] 553.63/176.54 [mark](x0) = [0 1 0]x0 + [1] 553.63/176.54 [0 0 0] [0], 553.63/176.54 553.63/176.54 [1 0 0] 553.63/176.54 [c](x0) = [0 1 0]x0 553.63/176.54 [0 0 0] , 553.63/176.54 553.63/176.54 [1 1 0] 553.63/176.54 [g](x0) = [0 1 0]x0 553.63/176.54 [0 0 0] , 553.63/176.54 553.63/176.54 [1 1 0] [0] 553.63/176.54 [active](x0) = [0 1 0]x0 + [1] 553.63/176.54 [0 0 0] [0], 553.63/176.54 553.63/176.54 [1 1 0] [0] 553.63/176.54 [f](x0) = [0 1 0]x0 + [1] 553.63/176.54 [0 0 0] [0] 553.63/176.54 orientation: 553.63/176.55 [1 1 0] [1] [1 1 0] [0] 553.63/176.55 f(mark(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = mark(f(X)) 553.63/176.55 [0 0 0] [0] [0 0 0] [0] 553.63/176.55 553.63/176.55 [1 0 0] [0] [1 0 0] [0] 553.63/176.55 h(mark(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = mark(h(X)) 553.63/176.55 [0 0 0] [0] [0 0 0] [0] 553.63/176.55 553.63/176.55 [1 1 0] [0] [1 1 0] [0] 553.63/176.55 proper(f(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = f(proper(X)) 553.63/176.55 [0 0 0] [1] [0 0 0] [0] 553.63/176.55 553.63/176.55 [1 0 0] [0] [1 0 0] 553.63/176.55 proper(h(X)) = [0 1 0]X + [0] >= [0 1 0]X = h(proper(X)) 553.63/176.55 [0 0 0] [1] [0 0 0] 553.63/176.55 553.63/176.55 [1 2 0] [1] [1 2 0] [1] 553.63/176.55 active(f(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = f(active(X)) 553.63/176.55 [0 0 0] [0] [0 0 0] [0] 553.63/176.55 553.63/176.55 [1 2 1] [2] [1 2 0] [2] 553.63/176.55 f(ok(X)) = [0 1 1]X + [2] >= [0 1 0]X + [2] = ok(f(X)) 553.63/176.55 [0 0 0] [0] [0 0 0] [0] 553.63/176.55 553.63/176.55 [1 1 0] [1] [1 1 0] [1] 553.63/176.55 c(ok(X)) = [0 1 1]X + [1] >= [0 1 0]X + [1] = ok(c(X)) 553.63/176.55 [0 0 0] [0] [0 0 0] [0] 553.63/176.55 553.63/176.55 [1 2 1] [2] [1 2 0] [1] 553.63/176.55 g(ok(X)) = [0 1 1]X + [1] >= [0 1 0]X + [1] = ok(g(X)) 553.63/176.55 [0 0 0] [0] [0 0 0] [0] 553.63/176.55 553.63/176.55 [1 1 0] [1] [1 1 0] [1] 553.63/176.55 d(ok(X)) = [0 1 1]X + [1] >= [0 1 0]X + [1] = ok(d(X)) 553.63/176.55 [0 0 0] [0] [0 0 0] [0] 553.63/176.55 553.63/176.55 [1 1 0] [1] [1 1 0] [1] 553.63/176.55 h(ok(X)) = [0 1 1]X + [1] >= [0 1 0]X + [1] = ok(h(X)) 553.63/176.55 [0 0 0] [0] [0 0 0] [0] 553.63/176.55 553.63/176.55 [1 3 0] [3] [1 3 0] [2] 553.63/176.55 active(f(f(X))) = [0 1 0]X + [3] >= [0 1 0]X + [3] = mark(c(f(g(f(X))))) 553.63/176.55 [0 0 0] [0] [0 0 0] [0] 553.63/176.55 553.63/176.55 [1 1 0] [0] [1 0 0] [0] 553.63/176.55 active(c(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = mark(d(X)) 553.63/176.55 [0 0 0] [0] [0 0 0] [0] 553.63/176.55 553.63/176.55 [1 1 0] [0] [1 0 0] [0] 553.63/176.55 active(h(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = mark(c(d(X))) 553.63/176.55 [0 0 0] [0] [0 0 0] [0] 553.63/176.55 553.63/176.55 [1 1 0] [2] [1 1 0] [1] 553.63/176.55 top(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = top(proper(X)) 553.63/176.55 [0 0 0] [0] [0 0 0] [0] 553.63/176.55 553.63/176.55 [1 2 1] [3] [1 2 0] [2] 553.63/176.55 top(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = top(active(X)) 553.63/176.55 [0 0 0] [0] [0 0 0] [0] 553.63/176.55 553.63/176.55 [1 1 0] [0] [1 1 0] [0] 553.63/176.55 active(h(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = h(active(X)) 553.63/176.55 [0 0 0] [0] [0 0 0] [0] 553.63/176.55 553.63/176.55 [1 0 0] [0] [1 0 0] 553.63/176.55 proper(c(X)) = [0 1 0]X + [0] >= [0 1 0]X = c(proper(X)) 553.63/176.55 [0 0 0] [1] [0 0 0] 553.63/176.55 553.63/176.55 [1 1 0] [0] [1 1 0] 553.63/176.55 proper(g(X)) = [0 1 0]X + [0] >= [0 1 0]X = g(proper(X)) 553.63/176.55 [0 0 0] [1] [0 0 0] 553.63/176.55 553.63/176.55 [1 0 0] [0] [1 0 0] 553.63/176.55 proper(d(X)) = [0 1 0]X + [0] >= [0 1 0]X = d(proper(X)) 553.63/176.55 [0 0 0] [1] [0 0 0] 553.63/176.55 problem: 553.63/176.55 strict: 553.63/176.55 553.63/176.55 weak: 553.63/176.55 f(mark(X)) -> mark(f(X)) 553.63/176.55 h(mark(X)) -> mark(h(X)) 553.63/176.55 proper(f(X)) -> f(proper(X)) 553.63/176.55 proper(h(X)) -> h(proper(X)) 553.63/176.55 active(f(X)) -> f(active(X)) 553.63/176.55 f(ok(X)) -> ok(f(X)) 553.63/176.55 c(ok(X)) -> ok(c(X)) 553.63/176.55 g(ok(X)) -> ok(g(X)) 553.63/176.55 d(ok(X)) -> ok(d(X)) 553.63/176.55 h(ok(X)) -> ok(h(X)) 553.63/176.55 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.55 active(c(X)) -> mark(d(X)) 553.63/176.55 active(h(X)) -> mark(c(d(X))) 553.63/176.55 top(mark(X)) -> top(proper(X)) 553.63/176.55 top(ok(X)) -> top(active(X)) 553.63/176.55 active(h(X)) -> h(active(X)) 553.63/176.55 proper(c(X)) -> c(proper(X)) 553.63/176.55 proper(g(X)) -> g(proper(X)) 553.63/176.55 proper(d(X)) -> d(proper(X)) 553.63/176.55 Qed 553.63/176.55 553.63/176.55 strict: 553.63/176.55 active(h(X)) -> h(active(X)) 553.63/176.55 f(mark(X)) -> mark(f(X)) 553.63/176.55 h(mark(X)) -> mark(h(X)) 553.63/176.55 proper(c(X)) -> c(proper(X)) 553.63/176.55 proper(g(X)) -> g(proper(X)) 553.63/176.55 proper(d(X)) -> d(proper(X)) 553.63/176.55 weak: 553.63/176.55 proper(f(X)) -> f(proper(X)) 553.63/176.55 proper(h(X)) -> h(proper(X)) 553.63/176.55 active(f(X)) -> f(active(X)) 553.63/176.55 f(ok(X)) -> ok(f(X)) 553.63/176.55 c(ok(X)) -> ok(c(X)) 553.63/176.55 g(ok(X)) -> ok(g(X)) 553.63/176.55 d(ok(X)) -> ok(d(X)) 553.63/176.55 h(ok(X)) -> ok(h(X)) 553.63/176.55 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.55 active(c(X)) -> mark(d(X)) 553.63/176.55 active(h(X)) -> mark(c(d(X))) 553.63/176.55 top(mark(X)) -> top(proper(X)) 553.63/176.55 top(ok(X)) -> top(active(X)) 553.63/176.55 Matrix Interpretation Processor: dim=3 553.63/176.55 553.63/176.55 max_matrix: 553.63/176.55 [1 1 0] 553.63/176.55 [0 1 0] 553.63/176.55 [0 0 0] 553.63/176.55 interpretation: 553.63/176.55 [1 1 0] [1] 553.63/176.55 [top](x0) = [0 0 0]x0 + [0] 553.63/176.55 [0 0 0] [0], 553.63/176.55 553.63/176.55 [1 1 0] [0] 553.63/176.55 [ok](x0) = [0 1 0]x0 + [1] 553.63/176.55 [0 0 0] [0], 553.63/176.55 553.63/176.55 [1 1 0] [1] 553.63/176.55 [proper](x0) = [0 1 0]x0 + [0] 553.63/176.55 [0 0 0] [1], 553.63/176.55 553.63/176.55 [1 1 0] [0] 553.63/176.55 [h](x0) = [0 1 0]x0 + [1] 553.63/176.55 [0 0 0] [1], 553.63/176.55 553.63/176.55 [1 0 0] 553.63/176.55 [d](x0) = [0 1 0]x0 553.63/176.55 [0 0 0] , 553.63/176.55 553.63/176.55 [1 1 0] [0] 553.63/176.55 [mark](x0) = [0 1 0]x0 + [1] 553.63/176.55 [0 0 0] [0], 553.63/176.55 553.63/176.55 [1 0 0] 553.63/176.55 [c](x0) = [0 1 0]x0 553.63/176.55 [0 0 0] , 553.63/176.55 553.63/176.55 [1 0 0] 553.63/176.55 [g](x0) = [0 1 0]x0 553.63/176.55 [0 0 0] , 553.63/176.55 553.63/176.55 [1 1 0] [0] 553.63/176.55 [active](x0) = [0 1 0]x0 + [1] 553.63/176.55 [0 0 0] [1], 553.63/176.55 553.63/176.55 [1 1 0] [0] 553.63/176.55 [f](x0) = [0 1 0]x0 + [1] 553.63/176.55 [0 0 0] [0] 553.63/176.55 orientation: 553.63/176.55 [1 2 0] [2] [1 2 0] [1] 553.63/176.55 proper(f(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = f(proper(X)) 553.63/176.55 [0 0 0] [1] [0 0 0] [0] 553.63/176.55 553.63/176.55 [1 2 0] [2] [1 2 0] [1] 553.63/176.56 proper(h(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = h(proper(X)) 553.63/176.56 [0 0 0] [1] [0 0 0] [1] 553.63/176.56 553.63/176.56 [1 2 0] [1] [1 2 0] [1] 553.63/176.56 active(f(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = f(active(X)) 553.63/176.56 [0 0 0] [1] [0 0 0] [0] 553.63/176.56 553.63/176.56 [1 2 0] [1] [1 2 0] [1] 553.63/176.56 f(ok(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = ok(f(X)) 553.63/176.56 [0 0 0] [0] [0 0 0] [0] 553.63/176.56 553.63/176.56 [1 1 0] [0] [1 1 0] [0] 553.63/176.56 c(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(c(X)) 553.63/176.56 [0 0 0] [0] [0 0 0] [0] 553.63/176.56 553.63/176.56 [1 1 0] [0] [1 1 0] [0] 553.63/176.56 g(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(g(X)) 553.63/176.56 [0 0 0] [0] [0 0 0] [0] 553.63/176.56 553.63/176.56 [1 1 0] [0] [1 1 0] [0] 553.63/176.56 d(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(d(X)) 553.63/176.56 [0 0 0] [0] [0 0 0] [0] 553.63/176.56 553.63/176.56 [1 2 0] [1] [1 2 0] [1] 553.63/176.56 h(ok(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = ok(h(X)) 553.63/176.56 [0 0 0] [1] [0 0 0] [0] 553.63/176.56 553.63/176.56 [1 3 0] [3] [1 3 0] [3] 553.63/176.56 active(f(f(X))) = [0 1 0]X + [3] >= [0 1 0]X + [3] = mark(c(f(g(f(X))))) 553.63/176.56 [0 0 0] [1] [0 0 0] [0] 553.63/176.56 553.63/176.56 [1 1 0] [0] [1 1 0] [0] 553.63/176.56 active(c(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = mark(d(X)) 553.63/176.56 [0 0 0] [1] [0 0 0] [0] 553.63/176.56 553.63/176.56 [1 2 0] [1] [1 1 0] [0] 553.63/176.56 active(h(X)) = [0 1 0]X + [2] >= [0 1 0]X + [1] = mark(c(d(X))) 553.63/176.56 [0 0 0] [1] [0 0 0] [0] 553.63/176.56 553.63/176.56 [1 2 0] [2] [1 2 0] [2] 553.63/176.56 top(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = top(proper(X)) 553.63/176.56 [0 0 0] [0] [0 0 0] [0] 553.63/176.56 553.63/176.56 [1 2 0] [2] [1 2 0] [2] 553.63/176.56 top(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = top(active(X)) 553.63/176.56 [0 0 0] [0] [0 0 0] [0] 553.63/176.56 553.63/176.56 [1 2 0] [1] [1 2 0] [1] 553.63/176.56 active(h(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = h(active(X)) 553.63/176.56 [0 0 0] [1] [0 0 0] [1] 553.63/176.56 553.63/176.56 [1 2 0] [1] [1 2 0] [1] 553.63/176.56 f(mark(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = mark(f(X)) 553.63/176.56 [0 0 0] [0] [0 0 0] [0] 553.63/176.56 553.63/176.56 [1 2 0] [1] [1 2 0] [1] 553.63/176.56 h(mark(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = mark(h(X)) 553.63/176.56 [0 0 0] [1] [0 0 0] [0] 553.63/176.56 553.63/176.56 [1 1 0] [1] [1 1 0] [1] 553.63/176.56 proper(c(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = c(proper(X)) 553.63/176.56 [0 0 0] [1] [0 0 0] [0] 553.63/176.56 553.63/176.56 [1 1 0] [1] [1 1 0] [1] 553.63/176.56 proper(g(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = g(proper(X)) 553.63/176.56 [0 0 0] [1] [0 0 0] [0] 553.63/176.56 553.63/176.56 [1 1 0] [1] [1 1 0] [1] 553.63/176.56 proper(d(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = d(proper(X)) 553.63/176.56 [0 0 0] [1] [0 0 0] [0] 553.63/176.56 problem: 553.63/176.56 strict: 553.63/176.56 553.63/176.56 weak: 553.63/176.56 proper(f(X)) -> f(proper(X)) 553.63/176.56 proper(h(X)) -> h(proper(X)) 553.63/176.56 active(f(X)) -> f(active(X)) 553.63/176.56 f(ok(X)) -> ok(f(X)) 553.63/176.56 c(ok(X)) -> ok(c(X)) 553.63/176.56 g(ok(X)) -> ok(g(X)) 553.63/176.56 d(ok(X)) -> ok(d(X)) 553.63/176.56 h(ok(X)) -> ok(h(X)) 553.63/176.56 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.56 active(c(X)) -> mark(d(X)) 553.63/176.56 active(h(X)) -> mark(c(d(X))) 553.63/176.56 top(mark(X)) -> top(proper(X)) 553.63/176.56 top(ok(X)) -> top(active(X)) 553.63/176.56 active(h(X)) -> h(active(X)) 553.63/176.56 f(mark(X)) -> mark(f(X)) 553.63/176.56 h(mark(X)) -> mark(h(X)) 553.63/176.56 proper(c(X)) -> c(proper(X)) 553.63/176.56 proper(g(X)) -> g(proper(X)) 553.63/176.56 proper(d(X)) -> d(proper(X)) 553.63/176.56 Qed 553.63/176.56 553.63/176.56 strict: 553.63/176.56 active(h(X)) -> h(active(X)) 553.63/176.56 f(mark(X)) -> mark(f(X)) 553.63/176.56 h(mark(X)) -> mark(h(X)) 553.63/176.56 proper(f(X)) -> f(proper(X)) 553.63/176.56 proper(c(X)) -> c(proper(X)) 553.63/176.56 proper(g(X)) -> g(proper(X)) 553.63/176.56 proper(d(X)) -> d(proper(X)) 553.63/176.56 proper(h(X)) -> h(proper(X)) 553.63/176.56 weak: 553.63/176.56 active(f(X)) -> f(active(X)) 553.63/176.56 f(ok(X)) -> ok(f(X)) 553.63/176.56 c(ok(X)) -> ok(c(X)) 553.63/176.56 g(ok(X)) -> ok(g(X)) 553.63/176.56 d(ok(X)) -> ok(d(X)) 553.63/176.56 h(ok(X)) -> ok(h(X)) 553.63/176.56 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.56 active(c(X)) -> mark(d(X)) 553.63/176.56 active(h(X)) -> mark(c(d(X))) 553.63/176.56 top(mark(X)) -> top(proper(X)) 553.63/176.56 top(ok(X)) -> top(active(X)) 553.63/176.56 Matrix Interpretation Processor: dim=3 553.63/176.56 553.63/176.56 max_matrix: 553.63/176.56 [1 0 1] 553.63/176.56 [0 0 0] 553.63/176.56 [0 0 1] 553.63/176.56 interpretation: 553.63/176.56 [1 0 0] 553.63/176.56 [top](x0) = [0 0 0]x0 553.63/176.56 [0 0 0] , 553.63/176.56 553.63/176.56 [1 0 1] [0] 553.63/176.56 [ok](x0) = [0 0 0]x0 + [0] 553.63/176.56 [0 0 1] [1], 553.63/176.56 553.63/176.56 [1 0 0] 553.63/176.56 [proper](x0) = [0 0 0]x0 553.63/176.56 [0 0 1] , 553.63/176.56 553.63/176.56 [1 0 0] [1] 553.63/176.56 [h](x0) = [0 0 0]x0 + [0] 553.63/176.56 [0 0 1] [0], 553.63/176.56 553.63/176.56 [1 0 1] 553.63/176.56 [d](x0) = [0 0 0]x0 553.63/176.56 [0 0 1] , 553.63/176.56 553.63/176.56 [1 0 0] 553.63/176.56 [mark](x0) = [0 0 0]x0 553.63/176.56 [0 0 1] , 553.63/176.56 553.63/176.56 [1 0 0] 553.63/176.56 [c](x0) = [0 0 0]x0 553.63/176.56 [0 0 1] , 553.63/176.56 553.63/176.56 [1 0 0] 553.63/176.56 [g](x0) = [0 0 0]x0 553.63/176.56 [0 0 1] , 553.63/176.56 553.63/176.56 [1 0 1] 553.63/176.56 [active](x0) = [0 0 0]x0 553.63/176.56 [0 0 1] , 553.63/176.56 553.63/176.56 [1 0 1] [0] 553.63/176.56 [f](x0) = [0 0 0]x0 + [0] 553.63/176.56 [0 0 1] [1] 553.63/176.56 orientation: 553.63/176.56 [1 0 2] [1] [1 0 2] [0] 553.63/176.56 active(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(active(X)) 553.63/176.56 [0 0 1] [1] [0 0 1] [1] 553.63/176.56 553.63/176.56 [1 0 2] [1] [1 0 2] [1] 553.63/176.56 f(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(f(X)) 553.63/176.56 [0 0 1] [2] [0 0 1] [2] 553.63/176.56 553.63/176.56 [1 0 1] [0] [1 0 1] [0] 553.63/176.56 c(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(c(X)) 553.63/176.56 [0 0 1] [1] [0 0 1] [1] 553.63/176.56 553.63/176.56 [1 0 1] [0] [1 0 1] [0] 553.63/176.56 g(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(g(X)) 553.63/176.56 [0 0 1] [1] [0 0 1] [1] 553.63/176.57 553.63/176.57 [1 0 2] [1] [1 0 2] [0] 553.63/176.57 d(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(d(X)) 553.63/176.57 [0 0 1] [1] [0 0 1] [1] 553.63/176.57 553.63/176.57 [1 0 1] [1] [1 0 1] [1] 553.63/176.57 h(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(h(X)) 553.63/176.57 [0 0 1] [1] [0 0 1] [1] 553.63/176.57 553.63/176.57 [1 0 3] [3] [1 0 2] [1] 553.63/176.57 active(f(f(X))) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(c(f(g(f(X))))) 553.63/176.57 [0 0 1] [2] [0 0 1] [2] 553.63/176.57 553.63/176.57 [1 0 1] [1 0 1] 553.63/176.57 active(c(X)) = [0 0 0]X >= [0 0 0]X = mark(d(X)) 553.63/176.57 [0 0 1] [0 0 1] 553.63/176.57 553.63/176.57 [1 0 1] [1] [1 0 1] 553.63/176.57 active(h(X)) = [0 0 0]X + [0] >= [0 0 0]X = mark(c(d(X))) 553.63/176.57 [0 0 1] [0] [0 0 1] 553.63/176.57 553.63/176.57 [1 0 0] [1 0 0] 553.63/176.57 top(mark(X)) = [0 0 0]X >= [0 0 0]X = top(proper(X)) 553.63/176.57 [0 0 0] [0 0 0] 553.63/176.57 553.63/176.57 [1 0 1] [1 0 1] 553.63/176.57 top(ok(X)) = [0 0 0]X >= [0 0 0]X = top(active(X)) 553.63/176.57 [0 0 0] [0 0 0] 553.63/176.57 553.63/176.57 [1 0 1] [1] [1 0 1] [1] 553.63/176.57 active(h(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = h(active(X)) 553.63/176.57 [0 0 1] [0] [0 0 1] [0] 553.63/176.57 553.63/176.57 [1 0 1] [0] [1 0 1] [0] 553.63/176.57 f(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(f(X)) 553.63/176.57 [0 0 1] [1] [0 0 1] [1] 553.63/176.57 553.63/176.57 [1 0 0] [1] [1 0 0] [1] 553.63/176.57 h(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(h(X)) 553.63/176.57 [0 0 1] [0] [0 0 1] [0] 553.63/176.57 553.63/176.57 [1 0 1] [0] [1 0 1] [0] 553.63/176.57 proper(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(proper(X)) 553.63/176.57 [0 0 1] [1] [0 0 1] [1] 553.63/176.57 553.63/176.57 [1 0 0] [1 0 0] 553.63/176.57 proper(c(X)) = [0 0 0]X >= [0 0 0]X = c(proper(X)) 553.63/176.57 [0 0 1] [0 0 1] 553.63/176.57 553.63/176.57 [1 0 0] [1 0 0] 553.63/176.57 proper(g(X)) = [0 0 0]X >= [0 0 0]X = g(proper(X)) 553.63/176.57 [0 0 1] [0 0 1] 553.63/176.57 553.63/176.57 [1 0 1] [1 0 1] 553.63/176.57 proper(d(X)) = [0 0 0]X >= [0 0 0]X = d(proper(X)) 553.63/176.57 [0 0 1] [0 0 1] 553.63/176.57 553.63/176.57 [1 0 0] [1] [1 0 0] [1] 553.63/176.57 proper(h(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = h(proper(X)) 553.63/176.57 [0 0 1] [0] [0 0 1] [0] 553.63/176.57 problem: 553.63/176.57 strict: 553.63/176.57 553.63/176.57 weak: 553.63/176.57 active(f(X)) -> f(active(X)) 553.63/176.57 f(ok(X)) -> ok(f(X)) 553.63/176.57 c(ok(X)) -> ok(c(X)) 553.63/176.57 g(ok(X)) -> ok(g(X)) 553.63/176.57 d(ok(X)) -> ok(d(X)) 553.63/176.57 h(ok(X)) -> ok(h(X)) 553.63/176.57 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.57 active(c(X)) -> mark(d(X)) 553.63/176.57 active(h(X)) -> mark(c(d(X))) 553.63/176.57 top(mark(X)) -> top(proper(X)) 553.63/176.57 top(ok(X)) -> top(active(X)) 553.63/176.57 active(h(X)) -> h(active(X)) 553.63/176.57 f(mark(X)) -> mark(f(X)) 553.63/176.57 h(mark(X)) -> mark(h(X)) 553.63/176.57 proper(f(X)) -> f(proper(X)) 553.63/176.57 proper(c(X)) -> c(proper(X)) 553.63/176.57 proper(g(X)) -> g(proper(X)) 553.63/176.57 proper(d(X)) -> d(proper(X)) 553.63/176.57 proper(h(X)) -> h(proper(X)) 553.63/176.57 Qed 553.63/176.57 553.63/176.57 strict: 553.63/176.57 active(f(X)) -> f(active(X)) 553.63/176.57 active(h(X)) -> h(active(X)) 553.63/176.57 f(mark(X)) -> mark(f(X)) 553.63/176.57 h(mark(X)) -> mark(h(X)) 553.63/176.57 proper(f(X)) -> f(proper(X)) 553.63/176.57 proper(c(X)) -> c(proper(X)) 553.63/176.57 proper(g(X)) -> g(proper(X)) 553.63/176.57 proper(d(X)) -> d(proper(X)) 553.63/176.57 proper(h(X)) -> h(proper(X)) 553.63/176.57 f(ok(X)) -> ok(f(X)) 553.63/176.57 c(ok(X)) -> ok(c(X)) 553.63/176.57 weak: 553.63/176.57 g(ok(X)) -> ok(g(X)) 553.63/176.57 d(ok(X)) -> ok(d(X)) 553.63/176.57 h(ok(X)) -> ok(h(X)) 553.63/176.57 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.57 active(c(X)) -> mark(d(X)) 553.63/176.57 active(h(X)) -> mark(c(d(X))) 553.63/176.57 top(mark(X)) -> top(proper(X)) 553.63/176.57 top(ok(X)) -> top(active(X)) 553.63/176.57 Matrix Interpretation Processor: dim=3 553.63/176.57 553.63/176.57 max_matrix: 553.63/176.57 [1 1 1] 553.63/176.57 [0 1 1] 553.63/176.57 [0 0 0] 553.63/176.57 interpretation: 553.63/176.57 [1 1 0] 553.63/176.57 [top](x0) = [0 0 0]x0 553.63/176.57 [0 0 0] , 553.63/176.57 553.63/176.57 [1 0 1] [1] 553.63/176.57 [ok](x0) = [0 1 0]x0 + [1] 553.63/176.57 [0 0 0] [0], 553.63/176.57 553.63/176.57 [1 0 0] 553.63/176.57 [proper](x0) = [0 0 0]x0 553.63/176.57 [0 0 0] , 553.63/176.57 553.63/176.57 [1 0 0] [1] 553.63/176.57 [h](x0) = [0 1 0]x0 + [0] 553.63/176.57 [0 0 0] [0], 553.63/176.57 553.63/176.57 [1 0 0] 553.63/176.57 [d](x0) = [0 1 0]x0 553.63/176.57 [0 0 0] , 553.63/176.57 553.63/176.57 [1 0 0] 553.63/176.57 [mark](x0) = [0 0 1]x0 553.63/176.57 [0 0 0] , 553.63/176.57 553.63/176.57 [1 0 0] 553.63/176.57 [c](x0) = [0 1 0]x0 553.63/176.57 [0 0 0] , 553.63/176.57 553.63/176.57 [1 1 1] 553.63/176.57 [g](x0) = [0 1 0]x0 553.63/176.57 [0 0 0] , 553.63/176.57 553.63/176.57 [1 1 0] 553.63/176.57 [active](x0) = [0 0 0]x0 553.63/176.57 [0 0 0] , 553.63/176.57 553.63/176.57 [1 0 0] 553.63/176.57 [f](x0) = [0 1 0]x0 553.63/176.57 [0 0 0] 553.63/176.57 orientation: 553.63/176.57 [1 1 1] [2] [1 1 1] [1] 553.63/176.57 g(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(g(X)) 553.63/176.57 [0 0 0] [0] [0 0 0] [0] 553.63/176.57 553.63/176.57 [1 0 1] [1] [1 0 0] [1] 553.63/176.57 d(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(d(X)) 553.63/176.57 [0 0 0] [0] [0 0 0] [0] 553.63/176.57 553.63/176.57 [1 0 1] [2] [1 0 0] [2] 553.63/176.57 h(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(h(X)) 553.63/176.57 [0 0 0] [0] [0 0 0] [0] 553.63/176.57 553.63/176.57 [1 1 0] [1 1 0] 553.63/176.57 active(f(f(X))) = [0 0 0]X >= [0 0 0]X = mark(c(f(g(f(X))))) 553.63/176.57 [0 0 0] [0 0 0] 553.63/176.57 553.63/176.57 [1 1 0] [1 0 0] 553.63/176.57 active(c(X)) = [0 0 0]X >= [0 0 0]X = mark(d(X)) 553.63/176.57 [0 0 0] [0 0 0] 553.63/176.57 553.63/176.57 [1 1 0] [1] [1 0 0] 553.63/176.57 active(h(X)) = [0 0 0]X + [0] >= [0 0 0]X = mark(c(d(X))) 553.63/176.57 [0 0 0] [0] [0 0 0] 553.63/176.57 553.63/176.57 [1 0 1] [1 0 0] 553.63/176.57 top(mark(X)) = [0 0 0]X >= [0 0 0]X = top(proper(X)) 553.63/176.57 [0 0 0] [0 0 0] 553.63/176.57 553.63/176.57 [1 1 1] [2] [1 1 0] 553.63/176.57 top(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X = top(active(X)) 553.63/176.57 [0 0 0] [0] [0 0 0] 553.63/176.57 553.63/176.57 [1 1 0] [1 1 0] 553.63/176.57 active(f(X)) = [0 0 0]X >= [0 0 0]X = f(active(X)) 553.63/176.57 [0 0 0] [0 0 0] 553.63/176.57 553.63/176.57 [1 1 0] [1] [1 1 0] [1] 553.63/176.57 active(h(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = h(active(X)) 553.63/176.57 [0 0 0] [0] [0 0 0] [0] 553.63/176.57 553.63/176.57 [1 0 0] [1 0 0] 553.63/176.57 f(mark(X)) = [0 0 1]X >= [0 0 0]X = mark(f(X)) 553.63/176.58 [0 0 0] [0 0 0] 553.63/176.58 553.63/176.58 [1 0 0] [1] [1 0 0] [1] 553.63/176.58 h(mark(X)) = [0 0 1]X + [0] >= [0 0 0]X + [0] = mark(h(X)) 553.63/176.58 [0 0 0] [0] [0 0 0] [0] 553.63/176.58 553.63/176.58 [1 0 0] [1 0 0] 553.63/176.58 proper(f(X)) = [0 0 0]X >= [0 0 0]X = f(proper(X)) 553.63/176.58 [0 0 0] [0 0 0] 553.63/176.58 553.63/176.58 [1 0 0] [1 0 0] 553.63/176.58 proper(c(X)) = [0 0 0]X >= [0 0 0]X = c(proper(X)) 553.63/176.58 [0 0 0] [0 0 0] 553.63/176.58 553.63/176.58 [1 1 1] [1 0 0] 553.63/176.58 proper(g(X)) = [0 0 0]X >= [0 0 0]X = g(proper(X)) 553.63/176.58 [0 0 0] [0 0 0] 553.63/176.58 553.63/176.58 [1 0 0] [1 0 0] 553.63/176.58 proper(d(X)) = [0 0 0]X >= [0 0 0]X = d(proper(X)) 553.63/176.58 [0 0 0] [0 0 0] 553.63/176.58 553.63/176.58 [1 0 0] [1] [1 0 0] [1] 553.63/176.58 proper(h(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = h(proper(X)) 553.63/176.58 [0 0 0] [0] [0 0 0] [0] 553.63/176.58 553.63/176.58 [1 0 1] [1] [1 0 0] [1] 553.63/176.58 f(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(f(X)) 553.63/176.58 [0 0 0] [0] [0 0 0] [0] 553.63/176.58 553.63/176.58 [1 0 1] [1] [1 0 0] [1] 553.63/176.58 c(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(c(X)) 553.63/176.58 [0 0 0] [0] [0 0 0] [0] 553.63/176.58 problem: 553.63/176.58 strict: 553.63/176.58 553.63/176.58 weak: 553.63/176.58 g(ok(X)) -> ok(g(X)) 553.63/176.58 d(ok(X)) -> ok(d(X)) 553.63/176.58 h(ok(X)) -> ok(h(X)) 553.63/176.58 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.58 active(c(X)) -> mark(d(X)) 553.63/176.58 active(h(X)) -> mark(c(d(X))) 553.63/176.58 top(mark(X)) -> top(proper(X)) 553.63/176.58 top(ok(X)) -> top(active(X)) 553.63/176.58 active(f(X)) -> f(active(X)) 553.63/176.58 active(h(X)) -> h(active(X)) 553.63/176.58 f(mark(X)) -> mark(f(X)) 553.63/176.58 h(mark(X)) -> mark(h(X)) 553.63/176.58 proper(f(X)) -> f(proper(X)) 553.63/176.58 proper(c(X)) -> c(proper(X)) 553.63/176.58 proper(g(X)) -> g(proper(X)) 553.63/176.58 proper(d(X)) -> d(proper(X)) 553.63/176.58 proper(h(X)) -> h(proper(X)) 553.63/176.58 f(ok(X)) -> ok(f(X)) 553.63/176.58 c(ok(X)) -> ok(c(X)) 553.63/176.58 Qed 553.63/176.58 553.63/176.58 strict: 553.63/176.58 active(f(X)) -> f(active(X)) 553.63/176.58 active(h(X)) -> h(active(X)) 553.63/176.58 f(mark(X)) -> mark(f(X)) 553.63/176.58 h(mark(X)) -> mark(h(X)) 553.63/176.58 proper(f(X)) -> f(proper(X)) 553.63/176.58 proper(c(X)) -> c(proper(X)) 553.63/176.58 proper(g(X)) -> g(proper(X)) 553.63/176.58 proper(d(X)) -> d(proper(X)) 553.63/176.58 proper(h(X)) -> h(proper(X)) 553.63/176.58 f(ok(X)) -> ok(f(X)) 553.63/176.58 c(ok(X)) -> ok(c(X)) 553.63/176.58 g(ok(X)) -> ok(g(X)) 553.63/176.58 d(ok(X)) -> ok(d(X)) 553.63/176.58 weak: 553.63/176.58 h(ok(X)) -> ok(h(X)) 553.63/176.58 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.58 active(c(X)) -> mark(d(X)) 553.63/176.58 active(h(X)) -> mark(c(d(X))) 553.63/176.58 top(mark(X)) -> top(proper(X)) 553.63/176.58 top(ok(X)) -> top(active(X)) 553.63/176.58 Matrix Interpretation Processor: dim=3 553.63/176.58 553.63/176.58 max_matrix: 553.63/176.58 [1 0 1] 553.63/176.58 [0 0 1] 553.63/176.58 [0 0 1] 553.63/176.58 interpretation: 553.63/176.58 [1 0 0] [0] 553.63/176.58 [top](x0) = [0 0 0]x0 + [1] 553.63/176.58 [0 0 0] [0], 553.63/176.58 553.63/176.58 [1 0 1] [1] 553.63/176.58 [ok](x0) = [0 0 0]x0 + [0] 553.63/176.58 [0 0 1] [1], 553.63/176.58 553.63/176.58 [1 0 0] [0] 553.63/176.58 [proper](x0) = [0 0 0]x0 + [1] 553.63/176.58 [0 0 0] [0], 553.63/176.58 553.63/176.58 [1 0 1] [0] 553.63/176.58 [h](x0) = [0 0 1]x0 + [1] 553.63/176.58 [0 0 1] [0], 553.63/176.58 553.63/176.58 [1 0 0] [1] 553.63/176.58 [d](x0) = [0 0 0]x0 + [0] 553.63/176.58 [0 0 1] [0], 553.63/176.58 553.63/176.58 [1 0 1] 553.63/176.58 [mark](x0) = [0 0 0]x0 553.63/176.58 [0 0 1] , 553.63/176.58 553.63/176.58 [1 0 0] 553.63/176.58 [c](x0) = [0 0 0]x0 553.63/176.58 [0 0 1] , 553.63/176.58 553.63/176.58 [1 0 0] [1] 553.63/176.58 [g](x0) = [0 0 0]x0 + [0] 553.63/176.58 [0 0 1] [0], 553.63/176.59 553.63/176.59 [1 0 1] [1] 553.63/176.59 [active](x0) = [0 0 1]x0 + [1] 553.63/176.59 [0 0 1] [0], 553.63/176.59 553.63/176.59 [1 0 0] 553.63/176.59 [f](x0) = [0 0 0]x0 553.63/176.59 [0 0 1] 553.63/176.59 orientation: 553.63/176.59 [1 0 2] [2] [1 0 2] [1] 553.63/176.59 h(ok(X)) = [0 0 1]X + [2] >= [0 0 0]X + [0] = ok(h(X)) 553.63/176.59 [0 0 1] [1] [0 0 1] [1] 553.63/176.59 553.63/176.59 [1 0 1] [1] [1 0 1] [1] 553.63/176.59 active(f(f(X))) = [0 0 1]X + [1] >= [0 0 0]X + [0] = mark(c(f(g(f(X))))) 553.63/176.59 [0 0 1] [0] [0 0 1] [0] 553.63/176.59 553.63/176.59 [1 0 1] [1] [1 0 1] [1] 553.63/176.59 active(c(X)) = [0 0 1]X + [1] >= [0 0 0]X + [0] = mark(d(X)) 553.63/176.59 [0 0 1] [0] [0 0 1] [0] 553.63/176.59 553.63/176.59 [1 0 2] [1] [1 0 1] [1] 553.63/176.59 active(h(X)) = [0 0 1]X + [1] >= [0 0 0]X + [0] = mark(c(d(X))) 553.63/176.59 [0 0 1] [0] [0 0 1] [0] 553.63/176.59 553.63/176.59 [1 0 1] [0] [1 0 0] [0] 553.63/176.59 top(mark(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = top(proper(X)) 553.63/176.59 [0 0 0] [0] [0 0 0] [0] 553.63/176.59 553.63/176.59 [1 0 1] [1] [1 0 1] [1] 553.63/176.59 top(ok(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = top(active(X)) 553.63/176.59 [0 0 0] [0] [0 0 0] [0] 553.63/176.59 553.63/176.59 [1 0 1] [1] [1 0 1] [1] 553.63/176.59 active(f(X)) = [0 0 1]X + [1] >= [0 0 0]X + [0] = f(active(X)) 553.63/176.59 [0 0 1] [0] [0 0 1] [0] 553.63/176.59 553.63/176.59 [1 0 2] [1] [1 0 2] [1] 553.63/176.59 active(h(X)) = [0 0 1]X + [1] >= [0 0 1]X + [1] = h(active(X)) 553.63/176.59 [0 0 1] [0] [0 0 1] [0] 553.63/176.59 553.63/176.59 [1 0 1] [1 0 1] 553.63/176.59 f(mark(X)) = [0 0 0]X >= [0 0 0]X = mark(f(X)) 553.63/176.59 [0 0 1] [0 0 1] 553.63/176.59 553.63/176.59 [1 0 2] [0] [1 0 2] 553.63/176.59 h(mark(X)) = [0 0 1]X + [1] >= [0 0 0]X = mark(h(X)) 553.63/176.59 [0 0 1] [0] [0 0 1] 553.63/176.59 553.63/176.59 [1 0 0] [0] [1 0 0] 553.63/176.59 proper(f(X)) = [0 0 0]X + [1] >= [0 0 0]X = f(proper(X)) 553.63/176.59 [0 0 0] [0] [0 0 0] 553.63/176.59 553.63/176.59 [1 0 0] [0] [1 0 0] 553.63/176.59 proper(c(X)) = [0 0 0]X + [1] >= [0 0 0]X = c(proper(X)) 553.63/176.59 [0 0 0] [0] [0 0 0] 553.63/176.59 553.63/176.59 [1 0 0] [1] [1 0 0] [1] 553.63/176.59 proper(g(X)) = [0 0 0]X + [1] >= [0 0 0]X + [0] = g(proper(X)) 553.63/176.59 [0 0 0] [0] [0 0 0] [0] 553.63/176.59 553.63/176.59 [1 0 0] [1] [1 0 0] [1] 553.63/176.59 proper(d(X)) = [0 0 0]X + [1] >= [0 0 0]X + [0] = d(proper(X)) 553.63/176.59 [0 0 0] [0] [0 0 0] [0] 553.63/176.59 553.63/176.59 [1 0 1] [0] [1 0 0] [0] 553.63/176.59 proper(h(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = h(proper(X)) 553.63/176.59 [0 0 0] [0] [0 0 0] [0] 553.63/176.59 553.63/176.59 [1 0 1] [1] [1 0 1] [1] 553.63/176.59 f(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(f(X)) 553.63/176.59 [0 0 1] [1] [0 0 1] [1] 553.63/176.59 553.63/176.59 [1 0 1] [1] [1 0 1] [1] 553.63/176.59 c(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(c(X)) 553.63/176.59 [0 0 1] [1] [0 0 1] [1] 553.63/176.59 553.63/176.59 [1 0 1] [2] [1 0 1] [2] 553.63/176.59 g(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(g(X)) 553.63/176.59 [0 0 1] [1] [0 0 1] [1] 553.63/176.59 553.63/176.59 [1 0 1] [2] [1 0 1] [2] 553.63/176.59 d(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(d(X)) 553.63/176.59 [0 0 1] [1] [0 0 1] [1] 553.63/176.59 problem: 553.63/176.59 strict: 553.63/176.59 553.63/176.59 weak: 553.63/176.59 h(ok(X)) -> ok(h(X)) 553.63/176.59 active(f(f(X))) -> mark(c(f(g(f(X))))) 553.63/176.59 active(c(X)) -> mark(d(X)) 553.63/176.59 active(h(X)) -> mark(c(d(X))) 553.63/176.59 top(mark(X)) -> top(proper(X)) 553.63/176.59 top(ok(X)) -> top(active(X)) 553.63/176.59 active(f(X)) -> f(active(X)) 553.63/176.59 active(h(X)) -> h(active(X)) 553.63/176.59 f(mark(X)) -> mark(f(X)) 553.63/176.59 h(mark(X)) -> mark(h(X)) 553.63/176.59 proper(f(X)) -> f(proper(X)) 553.63/176.59 proper(c(X)) -> c(proper(X)) 553.63/176.59 proper(g(X)) -> g(proper(X)) 553.63/176.59 proper(d(X)) -> d(proper(X)) 553.63/176.59 proper(h(X)) -> h(proper(X)) 553.63/176.59 f(ok(X)) -> ok(f(X)) 553.63/176.59 c(ok(X)) -> ok(c(X)) 553.63/176.59 g(ok(X)) -> ok(g(X)) 553.63/176.59 d(ok(X)) -> ok(d(X)) 553.63/176.59 Qed 553.63/176.59 EOF