YES(?,O(n^2)) 361.11/116.55 YES(?,O(n^2)) 361.11/116.56 361.11/116.56 Problem: 361.11/116.56 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.56 active(f(X)) -> f(active(X)) 361.11/116.56 active(h(X)) -> h(active(X)) 361.11/116.56 f(mark(X)) -> mark(f(X)) 361.11/116.56 h(mark(X)) -> mark(h(X)) 361.11/116.56 proper(f(X)) -> f(proper(X)) 361.11/116.56 proper(g(X)) -> g(proper(X)) 361.11/116.56 proper(h(X)) -> h(proper(X)) 361.11/116.56 f(ok(X)) -> ok(f(X)) 361.11/116.56 g(ok(X)) -> ok(g(X)) 361.11/116.56 h(ok(X)) -> ok(h(X)) 361.11/116.56 top(mark(X)) -> top(proper(X)) 361.11/116.56 top(ok(X)) -> top(active(X)) 361.11/116.56 361.11/116.56 Proof: 361.11/116.56 Complexity Transformation Processor: 361.11/116.56 strict: 361.11/116.56 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.56 active(f(X)) -> f(active(X)) 361.11/116.56 active(h(X)) -> h(active(X)) 361.11/116.56 f(mark(X)) -> mark(f(X)) 361.11/116.56 h(mark(X)) -> mark(h(X)) 361.11/116.56 proper(f(X)) -> f(proper(X)) 361.11/116.56 proper(g(X)) -> g(proper(X)) 361.11/116.56 proper(h(X)) -> h(proper(X)) 361.11/116.56 f(ok(X)) -> ok(f(X)) 361.11/116.56 g(ok(X)) -> ok(g(X)) 361.11/116.56 h(ok(X)) -> ok(h(X)) 361.11/116.56 top(mark(X)) -> top(proper(X)) 361.11/116.56 top(ok(X)) -> top(active(X)) 361.11/116.56 weak: 361.11/116.56 361.11/116.56 Matrix Interpretation Processor: dim=1 361.11/116.56 361.11/116.56 max_matrix: 361.11/116.56 1 361.11/116.56 interpretation: 361.11/116.56 [top](x0) = x0 + 52, 361.11/116.56 361.11/116.56 [ok](x0) = x0 + 65, 361.11/116.56 361.11/116.56 [proper](x0) = x0 + 4, 361.11/116.56 361.11/116.56 [mark](x0) = x0 + 1, 361.11/116.56 361.11/116.56 [g](x0) = x0 + 64, 361.11/116.56 361.11/116.56 [h](x0) = x0, 361.11/116.56 361.11/116.56 [active](x0) = x0 + 12, 361.11/116.56 361.11/116.56 [f](x0) = x0 + 71 361.11/116.56 orientation: 361.11/116.56 active(f(X)) = X + 83 >= X + 136 = mark(g(h(f(X)))) 361.11/116.56 361.11/116.56 active(f(X)) = X + 83 >= X + 83 = f(active(X)) 361.11/116.56 361.11/116.56 active(h(X)) = X + 12 >= X + 12 = h(active(X)) 361.11/116.56 361.11/116.56 f(mark(X)) = X + 72 >= X + 72 = mark(f(X)) 361.11/116.56 361.11/116.56 h(mark(X)) = X + 1 >= X + 1 = mark(h(X)) 361.11/116.56 361.11/116.56 proper(f(X)) = X + 75 >= X + 75 = f(proper(X)) 361.11/116.56 361.11/116.56 proper(g(X)) = X + 68 >= X + 68 = g(proper(X)) 361.11/116.56 361.11/116.56 proper(h(X)) = X + 4 >= X + 4 = h(proper(X)) 361.11/116.56 361.11/116.56 f(ok(X)) = X + 136 >= X + 136 = ok(f(X)) 361.11/116.56 361.11/116.56 g(ok(X)) = X + 129 >= X + 129 = ok(g(X)) 361.11/116.56 361.11/116.56 h(ok(X)) = X + 65 >= X + 65 = ok(h(X)) 361.11/116.56 361.11/116.56 top(mark(X)) = X + 53 >= X + 56 = top(proper(X)) 361.11/116.56 361.11/116.56 top(ok(X)) = X + 117 >= X + 64 = top(active(X)) 361.11/116.56 problem: 361.11/116.56 strict: 361.11/116.56 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.56 active(f(X)) -> f(active(X)) 361.11/116.56 active(h(X)) -> h(active(X)) 361.11/116.56 f(mark(X)) -> mark(f(X)) 361.11/116.56 h(mark(X)) -> mark(h(X)) 361.11/116.56 proper(f(X)) -> f(proper(X)) 361.11/116.56 proper(g(X)) -> g(proper(X)) 361.11/116.56 proper(h(X)) -> h(proper(X)) 361.11/116.56 f(ok(X)) -> ok(f(X)) 361.11/116.56 g(ok(X)) -> ok(g(X)) 361.11/116.56 h(ok(X)) -> ok(h(X)) 361.11/116.56 top(mark(X)) -> top(proper(X)) 361.11/116.56 weak: 361.11/116.56 top(ok(X)) -> top(active(X)) 361.11/116.56 Matrix Interpretation Processor: dim=1 361.11/116.56 361.11/116.56 max_matrix: 361.11/116.56 1 361.11/116.56 interpretation: 361.11/116.56 [top](x0) = x0 + 9, 361.11/116.56 361.11/116.56 [ok](x0) = x0 + 7, 361.11/116.56 361.11/116.56 [proper](x0) = x0 + 7, 361.11/116.56 361.11/116.56 [mark](x0) = x0 + 8, 361.11/116.56 361.11/116.56 [g](x0) = x0, 361.11/116.56 361.11/116.56 [h](x0) = x0, 361.11/116.56 361.11/116.56 [active](x0) = x0 + 7, 361.11/116.56 361.11/116.56 [f](x0) = x0 + 12 361.11/116.56 orientation: 361.11/116.56 active(f(X)) = X + 19 >= X + 20 = mark(g(h(f(X)))) 361.11/116.56 361.11/116.56 active(f(X)) = X + 19 >= X + 19 = f(active(X)) 361.11/116.56 361.11/116.56 active(h(X)) = X + 7 >= X + 7 = h(active(X)) 361.11/116.56 361.11/116.56 f(mark(X)) = X + 20 >= X + 20 = mark(f(X)) 361.11/116.56 361.11/116.56 h(mark(X)) = X + 8 >= X + 8 = mark(h(X)) 361.11/116.56 361.11/116.56 proper(f(X)) = X + 19 >= X + 19 = f(proper(X)) 361.11/116.56 361.11/116.56 proper(g(X)) = X + 7 >= X + 7 = g(proper(X)) 361.11/116.56 361.11/116.56 proper(h(X)) = X + 7 >= X + 7 = h(proper(X)) 361.11/116.56 361.11/116.56 f(ok(X)) = X + 19 >= X + 19 = ok(f(X)) 361.11/116.56 361.11/116.56 g(ok(X)) = X + 7 >= X + 7 = ok(g(X)) 361.11/116.56 361.11/116.56 h(ok(X)) = X + 7 >= X + 7 = ok(h(X)) 361.11/116.56 361.11/116.56 top(mark(X)) = X + 17 >= X + 16 = top(proper(X)) 361.11/116.56 361.11/116.56 top(ok(X)) = X + 16 >= X + 16 = top(active(X)) 361.11/116.56 problem: 361.11/116.56 strict: 361.11/116.56 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.56 active(f(X)) -> f(active(X)) 361.11/116.56 active(h(X)) -> h(active(X)) 361.11/116.56 f(mark(X)) -> mark(f(X)) 361.11/116.56 h(mark(X)) -> mark(h(X)) 361.11/116.56 proper(f(X)) -> f(proper(X)) 361.11/116.56 proper(g(X)) -> g(proper(X)) 361.11/116.56 proper(h(X)) -> h(proper(X)) 361.11/116.56 f(ok(X)) -> ok(f(X)) 361.11/116.56 g(ok(X)) -> ok(g(X)) 361.11/116.56 h(ok(X)) -> ok(h(X)) 361.11/116.56 weak: 361.11/116.56 top(mark(X)) -> top(proper(X)) 361.11/116.56 top(ok(X)) -> top(active(X)) 361.11/116.56 Matrix Interpretation Processor: dim=1 361.11/116.56 361.11/116.56 max_matrix: 361.11/116.56 1 361.11/116.56 interpretation: 361.11/116.56 [top](x0) = x0, 361.11/116.56 361.11/116.56 [ok](x0) = x0 + 1, 361.11/116.56 361.11/116.56 [proper](x0) = x0, 361.11/116.56 361.11/116.56 [mark](x0) = x0, 361.11/116.56 361.11/116.56 [g](x0) = x0, 361.11/116.56 361.11/116.56 [h](x0) = x0, 361.11/116.56 361.11/116.56 [active](x0) = x0 + 1, 361.11/116.56 361.11/116.56 [f](x0) = x0 361.11/116.56 orientation: 361.11/116.56 active(f(X)) = X + 1 >= X = mark(g(h(f(X)))) 361.11/116.56 361.11/116.56 active(f(X)) = X + 1 >= X + 1 = f(active(X)) 361.11/116.56 361.11/116.56 active(h(X)) = X + 1 >= X + 1 = h(active(X)) 361.11/116.56 361.11/116.56 f(mark(X)) = X >= X = mark(f(X)) 361.11/116.56 361.11/116.56 h(mark(X)) = X >= X = mark(h(X)) 361.11/116.56 361.11/116.56 proper(f(X)) = X >= X = f(proper(X)) 361.11/116.56 361.11/116.56 proper(g(X)) = X >= X = g(proper(X)) 361.11/116.56 361.11/116.56 proper(h(X)) = X >= X = h(proper(X)) 361.11/116.56 361.11/116.56 f(ok(X)) = X + 1 >= X + 1 = ok(f(X)) 361.11/116.56 361.11/116.56 g(ok(X)) = X + 1 >= X + 1 = ok(g(X)) 361.11/116.56 361.11/116.56 h(ok(X)) = X + 1 >= X + 1 = ok(h(X)) 361.11/116.56 361.11/116.56 top(mark(X)) = X >= X = top(proper(X)) 361.11/116.56 361.11/116.56 top(ok(X)) = X + 1 >= X + 1 = top(active(X)) 361.11/116.56 problem: 361.11/116.56 strict: 361.11/116.56 active(f(X)) -> f(active(X)) 361.11/116.56 active(h(X)) -> h(active(X)) 361.11/116.56 f(mark(X)) -> mark(f(X)) 361.11/116.56 h(mark(X)) -> mark(h(X)) 361.11/116.56 proper(f(X)) -> f(proper(X)) 361.11/116.56 proper(g(X)) -> g(proper(X)) 361.11/116.56 proper(h(X)) -> h(proper(X)) 361.11/116.56 f(ok(X)) -> ok(f(X)) 361.11/116.56 g(ok(X)) -> ok(g(X)) 361.11/116.56 h(ok(X)) -> ok(h(X)) 361.11/116.56 weak: 361.11/116.56 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.56 top(mark(X)) -> top(proper(X)) 361.11/116.56 top(ok(X)) -> top(active(X)) 361.11/116.56 Splitting Processor: 361.11/116.56 strict: 361.11/116.56 g(ok(X)) -> ok(g(X)) 361.11/116.56 weak: 361.11/116.56 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.56 top(mark(X)) -> top(proper(X)) 361.11/116.56 top(ok(X)) -> top(active(X)) 361.11/116.56 active(f(X)) -> f(active(X)) 361.11/116.56 active(h(X)) -> h(active(X)) 361.11/116.56 f(mark(X)) -> mark(f(X)) 361.11/116.56 h(mark(X)) -> mark(h(X)) 361.11/116.56 proper(f(X)) -> f(proper(X)) 361.11/116.56 proper(g(X)) -> g(proper(X)) 361.11/116.56 proper(h(X)) -> h(proper(X)) 361.11/116.56 f(ok(X)) -> ok(f(X)) 361.11/116.56 h(ok(X)) -> ok(h(X)) 361.11/116.56 Splitting Processor: 361.11/116.56 strict: 361.11/116.56 f(ok(X)) -> ok(f(X)) 361.11/116.56 weak: 361.11/116.56 g(ok(X)) -> ok(g(X)) 361.11/116.56 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.56 top(mark(X)) -> top(proper(X)) 361.11/116.56 top(ok(X)) -> top(active(X)) 361.11/116.56 active(f(X)) -> f(active(X)) 361.11/116.56 active(h(X)) -> h(active(X)) 361.11/116.56 f(mark(X)) -> mark(f(X)) 361.11/116.56 h(mark(X)) -> mark(h(X)) 361.11/116.56 proper(f(X)) -> f(proper(X)) 361.11/116.56 proper(g(X)) -> g(proper(X)) 361.11/116.56 proper(h(X)) -> h(proper(X)) 361.11/116.56 h(ok(X)) -> ok(h(X)) 361.11/116.56 Matrix Interpretation Processor: dim=3 361.11/116.56 361.11/116.56 max_matrix: 361.11/116.56 [1 1 1] 361.11/116.56 [0 1 1] 361.11/116.56 [0 0 0] 361.11/116.56 interpretation: 361.11/116.56 [1 0 1] 361.11/116.56 [top](x0) = [0 1 1]x0 361.11/116.56 [0 0 0] , 361.11/116.56 361.11/116.56 [1 0 1] [1] 361.11/116.56 [ok](x0) = [0 1 0]x0 + [1] 361.11/116.56 [0 0 0] [0], 361.11/116.56 361.11/116.56 [1 0 0] 361.11/116.56 [proper](x0) = [0 0 0]x0 361.11/116.56 [0 0 0] , 361.11/116.56 361.11/116.56 [1 0 1] 361.11/116.56 [mark](x0) = [0 1 0]x0 361.11/116.56 [0 0 0] , 361.11/116.56 361.11/116.56 [1 0 0] 361.11/116.56 [g](x0) = [0 1 0]x0 361.11/116.56 [0 0 0] , 361.11/116.56 361.11/116.56 [1 0 1] 361.11/116.56 [h](x0) = [0 1 0]x0 361.11/116.56 [0 0 0] , 361.11/116.56 361.11/116.56 [1 0 0] 361.11/116.56 [active](x0) = [0 1 0]x0 361.11/116.56 [0 0 0] , 361.11/116.56 361.11/116.56 [1 1 0] [1] 361.11/116.56 [f](x0) = [0 1 0]x0 + [0] 361.11/116.56 [0 0 0] [0] 361.11/116.56 orientation: 361.11/116.56 [1 1 1] [3] [1 1 0] [2] 361.11/116.56 f(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(f(X)) 361.11/116.56 [0 0 0] [0] [0 0 0] [0] 361.11/116.56 361.11/116.56 [1 0 1] [1] [1 0 0] [1] 361.11/116.56 g(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(g(X)) 361.11/116.56 [0 0 0] [0] [0 0 0] [0] 361.11/116.56 361.11/116.56 [1 1 0] [1] [1 1 0] [1] 361.11/116.56 active(f(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = mark(g(h(f(X)))) 361.11/116.56 [0 0 0] [0] [0 0 0] [0] 361.11/116.56 361.11/116.56 [1 0 1] [1 0 0] 361.11/116.56 top(mark(X)) = [0 1 0]X >= [0 0 0]X = top(proper(X)) 361.11/116.56 [0 0 0] [0 0 0] 361.11/116.56 361.11/116.57 [1 0 1] [1] [1 0 0] 361.11/116.57 top(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X = top(active(X)) 361.11/116.57 [0 0 0] [0] [0 0 0] 361.11/116.57 361.11/116.57 [1 1 0] [1] [1 1 0] [1] 361.11/116.57 active(f(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = f(active(X)) 361.11/116.57 [0 0 0] [0] [0 0 0] [0] 361.11/116.57 361.11/116.57 [1 0 1] [1 0 0] 361.11/116.57 active(h(X)) = [0 1 0]X >= [0 1 0]X = h(active(X)) 361.11/116.57 [0 0 0] [0 0 0] 361.11/116.57 361.11/116.57 [1 1 1] [1] [1 1 0] [1] 361.11/116.57 f(mark(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = mark(f(X)) 361.11/116.57 [0 0 0] [0] [0 0 0] [0] 361.11/116.57 361.11/116.57 [1 0 1] [1 0 1] 361.11/116.57 h(mark(X)) = [0 1 0]X >= [0 1 0]X = mark(h(X)) 361.11/116.57 [0 0 0] [0 0 0] 361.11/116.57 361.11/116.57 [1 1 0] [1] [1 0 0] [1] 361.11/116.57 proper(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(proper(X)) 361.11/116.57 [0 0 0] [0] [0 0 0] [0] 361.11/116.57 361.11/116.57 [1 0 0] [1 0 0] 361.11/116.57 proper(g(X)) = [0 0 0]X >= [0 0 0]X = g(proper(X)) 361.11/116.57 [0 0 0] [0 0 0] 361.11/116.57 361.11/116.57 [1 0 1] [1 0 0] 361.11/116.57 proper(h(X)) = [0 0 0]X >= [0 0 0]X = h(proper(X)) 361.11/116.57 [0 0 0] [0 0 0] 361.11/116.57 361.11/116.57 [1 0 1] [1] [1 0 1] [1] 361.11/116.57 h(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(h(X)) 361.11/116.57 [0 0 0] [0] [0 0 0] [0] 361.11/116.57 problem: 361.11/116.57 strict: 361.11/116.57 361.11/116.57 weak: 361.11/116.57 f(ok(X)) -> ok(f(X)) 361.11/116.57 g(ok(X)) -> ok(g(X)) 361.11/116.57 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.57 top(mark(X)) -> top(proper(X)) 361.11/116.57 top(ok(X)) -> top(active(X)) 361.11/116.57 active(f(X)) -> f(active(X)) 361.11/116.57 active(h(X)) -> h(active(X)) 361.11/116.57 f(mark(X)) -> mark(f(X)) 361.11/116.57 h(mark(X)) -> mark(h(X)) 361.11/116.57 proper(f(X)) -> f(proper(X)) 361.11/116.57 proper(g(X)) -> g(proper(X)) 361.11/116.57 proper(h(X)) -> h(proper(X)) 361.11/116.57 h(ok(X)) -> ok(h(X)) 361.11/116.57 Qed 361.11/116.57 361.11/116.57 strict: 361.11/116.57 active(f(X)) -> f(active(X)) 361.11/116.57 active(h(X)) -> h(active(X)) 361.11/116.57 f(mark(X)) -> mark(f(X)) 361.11/116.57 h(mark(X)) -> mark(h(X)) 361.11/116.57 proper(f(X)) -> f(proper(X)) 361.11/116.57 proper(g(X)) -> g(proper(X)) 361.11/116.57 proper(h(X)) -> h(proper(X)) 361.11/116.57 h(ok(X)) -> ok(h(X)) 361.11/116.57 weak: 361.11/116.57 f(ok(X)) -> ok(f(X)) 361.11/116.57 g(ok(X)) -> ok(g(X)) 361.11/116.57 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.57 top(mark(X)) -> top(proper(X)) 361.11/116.57 top(ok(X)) -> top(active(X)) 361.11/116.57 Splitting Processor: 361.11/116.57 strict: 361.11/116.57 h(ok(X)) -> ok(h(X)) 361.11/116.57 weak: 361.11/116.57 f(ok(X)) -> ok(f(X)) 361.11/116.57 g(ok(X)) -> ok(g(X)) 361.11/116.57 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.57 top(mark(X)) -> top(proper(X)) 361.11/116.57 top(ok(X)) -> top(active(X)) 361.11/116.57 active(f(X)) -> f(active(X)) 361.11/116.57 active(h(X)) -> h(active(X)) 361.11/116.57 f(mark(X)) -> mark(f(X)) 361.11/116.57 h(mark(X)) -> mark(h(X)) 361.11/116.57 proper(f(X)) -> f(proper(X)) 361.11/116.57 proper(g(X)) -> g(proper(X)) 361.11/116.57 proper(h(X)) -> h(proper(X)) 361.11/116.57 Splitting Processor: 361.11/116.57 strict: 361.11/116.57 proper(f(X)) -> f(proper(X)) 361.11/116.57 weak: 361.11/116.57 h(ok(X)) -> ok(h(X)) 361.11/116.57 f(ok(X)) -> ok(f(X)) 361.11/116.57 g(ok(X)) -> ok(g(X)) 361.11/116.57 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.57 top(mark(X)) -> top(proper(X)) 361.11/116.57 top(ok(X)) -> top(active(X)) 361.11/116.57 active(f(X)) -> f(active(X)) 361.11/116.57 active(h(X)) -> h(active(X)) 361.11/116.57 f(mark(X)) -> mark(f(X)) 361.11/116.57 h(mark(X)) -> mark(h(X)) 361.11/116.57 proper(g(X)) -> g(proper(X)) 361.11/116.57 proper(h(X)) -> h(proper(X)) 361.11/116.57 Matrix Interpretation Processor: dim=3 361.11/116.57 361.11/116.57 max_matrix: 361.11/116.57 [1 0 1] 361.11/116.57 [0 0 1] 361.11/116.57 [0 0 1] 361.11/116.57 interpretation: 361.11/116.57 [1 0 0] [1] 361.11/116.57 [top](x0) = [0 0 1]x0 + [0] 361.11/116.57 [0 0 0] [0], 361.11/116.57 361.11/116.57 [1 0 1] [0] 361.11/116.57 [ok](x0) = [0 0 0]x0 + [0] 361.11/116.57 [0 0 1] [1], 361.11/116.57 361.11/116.57 [1 0 1] 361.11/116.57 [proper](x0) = [0 0 0]x0 361.11/116.57 [0 0 1] , 361.11/116.57 361.11/116.57 [1 0 1] [0] 361.11/116.57 [mark](x0) = [0 0 0]x0 + [0] 361.11/116.57 [0 0 1] [1], 361.11/116.57 361.11/116.57 [1 0 0] 361.11/116.57 [g](x0) = [0 0 0]x0 361.11/116.57 [0 0 1] , 361.11/116.57 361.11/116.57 [1 0 0] 361.11/116.57 [h](x0) = [0 0 0]x0 361.11/116.57 [0 0 1] , 361.11/116.57 361.11/116.57 [1 0 1] [0] 361.11/116.57 [active](x0) = [0 0 1]x0 + [0] 361.11/116.57 [0 0 1] [1], 361.11/116.57 361.11/116.57 [1 0 1] [0] 361.11/116.57 [f](x0) = [0 0 0]x0 + [0] 361.11/116.57 [0 0 1] [1] 361.11/116.57 orientation: 361.11/116.57 [1 0 2] [1] [1 0 2] [0] 361.11/116.57 proper(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(proper(X)) 361.11/116.57 [0 0 1] [1] [0 0 1] [1] 361.11/116.57 361.11/116.57 [1 0 1] [0] [1 0 1] [0] 361.11/116.57 h(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(h(X)) 361.11/116.57 [0 0 1] [1] [0 0 1] [1] 361.11/116.57 361.11/116.57 [1 0 2] [1] [1 0 2] [1] 361.11/116.57 f(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(f(X)) 361.11/116.57 [0 0 1] [2] [0 0 1] [2] 361.11/116.57 361.11/116.57 [1 0 1] [0] [1 0 1] [0] 361.11/116.57 g(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(g(X)) 361.11/116.57 [0 0 1] [1] [0 0 1] [1] 361.11/116.57 361.11/116.57 [1 0 2] [1] [1 0 2] [1] 361.11/116.57 active(f(X)) = [0 0 1]X + [1] >= [0 0 0]X + [0] = mark(g(h(f(X)))) 361.11/116.57 [0 0 1] [2] [0 0 1] [2] 361.11/116.57 361.11/116.57 [1 0 1] [1] [1 0 1] [1] 361.11/116.57 top(mark(X)) = [0 0 1]X + [1] >= [0 0 1]X + [0] = top(proper(X)) 361.11/116.57 [0 0 0] [0] [0 0 0] [0] 361.11/116.57 361.11/116.57 [1 0 1] [1] [1 0 1] [1] 361.11/116.57 top(ok(X)) = [0 0 1]X + [1] >= [0 0 1]X + [1] = top(active(X)) 361.11/116.57 [0 0 0] [0] [0 0 0] [0] 361.11/116.57 361.11/116.57 [1 0 2] [1] [1 0 2] [1] 361.11/116.57 active(f(X)) = [0 0 1]X + [1] >= [0 0 0]X + [0] = f(active(X)) 361.11/116.57 [0 0 1] [2] [0 0 1] [2] 361.11/116.57 361.11/116.57 [1 0 1] [0] [1 0 1] [0] 361.11/116.57 active(h(X)) = [0 0 1]X + [0] >= [0 0 0]X + [0] = h(active(X)) 361.11/116.57 [0 0 1] [1] [0 0 1] [1] 361.11/116.57 361.11/116.57 [1 0 2] [1] [1 0 2] [1] 361.11/116.57 f(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(f(X)) 361.11/116.57 [0 0 1] [2] [0 0 1] [2] 361.11/116.57 361.11/116.57 [1 0 1] [0] [1 0 1] [0] 361.11/116.57 h(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(h(X)) 361.11/116.57 [0 0 1] [1] [0 0 1] [1] 361.11/116.57 361.11/116.57 [1 0 1] [1 0 1] 361.11/116.57 proper(g(X)) = [0 0 0]X >= [0 0 0]X = g(proper(X)) 361.11/116.57 [0 0 1] [0 0 1] 361.11/116.57 361.11/116.57 [1 0 1] [1 0 1] 361.11/116.57 proper(h(X)) = [0 0 0]X >= [0 0 0]X = h(proper(X)) 361.11/116.57 [0 0 1] [0 0 1] 361.11/116.57 problem: 361.11/116.57 strict: 361.11/116.57 361.11/116.57 weak: 361.11/116.57 proper(f(X)) -> f(proper(X)) 361.11/116.57 h(ok(X)) -> ok(h(X)) 361.11/116.57 f(ok(X)) -> ok(f(X)) 361.11/116.57 g(ok(X)) -> ok(g(X)) 361.11/116.57 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.58 top(mark(X)) -> top(proper(X)) 361.11/116.58 top(ok(X)) -> top(active(X)) 361.11/116.58 active(f(X)) -> f(active(X)) 361.11/116.58 active(h(X)) -> h(active(X)) 361.11/116.58 f(mark(X)) -> mark(f(X)) 361.11/116.58 h(mark(X)) -> mark(h(X)) 361.11/116.58 proper(g(X)) -> g(proper(X)) 361.11/116.58 proper(h(X)) -> h(proper(X)) 361.11/116.58 Qed 361.11/116.58 361.11/116.58 strict: 361.11/116.58 active(f(X)) -> f(active(X)) 361.11/116.58 active(h(X)) -> h(active(X)) 361.11/116.58 f(mark(X)) -> mark(f(X)) 361.11/116.58 h(mark(X)) -> mark(h(X)) 361.11/116.58 proper(g(X)) -> g(proper(X)) 361.11/116.58 proper(h(X)) -> h(proper(X)) 361.11/116.58 weak: 361.11/116.58 proper(f(X)) -> f(proper(X)) 361.11/116.58 h(ok(X)) -> ok(h(X)) 361.11/116.58 f(ok(X)) -> ok(f(X)) 361.11/116.58 g(ok(X)) -> ok(g(X)) 361.11/116.58 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.58 top(mark(X)) -> top(proper(X)) 361.11/116.58 top(ok(X)) -> top(active(X)) 361.11/116.58 Splitting Processor: 361.11/116.58 strict: 361.11/116.58 proper(g(X)) -> g(proper(X)) 361.11/116.58 weak: 361.11/116.58 proper(f(X)) -> f(proper(X)) 361.11/116.58 h(ok(X)) -> ok(h(X)) 361.11/116.58 f(ok(X)) -> ok(f(X)) 361.11/116.58 g(ok(X)) -> ok(g(X)) 361.11/116.58 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.58 top(mark(X)) -> top(proper(X)) 361.11/116.58 top(ok(X)) -> top(active(X)) 361.11/116.58 active(f(X)) -> f(active(X)) 361.11/116.58 active(h(X)) -> h(active(X)) 361.11/116.58 f(mark(X)) -> mark(f(X)) 361.11/116.58 h(mark(X)) -> mark(h(X)) 361.11/116.58 proper(h(X)) -> h(proper(X)) 361.11/116.58 Matrix Interpretation Processor: dim=2 361.11/116.58 361.11/116.58 max_matrix: 361.11/116.58 [1 2] 361.11/116.58 [0 1] 361.11/116.58 interpretation: 361.11/116.58 [1 0] 361.11/116.58 [top](x0) = [0 0]x0, 361.11/116.58 361.11/116.58 [1 2] [2] 361.11/116.58 [ok](x0) = [0 1]x0 + [2], 361.11/116.58 361.11/116.58 [1 1] [1] 361.11/116.58 [proper](x0) = [0 1]x0 + [0], 361.11/116.58 361.11/116.58 [1 1] [1] 361.11/116.58 [mark](x0) = [0 0]x0 + [0], 361.11/116.58 361.11/116.58 [1 1] [0] 361.11/116.58 [g](x0) = [0 1]x0 + [1], 361.11/116.58 361.11/116.58 361.11/116.58 [h](x0) = x0, 361.11/116.58 361.11/116.58 [1 2] [2] 361.11/116.58 [active](x0) = [0 0]x0 + [0], 361.11/116.58 361.11/116.58 361.11/116.58 [f](x0) = x0 361.11/116.58 orientation: 361.11/116.58 [1 2] [2] [1 2] [1] 361.11/116.58 proper(g(X)) = [0 1]X + [1] >= [0 1]X + [1] = g(proper(X)) 361.11/116.58 361.11/116.58 [1 1] [1] [1 1] [1] 361.11/116.58 proper(f(X)) = [0 1]X + [0] >= [0 1]X + [0] = f(proper(X)) 361.11/116.58 361.11/116.58 [1 2] [2] [1 2] [2] 361.11/116.58 h(ok(X)) = [0 1]X + [2] >= [0 1]X + [2] = ok(h(X)) 361.11/116.58 361.11/116.58 [1 2] [2] [1 2] [2] 361.11/116.58 f(ok(X)) = [0 1]X + [2] >= [0 1]X + [2] = ok(f(X)) 361.11/116.58 361.11/116.58 [1 3] [4] [1 3] [4] 361.11/116.58 g(ok(X)) = [0 1]X + [3] >= [0 1]X + [3] = ok(g(X)) 361.11/116.58 361.11/116.58 [1 2] [2] [1 2] [2] 361.11/116.58 active(f(X)) = [0 0]X + [0] >= [0 0]X + [0] = mark(g(h(f(X)))) 361.11/116.58 361.11/116.58 [1 1] [1] [1 1] [1] 361.11/116.58 top(mark(X)) = [0 0]X + [0] >= [0 0]X + [0] = top(proper(X)) 361.11/116.58 361.11/116.58 [1 2] [2] [1 2] [2] 361.11/116.58 top(ok(X)) = [0 0]X + [0] >= [0 0]X + [0] = top(active(X)) 361.11/116.58 361.11/116.58 [1 2] [2] [1 2] [2] 361.11/116.58 active(f(X)) = [0 0]X + [0] >= [0 0]X + [0] = f(active(X)) 361.11/116.58 361.11/116.58 [1 2] [2] [1 2] [2] 361.11/116.58 active(h(X)) = [0 0]X + [0] >= [0 0]X + [0] = h(active(X)) 361.11/116.58 361.11/116.58 [1 1] [1] [1 1] [1] 361.11/116.58 f(mark(X)) = [0 0]X + [0] >= [0 0]X + [0] = mark(f(X)) 361.11/116.58 361.11/116.58 [1 1] [1] [1 1] [1] 361.11/116.58 h(mark(X)) = [0 0]X + [0] >= [0 0]X + [0] = mark(h(X)) 361.11/116.58 361.11/116.58 [1 1] [1] [1 1] [1] 361.11/116.58 proper(h(X)) = [0 1]X + [0] >= [0 1]X + [0] = h(proper(X)) 361.11/116.58 problem: 361.11/116.58 strict: 361.11/116.58 361.11/116.58 weak: 361.11/116.58 proper(g(X)) -> g(proper(X)) 361.11/116.58 proper(f(X)) -> f(proper(X)) 361.11/116.58 h(ok(X)) -> ok(h(X)) 361.11/116.58 f(ok(X)) -> ok(f(X)) 361.11/116.58 g(ok(X)) -> ok(g(X)) 361.11/116.58 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.58 top(mark(X)) -> top(proper(X)) 361.11/116.58 top(ok(X)) -> top(active(X)) 361.11/116.58 active(f(X)) -> f(active(X)) 361.11/116.58 active(h(X)) -> h(active(X)) 361.11/116.58 f(mark(X)) -> mark(f(X)) 361.11/116.58 h(mark(X)) -> mark(h(X)) 361.11/116.58 proper(h(X)) -> h(proper(X)) 361.11/116.58 Qed 361.11/116.58 361.11/116.58 strict: 361.11/116.58 active(f(X)) -> f(active(X)) 361.11/116.58 active(h(X)) -> h(active(X)) 361.11/116.58 f(mark(X)) -> mark(f(X)) 361.11/116.58 h(mark(X)) -> mark(h(X)) 361.11/116.58 proper(h(X)) -> h(proper(X)) 361.11/116.58 weak: 361.11/116.58 proper(g(X)) -> g(proper(X)) 361.11/116.58 proper(f(X)) -> f(proper(X)) 361.11/116.58 h(ok(X)) -> ok(h(X)) 361.11/116.58 f(ok(X)) -> ok(f(X)) 361.11/116.58 g(ok(X)) -> ok(g(X)) 361.11/116.58 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.58 top(mark(X)) -> top(proper(X)) 361.11/116.58 top(ok(X)) -> top(active(X)) 361.11/116.58 Splitting Processor: 361.11/116.58 strict: 361.11/116.58 f(mark(X)) -> mark(f(X)) 361.11/116.58 weak: 361.11/116.58 proper(g(X)) -> g(proper(X)) 361.11/116.58 proper(f(X)) -> f(proper(X)) 361.11/116.58 h(ok(X)) -> ok(h(X)) 361.11/116.58 f(ok(X)) -> ok(f(X)) 361.11/116.58 g(ok(X)) -> ok(g(X)) 361.11/116.58 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.58 top(mark(X)) -> top(proper(X)) 361.11/116.58 top(ok(X)) -> top(active(X)) 361.11/116.58 active(f(X)) -> f(active(X)) 361.11/116.58 active(h(X)) -> h(active(X)) 361.11/116.58 h(mark(X)) -> mark(h(X)) 361.11/116.58 proper(h(X)) -> h(proper(X)) 361.11/116.58 Matrix Interpretation Processor: dim=4 361.11/116.58 361.11/116.58 max_matrix: 361.11/116.58 [1 1 1 1] 361.11/116.58 [0 1 0 1] 361.11/116.58 [0 0 0 1] 361.11/116.58 [0 0 0 0] 361.11/116.58 interpretation: 361.11/116.58 [1 0 1 0] [0] 361.11/116.58 [0 0 0 0] [1] 361.11/116.58 [top](x0) = [0 0 0 0]x0 + [0] 361.11/116.58 [0 0 0 0] [0], 361.11/116.58 361.11/116.58 [1 1 0 1] [0] 361.11/116.58 [0 1 0 1] [1] 361.11/116.58 [ok](x0) = [0 0 0 1]x0 + [0] 361.11/116.58 [0 0 0 0] [0], 361.11/116.58 361.11/116.58 [1 0 0 0] 361.11/116.58 [0 1 0 0] 361.11/116.58 [proper](x0) = [0 0 0 0]x0 361.11/116.58 [0 0 0 0] , 361.11/116.58 361.11/116.58 [1 0 0 0] 361.11/116.58 [0 1 0 0] 361.11/116.58 [mark](x0) = [0 0 0 0]x0 361.11/116.58 [0 0 0 0] , 361.11/116.58 361.11/116.58 [1 0 0 0] 361.11/116.58 [0 1 0 0] 361.11/116.58 [g](x0) = [0 0 0 1]x0 361.11/116.58 [0 0 0 0] , 361.11/116.58 361.11/116.58 [1 1 0 0] 361.11/116.58 [0 1 0 0] 361.11/116.58 [h](x0) = [0 0 0 0]x0 361.11/116.58 [0 0 0 0] , 361.11/116.58 361.11/116.58 [1 1 0 0] 361.11/116.58 [0 1 0 0] 361.11/116.58 [active](x0) = [0 0 0 0]x0 361.11/116.58 [0 0 0 0] , 361.11/116.58 361.11/116.58 [1 1 0 0] [0] 361.11/116.58 [0 1 0 0] [1] 361.11/116.58 [f](x0) = [0 0 0 0]x0 + [0] 361.11/116.58 [0 0 0 0] [0] 361.11/116.58 orientation: 361.11/116.58 [1 2 0 0] [1] [1 2 0 0] [0] 361.11/116.58 [0 1 0 0] [1] [0 1 0 0] [1] 361.11/116.58 active(f(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = f(active(X)) 361.11/116.58 [0 0 0 0] [0] [0 0 0 0] [0] 361.11/116.58 361.11/116.58 [1 2 0 0] [1 2 0 0] 361.11/116.58 [0 1 0 0] [0 1 0 0] 361.11/116.58 active(h(X)) = [0 0 0 0]X >= [0 0 0 0]X = h(active(X)) 361.11/116.58 [0 0 0 0] [0 0 0 0] 361.11/116.58 361.11/116.58 [1 1 0 0] [1 1 0 0] 361.11/116.59 [0 1 0 0] [0 1 0 0] 361.11/116.59 h(mark(X)) = [0 0 0 0]X >= [0 0 0 0]X = mark(h(X)) 361.11/116.59 [0 0 0 0] [0 0 0 0] 361.11/116.59 361.11/116.59 [1 1 0 0] [1 1 0 0] 361.11/116.59 [0 1 0 0] [0 1 0 0] 361.11/116.59 proper(h(X)) = [0 0 0 0]X >= [0 0 0 0]X = h(proper(X)) 361.11/116.59 [0 0 0 0] [0 0 0 0] 361.11/116.59 361.11/116.59 [1 1 0 0] [0] [1 1 0 0] [0] 361.11/116.59 [0 1 0 0] [1] [0 1 0 0] [1] 361.11/116.59 f(mark(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = mark(f(X)) 361.11/116.59 [0 0 0 0] [0] [0 0 0 0] [0] 361.11/116.59 361.11/116.59 [1 0 0 0] [1 0 0 0] 361.11/116.59 [0 1 0 0] [0 1 0 0] 361.11/116.59 proper(g(X)) = [0 0 0 0]X >= [0 0 0 0]X = g(proper(X)) 361.11/116.59 [0 0 0 0] [0 0 0 0] 361.11/116.59 361.11/116.59 [1 1 0 0] [0] [1 1 0 0] [0] 361.11/116.59 [0 1 0 0] [1] [0 1 0 0] [1] 361.11/116.59 proper(f(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = f(proper(X)) 361.11/116.59 [0 0 0 0] [0] [0 0 0 0] [0] 361.11/116.59 361.11/116.59 [1 2 0 2] [1] [1 2 0 0] [0] 361.11/116.59 [0 1 0 1] [1] [0 1 0 0] [1] 361.11/116.59 h(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = ok(h(X)) 361.11/116.59 [0 0 0 0] [0] [0 0 0 0] [0] 361.11/116.59 361.11/116.59 [1 2 0 2] [1] [1 2 0 0] [1] 361.11/116.59 [0 1 0 1] [2] [0 1 0 0] [2] 361.11/116.59 f(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = ok(f(X)) 361.11/116.59 [0 0 0 0] [0] [0 0 0 0] [0] 361.11/116.59 361.11/116.59 [1 1 0 1] [0] [1 1 0 0] [0] 361.11/116.59 [0 1 0 1] [1] [0 1 0 0] [1] 361.11/116.59 g(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = ok(g(X)) 361.11/116.59 [0 0 0 0] [0] [0 0 0 0] [0] 361.11/116.59 361.11/116.59 [1 2 0 0] [1] [1 2 0 0] [1] 361.11/116.59 [0 1 0 0] [1] [0 1 0 0] [1] 361.11/116.59 active(f(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = mark(g(h(f(X)))) 361.11/116.59 [0 0 0 0] [0] [0 0 0 0] [0] 361.11/116.59 361.11/116.59 [1 0 0 0] [0] [1 0 0 0] [0] 361.11/116.59 [0 0 0 0] [1] [0 0 0 0] [1] 361.11/116.59 top(mark(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = top(proper(X)) 361.11/116.59 [0 0 0 0] [0] [0 0 0 0] [0] 361.11/116.59 361.11/116.59 [1 1 0 2] [0] [1 1 0 0] [0] 361.11/116.59 [0 0 0 0] [1] [0 0 0 0] [1] 361.11/116.59 top(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = top(active(X)) 361.11/116.59 [0 0 0 0] [0] [0 0 0 0] [0] 361.11/116.59 problem: 361.11/116.59 strict: 361.11/116.59 active(h(X)) -> h(active(X)) 361.11/116.59 h(mark(X)) -> mark(h(X)) 361.11/116.59 proper(h(X)) -> h(proper(X)) 361.11/116.59 weak: 361.11/116.59 active(f(X)) -> f(active(X)) 361.11/116.59 f(mark(X)) -> mark(f(X)) 361.11/116.59 proper(g(X)) -> g(proper(X)) 361.11/116.59 proper(f(X)) -> f(proper(X)) 361.11/116.59 h(ok(X)) -> ok(h(X)) 361.11/116.59 f(ok(X)) -> ok(f(X)) 361.11/116.59 g(ok(X)) -> ok(g(X)) 361.11/116.59 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.59 top(mark(X)) -> top(proper(X)) 361.11/116.59 top(ok(X)) -> top(active(X)) 361.11/116.59 Splitting Processor: 361.11/116.59 strict: 361.11/116.59 active(h(X)) -> h(active(X)) 361.11/116.59 weak: 361.11/116.59 active(f(X)) -> f(active(X)) 361.11/116.59 f(mark(X)) -> mark(f(X)) 361.11/116.59 proper(g(X)) -> g(proper(X)) 361.11/116.59 proper(f(X)) -> f(proper(X)) 361.11/116.59 h(ok(X)) -> ok(h(X)) 361.11/116.59 f(ok(X)) -> ok(f(X)) 361.11/116.59 g(ok(X)) -> ok(g(X)) 361.11/116.59 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.59 top(mark(X)) -> top(proper(X)) 361.11/116.59 top(ok(X)) -> top(active(X)) 361.11/116.59 h(mark(X)) -> mark(h(X)) 361.11/116.59 proper(h(X)) -> h(proper(X)) 361.11/116.59 Matrix Interpretation Processor: dim=2 361.11/116.59 361.11/116.59 max_matrix: 361.11/116.59 [1 3] 361.11/116.59 [0 1] 361.11/116.59 interpretation: 361.11/116.59 [1 3] [1] 361.11/116.59 [top](x0) = [0 0]x0 + [0], 361.11/116.59 361.11/116.59 [1 3] [0] 361.11/116.59 [ok](x0) = [0 1]x0 + [3], 361.11/116.59 361.11/116.59 361.11/116.59 [proper](x0) = x0, 361.11/116.59 361.11/116.59 [1] 361.11/116.59 [mark](x0) = x0 + [0], 361.11/116.59 361.11/116.59 361.11/116.59 [g](x0) = x0, 361.11/116.59 361.11/116.59 [1 2] [0] 361.11/116.59 [h](x0) = [0 1]x0 + [2], 361.11/116.59 361.11/116.59 [1 3] [3] 361.11/116.59 [active](x0) = [0 1]x0 + [2], 361.11/116.59 361.11/116.59 [3] 361.11/116.59 [f](x0) = x0 + [0] 361.11/116.59 orientation: 361.11/116.59 [1 5] [9] [1 5] [7] 361.11/116.59 active(h(X)) = [0 1]X + [4] >= [0 1]X + [4] = h(active(X)) 361.11/116.59 361.11/116.59 [1 3] [6] [1 3] [6] 361.11/116.59 active(f(X)) = [0 1]X + [2] >= [0 1]X + [2] = f(active(X)) 361.11/116.59 361.11/116.59 [4] [4] 361.11/116.59 f(mark(X)) = X + [0] >= X + [0] = mark(f(X)) 361.11/116.59 361.11/116.59 361.11/116.59 proper(g(X)) = X >= X = g(proper(X)) 361.11/116.59 361.11/116.59 [3] [3] 361.11/116.59 proper(f(X)) = X + [0] >= X + [0] = f(proper(X)) 361.11/116.59 361.11/116.59 [1 5] [6] [1 5] [6] 361.11/116.59 h(ok(X)) = [0 1]X + [5] >= [0 1]X + [5] = ok(h(X)) 361.11/116.59 361.11/116.59 [1 3] [3] [1 3] [3] 361.11/116.59 f(ok(X)) = [0 1]X + [3] >= [0 1]X + [3] = ok(f(X)) 361.11/116.59 361.11/116.59 [1 3] [0] [1 3] [0] 361.11/116.59 g(ok(X)) = [0 1]X + [3] >= [0 1]X + [3] = ok(g(X)) 361.11/116.59 361.11/116.59 [1 3] [6] [1 2] [4] 361.11/116.59 active(f(X)) = [0 1]X + [2] >= [0 1]X + [2] = mark(g(h(f(X)))) 361.11/116.59 361.11/116.59 [1 3] [2] [1 3] [1] 361.11/116.59 top(mark(X)) = [0 0]X + [0] >= [0 0]X + [0] = top(proper(X)) 361.11/116.59 361.11/116.59 [1 6] [10] [1 6] [10] 361.11/116.59 top(ok(X)) = [0 0]X + [0 ] >= [0 0]X + [0 ] = top(active(X)) 361.11/116.59 361.11/116.59 [1 2] [1] [1 2] [1] 361.11/116.59 h(mark(X)) = [0 1]X + [2] >= [0 1]X + [2] = mark(h(X)) 361.11/116.59 361.11/116.59 [1 2] [0] [1 2] [0] 361.11/116.59 proper(h(X)) = [0 1]X + [2] >= [0 1]X + [2] = h(proper(X)) 361.11/116.59 problem: 361.11/116.59 strict: 361.11/116.59 361.11/116.59 weak: 361.11/116.59 active(h(X)) -> h(active(X)) 361.11/116.59 active(f(X)) -> f(active(X)) 361.11/116.59 f(mark(X)) -> mark(f(X)) 361.11/116.59 proper(g(X)) -> g(proper(X)) 361.11/116.59 proper(f(X)) -> f(proper(X)) 361.11/116.59 h(ok(X)) -> ok(h(X)) 361.11/116.59 f(ok(X)) -> ok(f(X)) 361.11/116.59 g(ok(X)) -> ok(g(X)) 361.11/116.59 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.59 top(mark(X)) -> top(proper(X)) 361.11/116.59 top(ok(X)) -> top(active(X)) 361.11/116.59 h(mark(X)) -> mark(h(X)) 361.11/116.59 proper(h(X)) -> h(proper(X)) 361.11/116.59 Qed 361.11/116.59 361.11/116.59 strict: 361.11/116.59 h(mark(X)) -> mark(h(X)) 361.11/116.59 proper(h(X)) -> h(proper(X)) 361.11/116.60 weak: 361.11/116.60 active(h(X)) -> h(active(X)) 361.11/116.60 active(f(X)) -> f(active(X)) 361.11/116.60 f(mark(X)) -> mark(f(X)) 361.11/116.60 proper(g(X)) -> g(proper(X)) 361.11/116.60 proper(f(X)) -> f(proper(X)) 361.11/116.60 h(ok(X)) -> ok(h(X)) 361.11/116.60 f(ok(X)) -> ok(f(X)) 361.11/116.60 g(ok(X)) -> ok(g(X)) 361.11/116.60 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.60 top(mark(X)) -> top(proper(X)) 361.11/116.60 top(ok(X)) -> top(active(X)) 361.11/116.60 Splitting Processor: 361.11/116.60 strict: 361.11/116.60 h(mark(X)) -> mark(h(X)) 361.11/116.60 weak: 361.11/116.60 active(h(X)) -> h(active(X)) 361.11/116.60 active(f(X)) -> f(active(X)) 361.11/116.60 f(mark(X)) -> mark(f(X)) 361.11/116.60 proper(g(X)) -> g(proper(X)) 361.11/116.60 proper(f(X)) -> f(proper(X)) 361.11/116.60 h(ok(X)) -> ok(h(X)) 361.11/116.60 f(ok(X)) -> ok(f(X)) 361.11/116.60 g(ok(X)) -> ok(g(X)) 361.11/116.60 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.60 top(mark(X)) -> top(proper(X)) 361.11/116.60 top(ok(X)) -> top(active(X)) 361.11/116.60 proper(h(X)) -> h(proper(X)) 361.11/116.60 Matrix Interpretation Processor: dim=2 361.11/116.60 361.11/116.60 max_matrix: 361.11/116.60 [1 2] 361.11/116.60 [0 1] 361.11/116.60 interpretation: 361.11/116.60 [1 0] [1] 361.11/116.60 [top](x0) = [0 0]x0 + [2], 361.11/116.60 361.11/116.60 [1 2] [0] 361.11/116.60 [ok](x0) = [0 1]x0 + [2], 361.11/116.60 361.11/116.60 361.11/116.60 [proper](x0) = x0, 361.11/116.60 361.11/116.60 [0] 361.11/116.60 [mark](x0) = x0 + [1], 361.11/116.60 361.11/116.60 361.11/116.60 [g](x0) = x0, 361.11/116.60 361.11/116.60 [1 1] [0] 361.11/116.60 [h](x0) = [0 1]x0 + [1], 361.11/116.60 361.11/116.60 [1 2] [0] 361.11/116.60 [active](x0) = [0 1]x0 + [2], 361.11/116.60 361.11/116.60 [1 2] [0] 361.11/116.60 [f](x0) = [0 1]x0 + [2] 361.11/116.60 orientation: 361.11/116.60 [1 1] [1] [1 1] [0] 361.11/116.60 h(mark(X)) = [0 1]X + [2] >= [0 1]X + [2] = mark(h(X)) 361.11/116.60 361.11/116.60 [1 3] [2] [1 3] [2] 361.11/116.60 active(h(X)) = [0 1]X + [3] >= [0 1]X + [3] = h(active(X)) 361.11/116.60 361.11/116.60 [1 4] [4] [1 4] [4] 361.11/116.60 active(f(X)) = [0 1]X + [4] >= [0 1]X + [4] = f(active(X)) 361.11/116.60 361.11/116.60 [1 2] [2] [1 2] [0] 361.11/116.60 f(mark(X)) = [0 1]X + [3] >= [0 1]X + [3] = mark(f(X)) 361.11/116.60 361.11/116.60 361.11/116.60 proper(g(X)) = X >= X = g(proper(X)) 361.11/116.60 361.11/116.60 [1 2] [0] [1 2] [0] 361.11/116.60 proper(f(X)) = [0 1]X + [2] >= [0 1]X + [2] = f(proper(X)) 361.11/116.60 361.11/116.60 [1 3] [2] [1 3] [2] 361.11/116.60 h(ok(X)) = [0 1]X + [3] >= [0 1]X + [3] = ok(h(X)) 361.11/116.60 361.11/116.60 [1 4] [4] [1 4] [4] 361.11/116.60 f(ok(X)) = [0 1]X + [4] >= [0 1]X + [4] = ok(f(X)) 361.11/116.60 361.11/116.60 [1 2] [0] [1 2] [0] 361.11/116.60 g(ok(X)) = [0 1]X + [2] >= [0 1]X + [2] = ok(g(X)) 361.11/116.60 361.11/116.60 [1 4] [4] [1 3] [2] 361.11/116.60 active(f(X)) = [0 1]X + [4] >= [0 1]X + [4] = mark(g(h(f(X)))) 361.11/116.60 361.11/116.60 [1 0] [1] [1 0] [1] 361.11/116.60 top(mark(X)) = [0 0]X + [2] >= [0 0]X + [2] = top(proper(X)) 361.11/116.60 361.11/116.60 [1 2] [1] [1 2] [1] 361.11/116.60 top(ok(X)) = [0 0]X + [2] >= [0 0]X + [2] = top(active(X)) 361.11/116.60 361.11/116.60 [1 1] [0] [1 1] [0] 361.11/116.60 proper(h(X)) = [0 1]X + [1] >= [0 1]X + [1] = h(proper(X)) 361.11/116.60 problem: 361.11/116.60 strict: 361.11/116.60 361.11/116.60 weak: 361.11/116.60 h(mark(X)) -> mark(h(X)) 361.11/116.60 active(h(X)) -> h(active(X)) 361.11/116.60 active(f(X)) -> f(active(X)) 361.11/116.60 f(mark(X)) -> mark(f(X)) 361.11/116.60 proper(g(X)) -> g(proper(X)) 361.11/116.60 proper(f(X)) -> f(proper(X)) 361.11/116.60 h(ok(X)) -> ok(h(X)) 361.11/116.60 f(ok(X)) -> ok(f(X)) 361.11/116.60 g(ok(X)) -> ok(g(X)) 361.11/116.60 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.60 top(mark(X)) -> top(proper(X)) 361.11/116.60 top(ok(X)) -> top(active(X)) 361.11/116.60 proper(h(X)) -> h(proper(X)) 361.11/116.60 Qed 361.11/116.60 361.11/116.60 strict: 361.11/116.60 proper(h(X)) -> h(proper(X)) 361.11/116.60 weak: 361.11/116.60 h(mark(X)) -> mark(h(X)) 361.11/116.60 active(h(X)) -> h(active(X)) 361.11/116.60 active(f(X)) -> f(active(X)) 361.11/116.60 f(mark(X)) -> mark(f(X)) 361.11/116.60 proper(g(X)) -> g(proper(X)) 361.11/116.60 proper(f(X)) -> f(proper(X)) 361.11/116.60 h(ok(X)) -> ok(h(X)) 361.11/116.60 f(ok(X)) -> ok(f(X)) 361.11/116.60 g(ok(X)) -> ok(g(X)) 361.11/116.60 active(f(X)) -> mark(g(h(f(X)))) 361.11/116.60 top(mark(X)) -> top(proper(X)) 361.11/116.60 top(ok(X)) -> top(active(X)) 361.11/116.60 Matrix Interpretation Processor: dim=2 361.11/116.60 361.11/116.60 max_matrix: 361.11/116.60 [1 3] 361.11/116.60 [0 1] 361.11/116.60 interpretation: 361.11/116.60 [1 2] 361.11/116.60 [top](x0) = [0 0]x0, 361.11/116.60 361.11/116.60 [1 3] [2] 361.11/116.60 [ok](x0) = [0 1]x0 + [3], 361.11/116.60 361.11/116.60 [1 2] [1] 361.11/116.60 [proper](x0) = [0 1]x0 + [1], 361.11/116.60 361.11/116.60 [1 2] [0] 361.11/116.60 [mark](x0) = [0 1]x0 + [2], 361.11/116.60 361.11/116.60 361.11/116.60 [g](x0) = x0, 361.11/116.60 361.11/116.60 [1 1] [0] 361.11/116.60 [h](x0) = [0 1]x0 + [1], 361.11/116.60 361.11/116.60 [1 3] [2] 361.11/116.60 [active](x0) = [0 1]x0 + [3], 361.11/116.60 361.11/116.60 361.11/116.60 [f](x0) = x0 361.11/116.60 orientation: 361.11/116.60 [1 3] [3] [1 3] [2] 361.11/116.60 proper(h(X)) = [0 1]X + [2] >= [0 1]X + [2] = h(proper(X)) 361.11/116.60 361.11/116.60 [1 3] [2] [1 3] [2] 361.11/116.60 h(mark(X)) = [0 1]X + [3] >= [0 1]X + [3] = mark(h(X)) 361.11/116.60 361.11/116.60 [1 4] [5] [1 4] [5] 361.11/116.60 active(h(X)) = [0 1]X + [4] >= [0 1]X + [4] = h(active(X)) 361.11/116.60 361.11/116.60 [1 3] [2] [1 3] [2] 361.11/116.60 active(f(X)) = [0 1]X + [3] >= [0 1]X + [3] = f(active(X)) 361.11/116.60 361.11/116.60 [1 2] [0] [1 2] [0] 361.11/116.60 f(mark(X)) = [0 1]X + [2] >= [0 1]X + [2] = mark(f(X)) 361.11/116.60 361.11/116.60 [1 2] [1] [1 2] [1] 361.11/116.60 proper(g(X)) = [0 1]X + [1] >= [0 1]X + [1] = g(proper(X)) 361.11/116.60 361.11/116.60 [1 2] [1] [1 2] [1] 361.11/116.60 proper(f(X)) = [0 1]X + [1] >= [0 1]X + [1] = f(proper(X)) 361.11/116.60 361.11/116.60 [1 4] [5] [1 4] [5] 361.11/116.60 h(ok(X)) = [0 1]X + [4] >= [0 1]X + [4] = ok(h(X)) 361.11/116.60 361.11/116.60 [1 3] [2] [1 3] [2] 361.11/116.60 f(ok(X)) = [0 1]X + [3] >= [0 1]X + [3] = ok(f(X)) 361.11/116.60 361.11/116.60 [1 3] [2] [1 3] [2] 361.11/116.60 g(ok(X)) = [0 1]X + [3] >= [0 1]X + [3] = ok(g(X)) 361.11/116.60 361.11/116.60 [1 3] [2] [1 3] [2] 361.11/116.60 active(f(X)) = [0 1]X + [3] >= [0 1]X + [3] = mark(g(h(f(X)))) 361.11/116.60 361.11/116.60 [1 4] [4] [1 4] [3] 361.21/116.60 top(mark(X)) = [0 0]X + [0] >= [0 0]X + [0] = top(proper(X)) 361.21/116.60 361.21/116.60 [1 5] [8] [1 5] [8] 361.21/116.60 top(ok(X)) = [0 0]X + [0] >= [0 0]X + [0] = top(active(X)) 361.21/116.60 problem: 361.21/116.60 strict: 361.21/116.60 361.21/116.60 weak: 361.21/116.60 proper(h(X)) -> h(proper(X)) 361.21/116.60 h(mark(X)) -> mark(h(X)) 361.21/116.60 active(h(X)) -> h(active(X)) 361.21/116.60 active(f(X)) -> f(active(X)) 361.21/116.60 f(mark(X)) -> mark(f(X)) 361.21/116.60 proper(g(X)) -> g(proper(X)) 361.21/116.60 proper(f(X)) -> f(proper(X)) 361.21/116.60 h(ok(X)) -> ok(h(X)) 361.21/116.60 f(ok(X)) -> ok(f(X)) 361.21/116.60 g(ok(X)) -> ok(g(X)) 361.21/116.60 active(f(X)) -> mark(g(h(f(X)))) 361.21/116.60 top(mark(X)) -> top(proper(X)) 361.21/116.60 top(ok(X)) -> top(active(X)) 361.21/116.60 Qed 361.21/116.60 361.21/116.60 strict: 361.21/116.60 active(f(X)) -> f(active(X)) 361.21/116.60 active(h(X)) -> h(active(X)) 361.21/116.60 h(mark(X)) -> mark(h(X)) 361.21/116.60 proper(h(X)) -> h(proper(X)) 361.21/116.60 weak: 361.21/116.60 f(mark(X)) -> mark(f(X)) 361.21/116.60 proper(g(X)) -> g(proper(X)) 361.21/116.60 proper(f(X)) -> f(proper(X)) 361.21/116.60 h(ok(X)) -> ok(h(X)) 361.21/116.60 f(ok(X)) -> ok(f(X)) 361.21/116.60 g(ok(X)) -> ok(g(X)) 361.21/116.60 active(f(X)) -> mark(g(h(f(X)))) 361.21/116.60 top(mark(X)) -> top(proper(X)) 361.21/116.60 top(ok(X)) -> top(active(X)) 361.21/116.60 Matrix Interpretation Processor: dim=3 361.21/116.60 361.21/116.60 max_matrix: 361.21/116.60 [1 0 1] 361.21/116.60 [0 0 1] 361.21/116.60 [0 0 1] 361.21/116.60 interpretation: 361.21/116.60 [1 0 0] 361.21/116.60 [top](x0) = [0 0 1]x0 361.21/116.60 [0 0 1] , 361.21/116.60 361.21/116.60 [1 0 1] [1] 361.21/116.60 [ok](x0) = [0 0 0]x0 + [0] 361.21/116.60 [0 0 1] [1], 361.21/116.60 361.21/116.60 [1 0 0] [0] 361.21/116.60 [proper](x0) = [0 0 0]x0 + [1] 361.21/116.60 [0 0 1] [0], 361.21/116.60 361.21/116.60 [1 0 0] [0] 361.21/116.60 [mark](x0) = [0 0 0]x0 + [0] 361.21/116.60 [0 0 1] [1], 361.21/116.60 361.21/116.60 [1 0 1] 361.21/116.60 [g](x0) = [0 0 0]x0 361.21/116.60 [0 0 1] , 361.21/116.60 361.21/116.60 [1 0 0] 361.21/116.60 [h](x0) = [0 0 0]x0 361.21/116.60 [0 0 1] , 361.21/116.60 361.21/116.60 [1 0 1] [1] 361.21/116.60 [active](x0) = [0 0 0]x0 + [0] 361.21/116.60 [0 0 1] [1], 361.21/116.60 361.21/116.60 [1 0 1] [0] 361.21/116.60 [f](x0) = [0 0 0]x0 + [0] 361.21/116.60 [0 0 1] [1] 361.21/116.60 orientation: 361.21/116.60 [1 0 1] [1] [1 0 1] [0] 361.21/116.60 f(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(f(X)) 361.21/116.60 [0 0 1] [2] [0 0 1] [2] 361.21/116.60 361.21/116.60 [1 0 1] [0] [1 0 1] 361.21/116.60 proper(g(X)) = [0 0 0]X + [1] >= [0 0 0]X = g(proper(X)) 361.21/116.60 [0 0 1] [0] [0 0 1] 361.21/116.60 361.21/116.60 [1 0 1] [0] [1 0 1] [0] 361.21/116.60 proper(f(X)) = [0 0 0]X + [1] >= [0 0 0]X + [0] = f(proper(X)) 361.21/116.60 [0 0 1] [1] [0 0 1] [1] 361.21/116.60 361.21/116.60 [1 0 1] [1] [1 0 1] [1] 361.21/116.60 h(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(h(X)) 361.21/116.60 [0 0 1] [1] [0 0 1] [1] 361.21/116.60 361.21/116.60 [1 0 2] [2] [1 0 2] [2] 361.21/116.60 f(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(f(X)) 361.21/116.60 [0 0 1] [2] [0 0 1] [2] 361.21/116.60 361.21/116.60 [1 0 2] [2] [1 0 2] [1] 361.21/116.60 g(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(g(X)) 361.21/116.60 [0 0 1] [1] [0 0 1] [1] 361.21/116.60 361.21/116.60 [1 0 2] [2] [1 0 2] [1] 361.21/116.61 active(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(g(h(f(X)))) 361.21/116.61 [0 0 1] [2] [0 0 1] [2] 361.21/116.61 361.21/116.61 [1 0 0] [0] [1 0 0] 361.21/116.61 top(mark(X)) = [0 0 1]X + [1] >= [0 0 1]X = top(proper(X)) 361.21/116.61 [0 0 1] [1] [0 0 1] 361.21/116.61 361.21/116.61 [1 0 1] [1] [1 0 1] [1] 361.21/116.61 top(ok(X)) = [0 0 1]X + [1] >= [0 0 1]X + [1] = top(active(X)) 361.21/116.61 [0 0 1] [1] [0 0 1] [1] 361.21/116.61 361.21/116.61 [1 0 2] [2] [1 0 2] [2] 361.21/116.61 active(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = f(active(X)) 361.21/116.61 [0 0 1] [2] [0 0 1] [2] 361.21/116.61 361.21/116.61 [1 0 1] [1] [1 0 1] [1] 361.21/116.61 active(h(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = h(active(X)) 361.21/116.61 [0 0 1] [1] [0 0 1] [1] 361.21/116.61 361.21/116.61 [1 0 0] [0] [1 0 0] [0] 361.21/116.61 h(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(h(X)) 361.21/116.61 [0 0 1] [1] [0 0 1] [1] 361.21/116.61 361.21/116.61 [1 0 0] [0] [1 0 0] 361.21/116.61 proper(h(X)) = [0 0 0]X + [1] >= [0 0 0]X = h(proper(X)) 361.21/116.61 [0 0 1] [0] [0 0 1] 361.21/116.61 problem: 361.21/116.61 strict: 361.21/116.61 361.21/116.61 weak: 361.21/116.61 f(mark(X)) -> mark(f(X)) 361.21/116.61 proper(g(X)) -> g(proper(X)) 361.21/116.61 proper(f(X)) -> f(proper(X)) 361.21/116.61 h(ok(X)) -> ok(h(X)) 361.21/116.61 f(ok(X)) -> ok(f(X)) 361.21/116.61 g(ok(X)) -> ok(g(X)) 361.21/116.61 active(f(X)) -> mark(g(h(f(X)))) 361.21/116.61 top(mark(X)) -> top(proper(X)) 361.21/116.61 top(ok(X)) -> top(active(X)) 361.21/116.61 active(f(X)) -> f(active(X)) 361.21/116.61 active(h(X)) -> h(active(X)) 361.21/116.61 h(mark(X)) -> mark(h(X)) 361.21/116.61 proper(h(X)) -> h(proper(X)) 361.21/116.61 Qed 361.21/116.61 361.21/116.61 strict: 361.21/116.61 active(f(X)) -> f(active(X)) 361.21/116.61 active(h(X)) -> h(active(X)) 361.21/116.61 f(mark(X)) -> mark(f(X)) 361.21/116.61 h(mark(X)) -> mark(h(X)) 361.21/116.61 proper(f(X)) -> f(proper(X)) 361.21/116.61 proper(g(X)) -> g(proper(X)) 361.21/116.61 proper(h(X)) -> h(proper(X)) 361.21/116.61 weak: 361.21/116.61 h(ok(X)) -> ok(h(X)) 361.21/116.61 f(ok(X)) -> ok(f(X)) 361.21/116.61 g(ok(X)) -> ok(g(X)) 361.21/116.61 active(f(X)) -> mark(g(h(f(X)))) 361.21/116.61 top(mark(X)) -> top(proper(X)) 361.21/116.61 top(ok(X)) -> top(active(X)) 361.21/116.61 Matrix Interpretation Processor: dim=3 361.21/116.61 361.21/116.61 max_matrix: 361.21/116.61 [1 0 1] 361.21/116.61 [0 0 1] 361.21/116.61 [0 0 1] 361.21/116.61 interpretation: 361.21/116.61 [1 0 0] 361.21/116.61 [top](x0) = [0 0 1]x0 361.21/116.61 [0 0 0] , 361.21/116.61 361.21/116.61 [1 0 1] [1] 361.21/116.61 [ok](x0) = [0 0 0]x0 + [0] 361.21/116.61 [0 0 1] [1], 361.21/116.61 361.21/116.61 [1 0 0] [0] 361.21/116.61 [proper](x0) = [0 0 0]x0 + [1] 361.21/116.61 [0 0 0] [0], 361.21/116.61 361.21/116.61 [1 0 0] 361.21/116.61 [mark](x0) = [0 0 0]x0 361.21/116.61 [0 0 1] , 361.21/116.61 361.21/116.61 [1 0 0] 361.21/116.61 [g](x0) = [0 0 0]x0 361.21/116.61 [0 0 1] , 361.21/116.61 361.21/116.61 [1 0 1] [1] 361.21/116.61 [h](x0) = [0 0 0]x0 + [1] 361.21/116.61 [0 0 1] [0], 361.21/116.61 361.21/116.61 [1 0 1] [1] 361.21/116.61 [active](x0) = [0 0 1]x0 + [1] 361.21/116.61 [0 0 1] [0], 361.21/116.61 361.21/116.61 [1 0 0] [1] 361.21/116.61 [f](x0) = [0 0 1]x0 + [1] 361.21/116.61 [0 0 1] [0] 361.21/116.61 orientation: 361.21/116.61 [1 0 2] [3] [1 0 2] [2] 361.21/116.61 h(ok(X)) = [0 0 0]X + [1] >= [0 0 0]X + [0] = ok(h(X)) 361.21/116.61 [0 0 1] [1] [0 0 1] [1] 361.21/116.61 361.21/116.61 [1 0 1] [2] [1 0 1] [2] 361.21/116.61 f(ok(X)) = [0 0 1]X + [2] >= [0 0 0]X + [0] = ok(f(X)) 361.21/116.61 [0 0 1] [1] [0 0 1] [1] 361.21/116.61 361.21/116.61 [1 0 1] [1] [1 0 1] [1] 361.21/116.61 g(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = ok(g(X)) 361.21/116.61 [0 0 1] [1] [0 0 1] [1] 361.21/116.61 361.21/116.61 [1 0 1] [2] [1 0 1] [2] 361.21/116.61 active(f(X)) = [0 0 1]X + [1] >= [0 0 0]X + [0] = mark(g(h(f(X)))) 361.21/116.61 [0 0 1] [0] [0 0 1] [0] 361.21/116.61 361.21/116.61 [1 0 0] [1 0 0] 361.21/116.61 top(mark(X)) = [0 0 1]X >= [0 0 0]X = top(proper(X)) 361.21/116.61 [0 0 0] [0 0 0] 361.21/116.61 361.21/116.61 [1 0 1] [1] [1 0 1] [1] 361.21/116.61 top(ok(X)) = [0 0 1]X + [1] >= [0 0 1]X + [0] = top(active(X)) 361.21/116.61 [0 0 0] [0] [0 0 0] [0] 361.21/116.61 361.21/116.61 [1 0 1] [2] [1 0 1] [2] 361.21/116.61 active(f(X)) = [0 0 1]X + [1] >= [0 0 1]X + [1] = f(active(X)) 361.21/116.61 [0 0 1] [0] [0 0 1] [0] 361.21/116.61 361.21/116.61 [1 0 2] [2] [1 0 2] [2] 361.21/116.61 active(h(X)) = [0 0 1]X + [1] >= [0 0 0]X + [1] = h(active(X)) 361.21/116.61 [0 0 1] [0] [0 0 1] [0] 361.21/116.61 361.21/116.61 [1 0 0] [1] [1 0 0] [1] 361.21/116.61 f(mark(X)) = [0 0 1]X + [1] >= [0 0 0]X + [0] = mark(f(X)) 361.21/116.61 [0 0 1] [0] [0 0 1] [0] 361.21/116.61 361.21/116.61 [1 0 1] [1] [1 0 1] [1] 361.21/116.61 h(mark(X)) = [0 0 0]X + [1] >= [0 0 0]X + [0] = mark(h(X)) 361.21/116.61 [0 0 1] [0] [0 0 1] [0] 361.21/116.61 361.21/116.61 [1 0 0] [1] [1 0 0] [1] 361.21/116.62 proper(f(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = f(proper(X)) 361.21/116.62 [0 0 0] [0] [0 0 0] [0] 361.21/116.62 361.21/116.62 [1 0 0] [0] [1 0 0] 361.21/116.62 proper(g(X)) = [0 0 0]X + [1] >= [0 0 0]X = g(proper(X)) 361.21/116.62 [0 0 0] [0] [0 0 0] 361.21/116.62 361.21/116.62 [1 0 1] [1] [1 0 0] [1] 361.21/116.62 proper(h(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = h(proper(X)) 361.21/116.62 [0 0 0] [0] [0 0 0] [0] 361.21/116.62 problem: 361.21/116.62 strict: 361.21/116.62 361.21/116.62 weak: 361.21/116.62 h(ok(X)) -> ok(h(X)) 361.21/116.62 f(ok(X)) -> ok(f(X)) 361.21/116.62 g(ok(X)) -> ok(g(X)) 361.21/116.62 active(f(X)) -> mark(g(h(f(X)))) 361.21/116.62 top(mark(X)) -> top(proper(X)) 361.21/116.62 top(ok(X)) -> top(active(X)) 361.21/116.62 active(f(X)) -> f(active(X)) 361.21/116.62 active(h(X)) -> h(active(X)) 361.21/116.62 f(mark(X)) -> mark(f(X)) 361.21/116.62 h(mark(X)) -> mark(h(X)) 361.21/116.62 proper(f(X)) -> f(proper(X)) 361.21/116.62 proper(g(X)) -> g(proper(X)) 361.21/116.62 proper(h(X)) -> h(proper(X)) 361.21/116.62 Qed 361.21/116.62 361.21/116.62 strict: 361.21/116.62 active(f(X)) -> f(active(X)) 361.21/116.62 active(h(X)) -> h(active(X)) 361.21/116.62 f(mark(X)) -> mark(f(X)) 361.21/116.62 h(mark(X)) -> mark(h(X)) 361.21/116.62 proper(f(X)) -> f(proper(X)) 361.21/116.62 proper(g(X)) -> g(proper(X)) 361.21/116.62 proper(h(X)) -> h(proper(X)) 361.21/116.62 f(ok(X)) -> ok(f(X)) 361.21/116.62 h(ok(X)) -> ok(h(X)) 361.21/116.62 weak: 361.21/116.62 g(ok(X)) -> ok(g(X)) 361.21/116.62 active(f(X)) -> mark(g(h(f(X)))) 361.21/116.62 top(mark(X)) -> top(proper(X)) 361.21/116.62 top(ok(X)) -> top(active(X)) 361.21/116.62 Matrix Interpretation Processor: dim=4 361.21/116.62 361.21/116.62 max_matrix: 361.21/116.62 [1 0 0 1] 361.21/116.62 [0 0 1 1] 361.21/116.62 [0 0 0 1] 361.21/116.62 [0 0 0 1] 361.21/116.62 interpretation: 361.21/116.62 [1 0 0 0] [0] 361.21/116.62 [0 0 0 0] [0] 361.21/116.62 [top](x0) = [0 0 0 1]x0 + [0] 361.21/116.62 [0 0 0 1] [1], 361.21/116.62 361.21/116.62 [1 0 0 1] [1] 361.21/116.62 [0 0 0 0] [0] 361.21/116.62 [ok](x0) = [0 0 0 0]x0 + [1] 361.21/116.62 [0 0 0 1] [1], 361.21/116.62 361.21/116.62 [1 0 0 0] [0] 361.21/116.62 [0 0 0 1] [1] 361.21/116.62 [proper](x0) = [0 0 0 1]x0 + [1] 361.21/116.62 [0 0 0 0] [0], 361.21/116.62 361.21/116.62 [1 0 0 0] 361.21/116.62 [0 0 0 0] 361.21/116.62 [mark](x0) = [0 0 0 0]x0 361.21/116.62 [0 0 0 0] , 361.21/116.62 361.21/116.62 [1 0 0 1] [0] 361.21/116.62 [0 0 0 1] [0] 361.21/116.62 [g](x0) = [0 0 0 1]x0 + [1] 361.21/116.62 [0 0 0 1] [0], 361.21/116.62 361.21/116.62 [1 0 0 0] [0] 361.21/116.62 [0 0 1 1] [0] 361.21/116.62 [h](x0) = [0 0 0 1]x0 + [1] 361.21/116.62 [0 0 0 1] [0], 361.21/116.62 361.21/116.62 [1 0 0 1] [1] 361.21/116.62 [0 0 1 1] [1] 361.21/116.62 [active](x0) = [0 0 0 1]x0 + [1] 361.21/116.62 [0 0 0 0] [0], 361.21/116.62 361.21/116.62 [1 0 0 0] 361.21/116.62 [0 0 1 1] 361.21/116.62 [f](x0) = [0 0 0 1]x0 361.21/116.62 [0 0 0 1] 361.21/116.62 orientation: 361.21/116.62 [1 0 0 2] [2] [1 0 0 2] [1] 361.21/116.62 [0 0 0 1] [1] [0 0 0 0] [0] 361.21/116.62 g(ok(X)) = [0 0 0 1]X + [2] >= [0 0 0 0]X + [1] = ok(g(X)) 361.21/116.62 [0 0 0 1] [1] [0 0 0 1] [1] 361.21/116.62 361.21/116.62 [1 0 0 1] [1] [1 0 0 1] 361.21/116.62 [0 0 0 2] [1] [0 0 0 0] 361.21/116.62 active(f(X)) = [0 0 0 1]X + [1] >= [0 0 0 0]X = mark(g(h(f(X)))) 361.21/116.62 [0 0 0 0] [0] [0 0 0 0] 361.21/116.62 361.21/116.62 [1 0 0 0] [0] [1 0 0 0] [0] 361.21/116.62 [0 0 0 0] [0] [0 0 0 0] [0] 361.21/116.62 top(mark(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = top(proper(X)) 361.21/116.62 [0 0 0 0] [1] [0 0 0 0] [1] 361.21/116.62 361.21/116.62 [1 0 0 1] [1] [1 0 0 1] [1] 361.21/116.62 [0 0 0 0] [0] [0 0 0 0] [0] 361.21/116.62 top(ok(X)) = [0 0 0 1]X + [1] >= [0 0 0 0]X + [0] = top(active(X)) 361.21/116.62 [0 0 0 1] [2] [0 0 0 0] [1] 361.21/116.62 361.21/116.62 [1 0 0 1] [1] [1 0 0 1] [1] 361.21/116.62 [0 0 0 2] [1] [0 0 0 1] [1] 361.21/116.62 active(f(X)) = [0 0 0 1]X + [1] >= [0 0 0 0]X + [0] = f(active(X)) 361.21/116.62 [0 0 0 0] [0] [0 0 0 0] [0] 361.21/116.62 361.21/116.62 [1 0 0 1] [1] [1 0 0 1] [1] 361.21/116.62 [0 0 0 2] [2] [0 0 0 1] [1] 361.21/116.62 active(h(X)) = [0 0 0 1]X + [1] >= [0 0 0 0]X + [1] = h(active(X)) 361.21/116.62 [0 0 0 0] [0] [0 0 0 0] [0] 361.21/116.62 361.21/116.62 [1 0 0 0] [1 0 0 0] 361.21/116.62 [0 0 0 0] [0 0 0 0] 361.21/116.62 f(mark(X)) = [0 0 0 0]X >= [0 0 0 0]X = mark(f(X)) 361.21/116.62 [0 0 0 0] [0 0 0 0] 361.21/116.62 361.21/116.62 [1 0 0 0] [0] [1 0 0 0] 361.21/116.62 [0 0 0 0] [0] [0 0 0 0] 361.21/116.62 h(mark(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X = mark(h(X)) 361.21/116.62 [0 0 0 0] [0] [0 0 0 0] 361.21/116.62 361.21/116.62 [1 0 0 0] [0] [1 0 0 0] [0] 361.21/116.62 [0 0 0 1] [1] [0 0 0 1] [1] 361.21/116.62 proper(f(X)) = [0 0 0 1]X + [1] >= [0 0 0 0]X + [0] = f(proper(X)) 361.21/116.62 [0 0 0 0] [0] [0 0 0 0] [0] 361.21/116.62 361.21/116.62 [1 0 0 1] [0] [1 0 0 0] [0] 361.21/116.62 [0 0 0 1] [1] [0 0 0 0] [0] 361.21/116.62 proper(g(X)) = [0 0 0 1]X + [1] >= [0 0 0 0]X + [1] = g(proper(X)) 361.21/116.62 [0 0 0 0] [0] [0 0 0 0] [0] 361.21/116.62 361.21/116.62 [1 0 0 0] [0] [1 0 0 0] [0] 361.21/116.62 [0 0 0 1] [1] [0 0 0 1] [1] 361.21/116.62 proper(h(X)) = [0 0 0 1]X + [1] >= [0 0 0 0]X + [1] = h(proper(X)) 361.21/116.62 [0 0 0 0] [0] [0 0 0 0] [0] 361.21/116.62 361.21/116.62 [1 0 0 1] [1] [1 0 0 1] [1] 361.21/116.62 [0 0 0 1] [2] [0 0 0 0] [0] 361.21/116.62 f(ok(X)) = [0 0 0 1]X + [1] >= [0 0 0 0]X + [1] = ok(f(X)) 361.21/116.62 [0 0 0 1] [1] [0 0 0 1] [1] 361.21/116.62 361.21/116.62 [1 0 0 1] [1] [1 0 0 1] [1] 361.21/116.62 [0 0 0 1] [2] [0 0 0 0] [0] 361.21/116.62 h(ok(X)) = [0 0 0 1]X + [2] >= [0 0 0 0]X + [1] = ok(h(X)) 361.21/116.62 [0 0 0 1] [1] [0 0 0 1] [1] 361.21/116.62 problem: 361.21/116.62 strict: 361.21/116.62 361.21/116.62 weak: 361.21/116.62 g(ok(X)) -> ok(g(X)) 361.21/116.62 active(f(X)) -> mark(g(h(f(X)))) 361.21/116.62 top(mark(X)) -> top(proper(X)) 361.21/116.62 top(ok(X)) -> top(active(X)) 361.21/116.62 active(f(X)) -> f(active(X)) 361.21/116.62 active(h(X)) -> h(active(X)) 361.21/116.62 f(mark(X)) -> mark(f(X)) 361.21/116.62 h(mark(X)) -> mark(h(X)) 361.21/116.62 proper(f(X)) -> f(proper(X)) 361.21/116.62 proper(g(X)) -> g(proper(X)) 361.21/116.62 proper(h(X)) -> h(proper(X)) 361.21/116.62 f(ok(X)) -> ok(f(X)) 361.21/116.62 h(ok(X)) -> ok(h(X)) 361.21/116.62 Qed 361.21/116.63 EOF