YES(?,O(n^3)) 499.90/254.97 YES(?,O(n^3)) 499.90/254.98 499.90/254.98 Problem: 499.90/254.98 active(f(f(a()))) -> mark(f(g(f(a())))) 499.90/254.98 active(f(X)) -> f(active(X)) 499.90/254.98 f(mark(X)) -> mark(f(X)) 499.90/254.98 proper(f(X)) -> f(proper(X)) 499.90/254.98 proper(a()) -> ok(a()) 499.90/254.98 proper(g(X)) -> g(proper(X)) 499.90/254.98 f(ok(X)) -> ok(f(X)) 499.90/254.98 g(ok(X)) -> ok(g(X)) 499.90/254.98 top(mark(X)) -> top(proper(X)) 499.90/254.98 top(ok(X)) -> top(active(X)) 499.90/254.98 499.90/254.98 Proof: 499.90/254.98 Complexity Transformation Processor: 499.90/254.98 strict: 499.90/254.98 active(f(f(a()))) -> mark(f(g(f(a())))) 499.90/254.98 active(f(X)) -> f(active(X)) 499.90/254.98 f(mark(X)) -> mark(f(X)) 499.90/254.98 proper(f(X)) -> f(proper(X)) 499.90/254.98 proper(a()) -> ok(a()) 499.90/254.98 proper(g(X)) -> g(proper(X)) 499.90/254.98 f(ok(X)) -> ok(f(X)) 499.90/254.98 g(ok(X)) -> ok(g(X)) 499.90/254.98 top(mark(X)) -> top(proper(X)) 499.90/254.98 top(ok(X)) -> top(active(X)) 499.90/254.98 weak: 499.90/254.98 499.90/254.98 Matrix Interpretation Processor: dim=1 499.90/254.98 499.90/254.98 max_matrix: 499.90/254.98 1 499.90/254.98 interpretation: 499.90/254.98 [top](x0) = x0 + 1, 499.90/254.98 499.90/254.98 [ok](x0) = x0 + 6, 499.90/254.98 499.90/254.98 [proper](x0) = x0 + 2, 499.90/254.98 499.90/254.98 [mark](x0) = x0 + 4, 499.90/254.98 499.90/254.98 [g](x0) = x0 + 14, 499.90/254.98 499.90/254.98 [active](x0) = x0 + 1, 499.90/254.98 499.90/254.98 [f](x0) = x0 + 4, 499.90/254.98 499.90/254.98 [a] = 4 499.90/254.98 orientation: 499.90/254.98 active(f(f(a()))) = 13 >= 30 = mark(f(g(f(a())))) 499.90/254.98 499.90/254.98 active(f(X)) = X + 5 >= X + 5 = f(active(X)) 499.90/254.98 499.90/254.98 f(mark(X)) = X + 8 >= X + 8 = mark(f(X)) 499.90/254.98 499.90/254.98 proper(f(X)) = X + 6 >= X + 6 = f(proper(X)) 499.90/254.98 499.90/254.98 proper(a()) = 6 >= 10 = ok(a()) 499.90/254.98 499.90/254.98 proper(g(X)) = X + 16 >= X + 16 = g(proper(X)) 499.90/254.98 499.90/254.98 f(ok(X)) = X + 10 >= X + 10 = ok(f(X)) 499.90/254.98 499.90/254.98 g(ok(X)) = X + 20 >= X + 20 = ok(g(X)) 499.90/254.98 499.90/254.98 top(mark(X)) = X + 5 >= X + 3 = top(proper(X)) 499.90/254.98 499.90/254.98 top(ok(X)) = X + 7 >= X + 2 = top(active(X)) 499.90/254.98 problem: 499.90/254.98 strict: 499.90/254.98 active(f(f(a()))) -> mark(f(g(f(a())))) 499.90/254.98 active(f(X)) -> f(active(X)) 499.90/254.98 f(mark(X)) -> mark(f(X)) 499.90/254.98 proper(f(X)) -> f(proper(X)) 499.90/254.98 proper(a()) -> ok(a()) 499.90/254.98 proper(g(X)) -> g(proper(X)) 499.90/254.98 f(ok(X)) -> ok(f(X)) 499.90/254.98 g(ok(X)) -> ok(g(X)) 499.90/254.98 weak: 499.90/254.98 top(mark(X)) -> top(proper(X)) 499.90/254.98 top(ok(X)) -> top(active(X)) 499.90/254.98 Matrix Interpretation Processor: dim=1 499.90/254.98 499.90/254.98 max_matrix: 499.90/254.98 1 499.90/254.98 interpretation: 499.90/254.98 [top](x0) = x0 + 1, 499.90/254.98 499.90/254.98 [ok](x0) = x0 + 2, 499.90/254.98 499.90/254.98 [proper](x0) = x0, 499.90/254.98 499.90/254.98 [mark](x0) = x0, 499.90/254.98 499.90/254.98 [g](x0) = x0, 499.90/254.98 499.90/254.98 [active](x0) = x0 + 2, 499.90/254.98 499.90/254.98 [f](x0) = x0 + 11, 499.90/254.98 499.90/254.98 [a] = 5 499.90/254.98 orientation: 499.90/254.98 active(f(f(a()))) = 29 >= 27 = mark(f(g(f(a())))) 499.90/254.98 499.90/254.98 active(f(X)) = X + 13 >= X + 13 = f(active(X)) 499.90/254.98 499.90/254.98 f(mark(X)) = X + 11 >= X + 11 = mark(f(X)) 499.90/254.98 499.90/254.98 proper(f(X)) = X + 11 >= X + 11 = f(proper(X)) 499.90/254.98 499.90/254.98 proper(a()) = 5 >= 7 = ok(a()) 499.90/254.98 499.90/254.98 proper(g(X)) = X >= X = g(proper(X)) 499.90/254.98 499.90/254.98 f(ok(X)) = X + 13 >= X + 13 = ok(f(X)) 499.90/254.98 499.90/254.98 g(ok(X)) = X + 2 >= X + 2 = ok(g(X)) 499.90/254.98 499.90/254.98 top(mark(X)) = X + 1 >= X + 1 = top(proper(X)) 499.90/254.98 499.90/254.98 top(ok(X)) = X + 3 >= X + 3 = top(active(X)) 499.90/254.98 problem: 499.90/254.98 strict: 499.90/254.98 active(f(X)) -> f(active(X)) 499.90/254.98 f(mark(X)) -> mark(f(X)) 499.90/254.98 proper(f(X)) -> f(proper(X)) 499.90/254.98 proper(a()) -> ok(a()) 499.90/254.98 proper(g(X)) -> g(proper(X)) 499.90/254.98 f(ok(X)) -> ok(f(X)) 499.90/254.98 g(ok(X)) -> ok(g(X)) 499.90/254.98 weak: 499.90/254.98 active(f(f(a()))) -> mark(f(g(f(a())))) 499.90/254.98 top(mark(X)) -> top(proper(X)) 499.90/254.98 top(ok(X)) -> top(active(X)) 499.90/254.98 Splitting Processor: 499.90/254.98 strict: 499.90/254.98 g(ok(X)) -> ok(g(X)) 499.90/254.98 weak: 499.90/254.98 active(f(f(a()))) -> mark(f(g(f(a())))) 499.90/254.98 top(mark(X)) -> top(proper(X)) 499.90/254.98 top(ok(X)) -> top(active(X)) 499.90/254.98 active(f(X)) -> f(active(X)) 499.90/254.98 f(mark(X)) -> mark(f(X)) 499.90/254.98 proper(f(X)) -> f(proper(X)) 499.90/254.98 proper(a()) -> ok(a()) 499.90/254.98 proper(g(X)) -> g(proper(X)) 499.90/254.98 f(ok(X)) -> ok(f(X)) 499.90/254.98 Splitting Processor: 499.90/254.98 strict: 499.90/254.98 proper(a()) -> ok(a()) 499.90/254.98 weak: 499.90/254.98 g(ok(X)) -> ok(g(X)) 499.90/254.98 active(f(f(a()))) -> mark(f(g(f(a())))) 499.90/254.98 top(mark(X)) -> top(proper(X)) 499.90/254.98 top(ok(X)) -> top(active(X)) 499.90/254.98 active(f(X)) -> f(active(X)) 499.90/254.98 f(mark(X)) -> mark(f(X)) 499.90/254.98 proper(f(X)) -> f(proper(X)) 499.90/254.98 proper(g(X)) -> g(proper(X)) 499.90/254.98 f(ok(X)) -> ok(f(X)) 499.90/254.98 Matrix Interpretation Processor: dim=3 499.90/254.98 499.90/254.98 max_matrix: 499.90/254.98 [1 1 0] 499.90/254.98 [0 1 0] 499.90/254.98 [0 0 0] 499.90/254.98 interpretation: 499.90/254.98 [1 1 0] [0] 499.90/254.98 [top](x0) = [0 0 0]x0 + [1] 499.90/254.98 [0 0 0] [0], 499.90/254.98 499.90/254.98 [1 0 0] 499.90/254.98 [ok](x0) = [0 1 0]x0 499.90/254.98 [0 0 0] , 499.90/254.98 499.90/254.98 [1 0 0] [1] 499.90/254.98 [proper](x0) = [0 1 0]x0 + [0] 499.90/254.98 [0 0 0] [0], 499.90/254.98 499.90/254.98 [1 0 0] [0] 499.90/254.98 [mark](x0) = [0 1 0]x0 + [1] 499.90/254.98 [0 0 0] [0], 499.90/254.98 499.90/254.98 [1 0 0] 499.90/254.98 [g](x0) = [0 0 0]x0 499.90/254.98 [0 0 0] , 499.90/254.98 499.90/254.98 [1 0 0] 499.90/254.98 [active](x0) = [0 1 0]x0 499.90/254.98 [0 0 0] , 499.90/254.98 499.90/254.98 [1 0 0] 499.90/254.98 [f](x0) = [0 1 0]x0 499.90/254.98 [0 0 0] , 499.90/254.98 499.90/254.98 [0] 499.90/254.98 [a] = [1] 499.90/254.98 [0] 499.90/254.98 orientation: 499.90/254.98 [1] [0] 499.90/254.98 proper(a()) = [1] >= [1] = ok(a()) 499.90/254.98 [0] [0] 499.90/254.98 499.90/254.98 [1 0 0] [1 0 0] 499.90/254.98 g(ok(X)) = [0 0 0]X >= [0 0 0]X = ok(g(X)) 499.90/254.98 [0 0 0] [0 0 0] 499.90/254.98 499.90/254.98 [0] [0] 499.90/254.98 active(f(f(a()))) = [1] >= [1] = mark(f(g(f(a())))) 499.90/254.98 [0] [0] 499.90/254.98 499.90/254.98 [1 1 0] [1] [1 1 0] [1] 499.90/254.98 top(mark(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = top(proper(X)) 499.90/254.98 [0 0 0] [0] [0 0 0] [0] 499.90/254.98 499.90/254.98 [1 1 0] [0] [1 1 0] [0] 499.90/254.98 top(ok(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = top(active(X)) 499.90/254.98 [0 0 0] [0] [0 0 0] [0] 499.90/254.98 499.90/254.98 [1 0 0] [1 0 0] 499.90/254.98 active(f(X)) = [0 1 0]X >= [0 1 0]X = f(active(X)) 499.90/254.98 [0 0 0] [0 0 0] 499.90/254.98 499.90/254.98 [1 0 0] [0] [1 0 0] [0] 499.90/254.98 f(mark(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = mark(f(X)) 499.90/254.98 [0 0 0] [0] [0 0 0] [0] 499.90/254.98 499.90/254.98 [1 0 0] [1] [1 0 0] [1] 499.90/254.98 proper(f(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = f(proper(X)) 499.90/254.98 [0 0 0] [0] [0 0 0] [0] 499.90/254.98 499.90/254.98 [1 0 0] [1] [1 0 0] [1] 499.90/254.98 proper(g(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = g(proper(X)) 499.90/254.98 [0 0 0] [0] [0 0 0] [0] 499.90/254.98 499.90/254.98 [1 0 0] [1 0 0] 499.90/254.98 f(ok(X)) = [0 1 0]X >= [0 1 0]X = ok(f(X)) 499.90/254.98 [0 0 0] [0 0 0] 499.90/254.98 problem: 499.90/254.98 strict: 499.90/254.98 499.90/254.98 weak: 499.90/254.98 proper(a()) -> ok(a()) 499.90/254.98 g(ok(X)) -> ok(g(X)) 499.90/254.98 active(f(f(a()))) -> mark(f(g(f(a())))) 499.90/254.98 top(mark(X)) -> top(proper(X)) 499.90/254.98 top(ok(X)) -> top(active(X)) 499.90/254.98 active(f(X)) -> f(active(X)) 499.90/254.98 f(mark(X)) -> mark(f(X)) 499.90/254.98 proper(f(X)) -> f(proper(X)) 499.90/254.98 proper(g(X)) -> g(proper(X)) 499.90/254.98 f(ok(X)) -> ok(f(X)) 499.90/254.98 Qed 499.90/254.98 499.90/254.98 strict: 499.90/254.98 active(f(X)) -> f(active(X)) 499.90/254.98 f(mark(X)) -> mark(f(X)) 499.90/254.98 proper(f(X)) -> f(proper(X)) 499.90/254.98 proper(g(X)) -> g(proper(X)) 499.90/254.98 f(ok(X)) -> ok(f(X)) 499.90/254.98 weak: 499.90/254.98 proper(a()) -> ok(a()) 499.90/254.98 g(ok(X)) -> ok(g(X)) 499.90/254.98 active(f(f(a()))) -> mark(f(g(f(a())))) 499.90/254.98 top(mark(X)) -> top(proper(X)) 499.90/254.98 top(ok(X)) -> top(active(X)) 499.90/254.98 Matrix Interpretation Processor: dim=4 499.90/254.98 499.90/254.98 max_matrix: 499.90/254.98 [1 1 0 1] 499.90/254.98 [0 1 1 1] 499.90/254.98 [0 0 0 0] 499.90/254.98 [0 0 0 0] 499.90/254.98 interpretation: 499.90/254.98 [1 0 0 0] [0] 499.90/254.98 [0 0 1 1] [0] 499.90/254.98 [top](x0) = [0 0 0 0]x0 + [1] 499.90/254.98 [0 0 0 0] [1], 499.90/254.98 499.90/254.98 [1 0 0 0] 499.90/254.98 [0 1 0 0] 499.90/254.98 [ok](x0) = [0 0 0 0]x0 499.90/254.98 [0 0 0 0] , 499.90/254.98 499.90/254.98 [1 0 0 0] 499.90/254.98 [0 1 0 0] 499.90/254.98 [proper](x0) = [0 0 0 0]x0 499.90/254.98 [0 0 0 0] , 499.90/254.99 499.90/254.99 [1 0 0 1] [0] 499.90/254.99 [0 1 0 1] [1] 499.90/254.99 [mark](x0) = [0 0 0 0]x0 + [0] 499.90/254.99 [0 0 0 0] [0], 499.90/254.99 499.90/254.99 [1 1 0 0] 499.90/254.99 [0 0 0 0] 499.90/254.99 [g](x0) = [0 0 0 0]x0 499.90/254.99 [0 0 0 0] , 499.90/254.99 499.90/254.99 [1 0 0 0] 499.90/254.99 [0 1 0 0] 499.90/254.99 [active](x0) = [0 0 0 0]x0 499.90/254.99 [0 0 0 0] , 499.90/254.99 499.90/254.99 [1 1 0 0] 499.90/254.99 [0 1 0 0] 499.90/254.99 [f](x0) = [0 0 0 0]x0 499.90/254.99 [0 0 0 0] , 499.90/254.99 499.90/254.99 [0] 499.90/254.99 [1] 499.90/254.99 [a] = [0] 499.90/254.99 [0] 499.90/254.99 orientation: 499.90/254.99 [1 1 0 0] [1 1 0 0] 499.90/254.99 [0 1 0 0] [0 1 0 0] 499.90/254.99 active(f(X)) = [0 0 0 0]X >= [0 0 0 0]X = f(active(X)) 499.90/254.99 [0 0 0 0] [0 0 0 0] 499.90/254.99 499.90/254.99 [1 1 0 2] [1] [1 1 0 0] [0] 499.90/254.99 [0 1 0 1] [1] [0 1 0 0] [1] 499.90/254.99 f(mark(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = mark(f(X)) 499.90/254.99 [0 0 0 0] [0] [0 0 0 0] [0] 499.90/254.99 499.90/254.99 [1 1 0 0] [1 1 0 0] 499.90/254.99 [0 1 0 0] [0 1 0 0] 499.90/254.99 proper(f(X)) = [0 0 0 0]X >= [0 0 0 0]X = f(proper(X)) 499.90/254.99 [0 0 0 0] [0 0 0 0] 499.90/254.99 499.90/254.99 [1 1 0 0] [1 1 0 0] 499.90/254.99 [0 0 0 0] [0 0 0 0] 499.90/254.99 proper(g(X)) = [0 0 0 0]X >= [0 0 0 0]X = g(proper(X)) 499.90/254.99 [0 0 0 0] [0 0 0 0] 499.90/254.99 499.90/254.99 [1 1 0 0] [1 1 0 0] 499.90/254.99 [0 1 0 0] [0 1 0 0] 499.90/254.99 f(ok(X)) = [0 0 0 0]X >= [0 0 0 0]X = ok(f(X)) 499.90/254.99 [0 0 0 0] [0 0 0 0] 499.90/254.99 499.90/254.99 [0] [0] 499.90/254.99 [1] [1] 499.90/254.99 proper(a()) = [0] >= [0] = ok(a()) 499.90/254.99 [0] [0] 499.90/254.99 499.90/254.99 [1 1 0 0] [1 1 0 0] 499.90/254.99 [0 0 0 0] [0 0 0 0] 499.90/254.99 g(ok(X)) = [0 0 0 0]X >= [0 0 0 0]X = ok(g(X)) 499.90/254.99 [0 0 0 0] [0 0 0 0] 499.90/254.99 499.90/254.99 [2] [2] 499.90/254.99 [1] [1] 499.90/254.99 active(f(f(a()))) = [0] >= [0] = mark(f(g(f(a())))) 499.90/254.99 [0] [0] 499.90/254.99 499.90/254.99 [1 0 0 1] [0] [1 0 0 0] [0] 499.90/254.99 [0 0 0 0] [0] [0 0 0 0] [0] 499.90/254.99 top(mark(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(proper(X)) 499.90/254.99 [0 0 0 0] [1] [0 0 0 0] [1] 499.90/254.99 499.90/254.99 [1 0 0 0] [0] [1 0 0 0] [0] 499.90/254.99 [0 0 0 0] [0] [0 0 0 0] [0] 499.90/254.99 top(ok(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(active(X)) 499.90/254.99 [0 0 0 0] [1] [0 0 0 0] [1] 499.90/254.99 problem: 499.90/254.99 strict: 499.90/254.99 active(f(X)) -> f(active(X)) 499.90/254.99 proper(f(X)) -> f(proper(X)) 499.90/254.99 proper(g(X)) -> g(proper(X)) 499.90/254.99 f(ok(X)) -> ok(f(X)) 499.90/254.99 weak: 499.90/254.99 f(mark(X)) -> mark(f(X)) 499.90/254.99 proper(a()) -> ok(a()) 499.90/254.99 g(ok(X)) -> ok(g(X)) 499.90/254.99 active(f(f(a()))) -> mark(f(g(f(a())))) 499.90/254.99 top(mark(X)) -> top(proper(X)) 499.90/254.99 top(ok(X)) -> top(active(X)) 499.90/254.99 Splitting Processor: 499.90/254.99 strict: 499.90/254.99 f(ok(X)) -> ok(f(X)) 499.90/254.99 weak: 499.90/254.99 f(mark(X)) -> mark(f(X)) 499.90/254.99 proper(a()) -> ok(a()) 499.90/254.99 g(ok(X)) -> ok(g(X)) 499.90/254.99 active(f(f(a()))) -> mark(f(g(f(a())))) 499.90/254.99 top(mark(X)) -> top(proper(X)) 499.90/254.99 top(ok(X)) -> top(active(X)) 499.90/254.99 active(f(X)) -> f(active(X)) 499.90/254.99 proper(f(X)) -> f(proper(X)) 499.90/254.99 proper(g(X)) -> g(proper(X)) 500.00/255.00 Splitting Processor: 500.00/255.00 strict: 500.00/255.00 proper(g(X)) -> g(proper(X)) 500.00/255.00 weak: 500.00/255.00 f(ok(X)) -> ok(f(X)) 500.00/255.00 f(mark(X)) -> mark(f(X)) 500.00/255.00 proper(a()) -> ok(a()) 500.00/255.00 g(ok(X)) -> ok(g(X)) 500.00/255.00 active(f(f(a()))) -> mark(f(g(f(a())))) 500.00/255.00 top(mark(X)) -> top(proper(X)) 500.00/255.00 top(ok(X)) -> top(active(X)) 500.00/255.00 active(f(X)) -> f(active(X)) 500.00/255.00 proper(f(X)) -> f(proper(X)) 500.00/255.00 Matrix Interpretation Processor: dim=4 500.00/255.00 500.00/255.00 max_matrix: 500.00/255.00 [1 1 1 1] 500.00/255.00 [0 0 1 1] 500.00/255.00 [0 0 1 1] 500.00/255.00 [0 0 0 1] 500.00/255.00 interpretation: 500.00/255.00 [1 1 0 0] [0] 500.00/255.00 [0 0 0 0] [1] 500.00/255.00 [top](x0) = [0 0 1 0]x0 + [1] 500.00/255.00 [0 0 0 0] [1], 500.00/255.00 500.00/255.00 [1 0 1 0] 500.00/255.00 [0 0 1 0] 500.00/255.00 [ok](x0) = [0 0 1 0]x0 500.00/255.00 [0 0 0 0] , 500.00/255.00 500.00/255.00 [1 0 0 1] [1] 500.00/255.00 [0 0 1 0] [0] 500.00/255.00 [proper](x0) = [0 0 1 0]x0 + [0] 500.00/255.00 [0 0 0 1] [0], 500.00/255.00 500.00/255.00 [1 0 0 0] [1] 500.00/255.00 [0 0 1 1] [0] 500.00/255.00 [mark](x0) = [0 0 1 1]x0 + [0] 500.00/255.00 [0 0 0 0] [0], 500.00/255.00 500.00/255.00 [1 0 0 0] [0] 500.00/255.00 [0 0 0 0] [0] 500.00/255.00 [g](x0) = [0 0 0 0]x0 + [0] 500.00/255.00 [0 0 0 1] [1], 500.00/255.00 500.00/255.00 [1 0 1 0] 500.00/255.00 [0 0 1 0] 500.00/255.00 [active](x0) = [0 0 1 0]x0 500.00/255.00 [0 0 0 0] , 500.00/255.00 500.00/255.00 [1 0 0 0] 500.00/255.00 [0 0 1 0] 500.00/255.00 [f](x0) = [0 0 1 0]x0 500.00/255.00 [0 0 0 1] , 500.00/255.00 500.00/255.00 [1] 500.00/255.00 [0] 500.00/255.00 [a] = [1] 500.00/255.00 [0] 500.00/255.00 orientation: 500.00/255.00 [1 0 0 1] [2] [1 0 0 1] [1] 500.00/255.00 [0 0 0 0] [0] [0 0 0 0] [0] 500.00/255.00 proper(g(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = g(proper(X)) 500.00/255.00 [0 0 0 1] [1] [0 0 0 1] [1] 500.00/255.00 500.00/255.00 [1 0 1 0] [1 0 1 0] 500.00/255.00 [0 0 1 0] [0 0 1 0] 500.00/255.00 f(ok(X)) = [0 0 1 0]X >= [0 0 1 0]X = ok(f(X)) 500.00/255.00 [0 0 0 0] [0 0 0 0] 500.00/255.00 500.00/255.00 [1 0 0 0] [1] [1 0 0 0] [1] 500.00/255.00 [0 0 1 1] [0] [0 0 1 1] [0] 500.00/255.00 f(mark(X)) = [0 0 1 1]X + [0] >= [0 0 1 1]X + [0] = mark(f(X)) 500.00/255.00 [0 0 0 0] [0] [0 0 0 0] [0] 500.00/255.00 500.00/255.00 [2] [2] 500.00/255.00 [1] [1] 500.00/255.00 proper(a()) = [1] >= [1] = ok(a()) 500.00/255.00 [0] [0] 500.00/255.00 500.00/255.00 [1 0 1 0] [0] [1 0 0 0] 500.00/255.00 [0 0 0 0] [0] [0 0 0 0] 500.00/255.00 g(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X = ok(g(X)) 500.00/255.00 [0 0 0 0] [1] [0 0 0 0] 500.00/255.00 500.00/255.00 [2] [2] 500.00/255.00 [1] [1] 500.00/255.00 active(f(f(a()))) = [1] >= [1] = mark(f(g(f(a())))) 500.00/255.00 [0] [0] 500.00/255.00 500.00/255.00 [1 0 1 1] [1] [1 0 1 1] [1] 500.00/255.00 [0 0 0 0] [1] [0 0 0 0] [1] 500.00/255.00 top(mark(X)) = [0 0 1 1]X + [1] >= [0 0 1 0]X + [1] = top(proper(X)) 500.00/255.00 [0 0 0 0] [1] [0 0 0 0] [1] 500.00/255.00 500.00/255.00 [1 0 2 0] [0] [1 0 2 0] [0] 500.00/255.00 [0 0 0 0] [1] [0 0 0 0] [1] 500.00/255.00 top(ok(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = top(active(X)) 500.00/255.00 [0 0 0 0] [1] [0 0 0 0] [1] 500.00/255.00 500.00/255.00 [1 0 1 0] [1 0 1 0] 500.00/255.00 [0 0 1 0] [0 0 1 0] 500.00/255.00 active(f(X)) = [0 0 1 0]X >= [0 0 1 0]X = f(active(X)) 500.00/255.00 [0 0 0 0] [0 0 0 0] 500.00/255.00 500.00/255.00 [1 0 0 1] [1] [1 0 0 1] [1] 500.00/255.00 [0 0 1 0] [0] [0 0 1 0] [0] 500.00/255.00 proper(f(X)) = [0 0 1 0]X + [0] >= [0 0 1 0]X + [0] = f(proper(X)) 500.00/255.00 [0 0 0 1] [0] [0 0 0 1] [0] 500.00/255.00 problem: 500.00/255.00 strict: 500.00/255.00 500.00/255.00 weak: 500.00/255.00 proper(g(X)) -> g(proper(X)) 500.00/255.00 f(ok(X)) -> ok(f(X)) 500.00/255.00 f(mark(X)) -> mark(f(X)) 500.00/255.00 proper(a()) -> ok(a()) 500.00/255.00 g(ok(X)) -> ok(g(X)) 500.00/255.00 active(f(f(a()))) -> mark(f(g(f(a())))) 500.00/255.00 top(mark(X)) -> top(proper(X)) 500.00/255.00 top(ok(X)) -> top(active(X)) 500.00/255.00 active(f(X)) -> f(active(X)) 500.00/255.00 proper(f(X)) -> f(proper(X)) 500.00/255.00 Qed 500.00/255.00 500.00/255.00 strict: 500.00/255.00 active(f(X)) -> f(active(X)) 500.00/255.00 proper(f(X)) -> f(proper(X)) 500.00/255.00 weak: 500.00/255.00 proper(g(X)) -> g(proper(X)) 500.00/255.00 f(ok(X)) -> ok(f(X)) 500.00/255.00 f(mark(X)) -> mark(f(X)) 500.00/255.00 proper(a()) -> ok(a()) 500.00/255.00 g(ok(X)) -> ok(g(X)) 500.00/255.00 active(f(f(a()))) -> mark(f(g(f(a())))) 500.00/255.00 top(mark(X)) -> top(proper(X)) 500.00/255.00 top(ok(X)) -> top(active(X)) 500.00/255.00 Splitting Processor: 500.00/255.00 strict: 500.00/255.00 proper(f(X)) -> f(proper(X)) 500.00/255.00 weak: 500.00/255.00 proper(g(X)) -> g(proper(X)) 500.00/255.00 f(ok(X)) -> ok(f(X)) 500.00/255.00 f(mark(X)) -> mark(f(X)) 500.00/255.00 proper(a()) -> ok(a()) 500.00/255.00 g(ok(X)) -> ok(g(X)) 500.00/255.00 active(f(f(a()))) -> mark(f(g(f(a())))) 500.00/255.00 top(mark(X)) -> top(proper(X)) 500.00/255.00 top(ok(X)) -> top(active(X)) 500.00/255.00 active(f(X)) -> f(active(X)) 500.00/255.00 Matrix Interpretation Processor: dim=3 500.00/255.00 500.00/255.00 max_matrix: 500.00/255.00 [1 1 1] 500.00/255.00 [0 1 1] 500.00/255.00 [0 0 1] 500.00/255.00 interpretation: 500.00/255.00 [1 0 0] [0] 500.00/255.00 [top](x0) = [0 0 0]x0 + [0] 500.00/255.00 [0 0 0] [1], 500.00/255.00 500.00/255.00 [1 0 1] [0] 500.00/255.00 [ok](x0) = [0 1 0]x0 + [1] 500.00/255.00 [0 0 1] [1], 500.00/255.00 500.00/255.00 [1 0 1] [0] 500.00/255.00 [proper](x0) = [0 1 0]x0 + [1] 500.00/255.00 [0 0 1] [1], 500.00/255.00 500.00/255.00 [1 0 1] [0] 500.00/255.00 [mark](x0) = [0 1 0]x0 + [1] 500.00/255.00 [0 0 0] [0], 500.00/255.00 500.00/255.00 [1 0 0] [1] 500.00/255.00 [g](x0) = [0 0 1]x0 + [0] 500.00/255.00 [0 0 1] [0], 500.00/255.00 500.00/255.00 [1 0 1] [0] 500.00/255.00 [active](x0) = [0 1 0]x0 + [0] 500.00/255.00 [0 0 1] [3], 500.00/255.00 500.00/255.00 [1 1 0] [0] 500.00/255.00 [f](x0) = [0 1 0]x0 + [0] 500.00/255.00 [0 0 1] [1], 500.00/255.00 500.00/255.00 [0] 500.00/255.00 [a] = [2] 500.00/255.00 [0] 500.00/255.00 orientation: 500.00/255.00 [1 1 1] [1] [1 1 1] [0] 500.00/255.00 active(f(X)) = [0 1 0]X + [0] >= [0 1 0]X + [0] = f(active(X)) 500.00/255.00 [0 0 1] [4] [0 0 1] [4] 500.00/255.00 500.00/255.00 [1 1 1] [1] [1 1 1] [1] 500.00/255.00 proper(f(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = f(proper(X)) 500.00/255.00 [0 0 1] [2] [0 0 1] [2] 500.00/255.00 500.00/255.00 [1 0 1] [1] [1 0 1] [1] 500.00/255.00 proper(g(X)) = [0 0 1]X + [1] >= [0 0 1]X + [1] = g(proper(X)) 500.00/255.00 [0 0 1] [1] [0 0 1] [1] 500.00/255.00 500.00/255.00 [1 1 1] [1] [1 1 1] [1] 500.00/255.00 f(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(f(X)) 500.00/255.00 [0 0 1] [2] [0 0 1] [2] 500.00/255.01 500.00/255.01 [1 1 1] [1] [1 1 1] [1] 500.00/255.01 f(mark(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = mark(f(X)) 500.00/255.01 [0 0 0] [1] [0 0 0] [0] 500.00/255.01 500.00/255.01 [0] [0] 500.00/255.01 proper(a()) = [3] >= [3] = ok(a()) 500.00/255.01 [1] [1] 500.00/255.01 500.00/255.01 [1 0 1] [1] [1 0 1] [1] 500.00/255.01 g(ok(X)) = [0 0 1]X + [1] >= [0 0 1]X + [1] = ok(g(X)) 500.00/255.01 [0 0 1] [1] [0 0 1] [1] 500.00/255.01 500.00/255.01 [6] [6] 500.00/255.01 active(f(f(a()))) = [2] >= [2] = mark(f(g(f(a())))) 500.00/255.01 [5] [0] 500.00/255.01 500.00/255.01 [1 0 1] [0] [1 0 1] [0] 500.00/255.01 top(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = top(proper(X)) 500.00/255.01 [0 0 0] [1] [0 0 0] [1] 500.00/255.01 500.00/255.01 [1 0 1] [0] [1 0 1] [0] 500.00/255.01 top(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = top(active(X)) 500.00/255.01 [0 0 0] [1] [0 0 0] [1] 500.00/255.01 problem: 500.00/255.01 strict: 500.00/255.01 500.00/255.01 weak: 500.00/255.01 active(f(X)) -> f(active(X)) 500.00/255.01 proper(f(X)) -> f(proper(X)) 500.00/255.01 proper(g(X)) -> g(proper(X)) 500.00/255.01 f(ok(X)) -> ok(f(X)) 500.00/255.01 f(mark(X)) -> mark(f(X)) 500.00/255.01 proper(a()) -> ok(a()) 500.00/255.01 g(ok(X)) -> ok(g(X)) 500.00/255.01 active(f(f(a()))) -> mark(f(g(f(a())))) 500.00/255.01 top(mark(X)) -> top(proper(X)) 500.00/255.01 top(ok(X)) -> top(active(X)) 500.00/255.01 Qed 500.00/255.01 500.00/255.01 strict: 500.00/255.01 active(f(X)) -> f(active(X)) 500.00/255.01 weak: 500.00/255.01 proper(f(X)) -> f(proper(X)) 500.00/255.01 proper(g(X)) -> g(proper(X)) 500.00/255.01 f(ok(X)) -> ok(f(X)) 500.00/255.01 f(mark(X)) -> mark(f(X)) 500.00/255.01 proper(a()) -> ok(a()) 500.00/255.01 g(ok(X)) -> ok(g(X)) 500.00/255.01 active(f(f(a()))) -> mark(f(g(f(a())))) 500.00/255.01 top(mark(X)) -> top(proper(X)) 500.00/255.01 top(ok(X)) -> top(active(X)) 500.00/255.01 Matrix Interpretation Processor: dim=4 500.00/255.01 500.00/255.01 max_matrix: 500.00/255.01 [1 1 1 1] 500.00/255.01 [0 1 0 1] 500.00/255.01 [0 0 0 0] 500.00/255.01 [0 0 0 1] 500.00/255.01 interpretation: 500.00/255.01 [1 0 0 1] [0] 500.00/255.01 [0 0 0 1] [0] 500.00/255.01 [top](x0) = [0 0 0 0]x0 + [1] 500.00/255.01 [0 0 0 0] [0], 500.00/255.01 500.00/255.01 [1 0 1 0] [1] 500.00/255.01 [0 0 0 0] [0] 500.00/255.01 [ok](x0) = [0 0 0 0]x0 + [0] 500.00/255.01 [0 0 0 1] [0], 500.00/255.01 500.00/255.01 [1 1 0 0] [1] 500.00/255.01 [0 1 0 0] [0] 500.00/255.01 [proper](x0) = [0 0 0 0]x0 + [0] 500.00/255.01 [0 0 0 1] [0], 500.00/255.01 500.00/255.01 [1 1 0 0] [0] 500.00/255.01 [0 0 0 0] [0] 500.00/255.01 [mark](x0) = [0 0 0 0]x0 + [0] 500.00/255.01 [0 0 0 1] [1], 500.00/255.01 500.00/255.01 [1 0 0 0] 500.00/255.01 [0 1 0 0] 500.00/255.01 [g](x0) = [0 0 0 0]x0 500.00/255.01 [0 0 0 0] , 500.00/255.01 500.00/255.01 [1 0 0 0] [1] 500.00/255.01 [0 1 0 1] [0] 500.00/255.01 [active](x0) = [0 0 0 0]x0 + [1] 500.00/255.01 [0 0 0 1] [0], 500.00/255.01 500.00/255.01 [1 0 0 1] [0] 500.00/255.01 [0 1 0 0] [1] 500.00/255.01 [f](x0) = [0 0 0 0]x0 + [0] 500.00/255.01 [0 0 0 1] [0], 500.00/255.01 500.00/255.01 [0] 500.00/255.01 [0] 500.00/255.01 [a] = [0] 500.00/255.01 [1] 500.00/255.01 orientation: 500.00/255.01 [1 1 0 1] [2] [1 1 0 1] [1] 500.00/255.01 [0 1 0 0] [1] [0 1 0 0] [1] 500.00/255.01 proper(f(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = f(proper(X)) 500.00/255.01 [0 0 0 1] [0] [0 0 0 1] [0] 500.00/255.01 500.00/255.01 [1 1 0 0] [1] [1 1 0 0] [1] 500.00/255.01 [0 1 0 0] [0] [0 1 0 0] [0] 500.00/255.01 proper(g(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = g(proper(X)) 500.00/255.01 [0 0 0 0] [0] [0 0 0 0] [0] 500.00/255.01 500.00/255.01 [1 0 1 1] [1] [1 0 0 1] [1] 500.00/255.01 [0 0 0 0] [1] [0 0 0 0] [0] 500.00/255.01 f(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = ok(f(X)) 500.00/255.01 [0 0 0 1] [0] [0 0 0 1] [0] 500.00/255.01 500.00/255.01 [1 1 0 1] [1] [1 1 0 1] [1] 500.00/255.01 [0 0 0 0] [1] [0 0 0 0] [0] 500.00/255.01 f(mark(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = mark(f(X)) 500.00/255.01 [0 0 0 1] [1] [0 0 0 1] [1] 500.00/255.01 500.00/255.01 [1] [1] 500.00/255.01 [0] [0] 500.00/255.01 proper(a()) = [0] >= [0] = ok(a()) 500.00/255.01 [1] [1] 500.00/255.01 500.00/255.01 [1 0 1 0] [1] [1 0 0 0] [1] 500.00/255.01 [0 0 0 0] [0] [0 0 0 0] [0] 500.00/255.01 g(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = ok(g(X)) 500.00/255.01 [0 0 0 0] [0] [0 0 0 0] [0] 500.00/255.01 500.00/255.01 [3] [3] 500.00/255.01 [3] [0] 500.00/255.01 active(f(f(a()))) = [1] >= [0] = mark(f(g(f(a())))) 500.00/255.01 [1] [1] 500.00/255.01 500.00/255.01 [1 1 0 1] [1] [1 1 0 1] [1] 500.00/255.01 [0 0 0 1] [1] [0 0 0 1] [0] 500.00/255.01 top(mark(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(proper(X)) 500.00/255.01 [0 0 0 0] [0] [0 0 0 0] [0] 500.00/255.01 500.00/255.01 [1 0 1 1] [1] [1 0 0 1] [1] 500.00/255.01 [0 0 0 1] [0] [0 0 0 1] [0] 500.00/255.01 top(ok(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(active(X)) 500.00/255.01 [0 0 0 0] [0] [0 0 0 0] [0] 500.00/255.01 500.00/255.01 [1 0 0 1] [1] [1 0 0 1] [1] 500.00/255.01 [0 1 0 1] [1] [0 1 0 1] [1] 500.00/255.01 active(f(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [0] = f(active(X)) 500.00/255.01 [0 0 0 1] [0] [0 0 0 1] [0] 500.00/255.01 problem: 500.00/255.01 strict: 500.00/255.01 500.00/255.01 weak: 500.00/255.01 proper(f(X)) -> f(proper(X)) 500.00/255.01 proper(g(X)) -> g(proper(X)) 500.00/255.01 f(ok(X)) -> ok(f(X)) 500.00/255.01 f(mark(X)) -> mark(f(X)) 500.00/255.01 proper(a()) -> ok(a()) 500.00/255.01 g(ok(X)) -> ok(g(X)) 500.00/255.01 active(f(f(a()))) -> mark(f(g(f(a())))) 500.00/255.01 top(mark(X)) -> top(proper(X)) 500.00/255.01 top(ok(X)) -> top(active(X)) 500.00/255.01 active(f(X)) -> f(active(X)) 500.00/255.01 Qed 500.00/255.01 500.00/255.01 strict: 500.00/255.01 active(f(X)) -> f(active(X)) 500.00/255.01 proper(f(X)) -> f(proper(X)) 500.00/255.01 proper(g(X)) -> g(proper(X)) 500.00/255.01 weak: 500.00/255.01 f(ok(X)) -> ok(f(X)) 500.00/255.01 f(mark(X)) -> mark(f(X)) 500.00/255.01 proper(a()) -> ok(a()) 500.00/255.01 g(ok(X)) -> ok(g(X)) 500.00/255.01 active(f(f(a()))) -> mark(f(g(f(a())))) 500.00/255.01 top(mark(X)) -> top(proper(X)) 500.00/255.01 top(ok(X)) -> top(active(X)) 500.00/255.01 Matrix Interpretation Processor: dim=4 500.00/255.01 500.00/255.01 max_matrix: 500.00/255.01 [1 1 0 1] 500.00/255.01 [0 1 0 0] 500.00/255.01 [0 0 0 0] 500.00/255.01 [0 0 0 1] 500.00/255.01 interpretation: 500.00/255.01 [1 0 0 1] [0] 500.00/255.01 [0 0 0 0] [1] 500.00/255.01 [top](x0) = [0 0 0 0]x0 + [1] 500.00/255.01 [0 0 0 1] [0], 500.00/255.01 500.00/255.01 [1 0 0 0] [1] 500.00/255.01 [0 1 0 0] [1] 500.00/255.01 [ok](x0) = [0 0 0 0]x0 + [0] 500.00/255.02 [0 0 0 1] [0], 500.00/255.02 500.00/255.02 [1 1 0 0] [1] 500.00/255.02 [0 1 0 0] [1] 500.00/255.02 [proper](x0) = [0 0 0 0]x0 + [0] 500.00/255.02 [0 0 0 1] [0], 500.00/255.02 500.00/255.02 [1 1 0 0] [0] 500.00/255.02 [0 1 0 0] [0] 500.00/255.02 [mark](x0) = [0 0 0 0]x0 + [0] 500.00/255.02 [0 0 0 1] [1], 500.00/255.02 500.00/255.02 [1 0 0 0] 500.00/255.02 [0 1 0 0] 500.00/255.02 [g](x0) = [0 0 0 0]x0 500.00/255.02 [0 0 0 0] , 500.00/255.02 500.00/255.02 [1 0 0 0] [1] 500.00/255.02 [0 1 0 0] [0] 500.00/255.02 [active](x0) = [0 0 0 0]x0 + [0] 500.00/255.02 [0 0 0 1] [0], 500.00/255.02 500.00/255.02 [1 1 0 1] [0] 500.00/255.02 [0 1 0 0] [1] 500.00/255.02 [f](x0) = [0 0 0 0]x0 + [0] 500.00/255.02 [0 0 0 1] [1], 500.00/255.02 500.00/255.02 [0] 500.00/255.02 [0] 500.00/255.02 [a] = [0] 500.00/255.02 [0] 500.00/255.02 orientation: 500.00/255.02 [1 1 0 1] [2] [1 1 0 1] [1] 500.00/255.02 [0 1 0 0] [2] [0 1 0 0] [2] 500.00/255.02 f(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = ok(f(X)) 500.00/255.02 [0 0 0 1] [1] [0 0 0 1] [1] 500.00/255.02 500.00/255.02 [1 2 0 1] [1] [1 2 0 1] [1] 500.00/255.02 [0 1 0 0] [1] [0 1 0 0] [1] 500.00/255.02 f(mark(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = mark(f(X)) 500.00/255.02 [0 0 0 1] [2] [0 0 0 1] [2] 500.00/255.02 500.00/255.02 [1] [1] 500.00/255.02 [1] [1] 500.00/255.02 proper(a()) = [0] >= [0] = ok(a()) 500.00/255.02 [0] [0] 500.00/255.02 500.00/255.02 [1 0 0 0] [1] [1 0 0 0] [1] 500.00/255.02 [0 1 0 0] [1] [0 1 0 0] [1] 500.00/255.02 g(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = ok(g(X)) 500.00/255.02 [0 0 0 0] [0] [0 0 0 0] [0] 500.00/255.02 500.00/255.02 [3] [3] 500.00/255.02 [2] [2] 500.00/255.02 active(f(f(a()))) = [0] >= [0] = mark(f(g(f(a())))) 500.00/255.02 [2] [2] 500.00/255.02 500.00/255.02 [1 1 0 1] [1] [1 1 0 1] [1] 500.00/255.02 [0 0 0 0] [1] [0 0 0 0] [1] 500.00/255.02 top(mark(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(proper(X)) 500.00/255.02 [0 0 0 1] [1] [0 0 0 1] [0] 500.00/255.02 500.00/255.02 [1 0 0 1] [1] [1 0 0 1] [1] 500.00/255.02 [0 0 0 0] [1] [0 0 0 0] [1] 500.00/255.02 top(ok(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(active(X)) 500.00/255.02 [0 0 0 1] [0] [0 0 0 1] [0] 500.00/255.02 500.00/255.02 [1 1 0 1] [1] [1 1 0 1] [1] 500.00/255.02 [0 1 0 0] [1] [0 1 0 0] [1] 500.00/255.02 active(f(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = f(active(X)) 500.00/255.02 [0 0 0 1] [1] [0 0 0 1] [1] 500.00/255.02 500.00/255.02 [1 2 0 1] [2] [1 2 0 1] [2] 500.00/255.02 [0 1 0 0] [2] [0 1 0 0] [2] 500.00/255.02 proper(f(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = f(proper(X)) 500.00/255.02 [0 0 0 1] [1] [0 0 0 1] [1] 500.00/255.02 500.00/255.02 [1 1 0 0] [1] [1 1 0 0] [1] 500.00/255.02 [0 1 0 0] [1] [0 1 0 0] [1] 500.00/255.02 proper(g(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = g(proper(X)) 500.00/255.02 [0 0 0 0] [0] [0 0 0 0] [0] 500.00/255.02 problem: 500.00/255.02 strict: 500.00/255.02 500.00/255.02 weak: 500.00/255.02 f(ok(X)) -> ok(f(X)) 500.00/255.02 f(mark(X)) -> mark(f(X)) 500.00/255.02 proper(a()) -> ok(a()) 500.00/255.03 g(ok(X)) -> ok(g(X)) 500.00/255.03 active(f(f(a()))) -> mark(f(g(f(a())))) 500.00/255.03 top(mark(X)) -> top(proper(X)) 500.00/255.03 top(ok(X)) -> top(active(X)) 500.00/255.03 active(f(X)) -> f(active(X)) 500.00/255.03 proper(f(X)) -> f(proper(X)) 500.00/255.03 proper(g(X)) -> g(proper(X)) 500.00/255.03 Qed 500.00/255.03 500.00/255.03 strict: 500.00/255.03 active(f(X)) -> f(active(X)) 500.00/255.03 f(mark(X)) -> mark(f(X)) 500.00/255.03 proper(f(X)) -> f(proper(X)) 500.00/255.03 proper(a()) -> ok(a()) 500.00/255.03 proper(g(X)) -> g(proper(X)) 500.00/255.03 f(ok(X)) -> ok(f(X)) 500.00/255.03 weak: 500.00/255.03 g(ok(X)) -> ok(g(X)) 500.00/255.03 active(f(f(a()))) -> mark(f(g(f(a())))) 500.00/255.03 top(mark(X)) -> top(proper(X)) 500.00/255.03 top(ok(X)) -> top(active(X)) 500.00/255.03 Matrix Interpretation Processor: dim=5 500.00/255.03 500.00/255.03 max_matrix: 500.00/255.03 [1 1 1 1 1] 500.00/255.03 [0 0 1 0 0] 500.00/255.03 [0 0 0 0 1] 500.00/255.03 [0 0 0 1 0] 500.00/255.03 [0 0 0 0 0] 500.00/255.03 interpretation: 500.00/255.03 [1 0 0 0 0] [0] 500.00/255.03 [0 0 0 0 0] [1] 500.00/255.03 [top](x0) = [0 0 0 0 0]x0 + [0] 500.00/255.03 [0 0 0 0 0] [1] 500.00/255.03 [0 0 0 0 0] [0], 500.00/255.03 500.00/255.03 [1 1 1 0 1] [0] 500.00/255.03 [0 0 1 0 0] [0] 500.00/255.03 [ok](x0) = [0 0 0 0 1]x0 + [0] 500.00/255.03 [0 0 0 1 0] [1] 500.00/255.03 [0 0 0 0 0] [0], 500.00/255.03 500.00/255.03 [1 0 0 1 0] [1] 500.00/255.03 [0 0 1 0 0] [0] 500.00/255.03 [proper](x0) = [0 0 0 0 1]x0 + [0] 500.00/255.03 [0 0 0 1 0] [1] 500.00/255.03 [0 0 0 0 0] [0], 500.00/255.03 500.00/255.03 [1 1 1 1 1] [1] 500.00/255.03 [0 0 1 0 0] [0] 500.00/255.03 [mark](x0) = [0 0 0 0 1]x0 + [0] 500.00/255.03 [0 0 0 0 0] [0] 500.00/255.03 [0 0 0 0 0] [0], 500.00/255.03 500.00/255.03 [1 0 0 1 0] [0] 500.00/255.03 [0 0 0 0 0] [0] 500.00/255.03 [g](x0) = [0 0 0 0 0]x0 + [0] 500.00/255.03 [0 0 0 1 0] [1] 500.00/255.03 [0 0 0 0 0] [0], 500.00/255.03 500.00/255.03 [1 1 0 0 0] 500.00/255.03 [0 0 1 0 0] 500.00/255.03 [active](x0) = [0 0 0 0 1]x0 500.00/255.03 [0 0 0 1 0] 500.00/255.03 [0 0 0 0 0] , 500.00/255.03 500.00/255.03 [1 1 1 0 1] 500.00/255.03 [0 0 1 0 0] 500.00/255.03 [f](x0) = [0 0 0 0 1]x0 500.00/255.03 [0 0 0 1 0] 500.00/255.03 [0 0 0 0 0] , 500.00/255.03 500.00/255.03 [0] 500.00/255.03 [0] 500.00/255.03 [a] = [0] 500.00/255.03 [0] 500.00/255.03 [1] 500.00/255.03 orientation: 500.00/255.03 [1 1 1 1 1] [1] [1 0 0 1 0] [0] 500.00/255.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 500.00/255.03 g(ok(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = ok(g(X)) 500.00/255.03 [0 0 0 1 0] [2] [0 0 0 1 0] [2] 500.00/255.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 500.00/255.03 500.00/255.03 [3] [3] 500.00/255.03 [0] [0] 500.00/255.03 active(f(f(a()))) = [0] >= [0] = mark(f(g(f(a())))) 500.00/255.03 [0] [0] 500.00/255.03 [0] [0] 500.00/255.03 500.00/255.03 [1 1 1 1 1] [1] [1 0 0 1 0] [1] 500.00/255.03 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 500.00/255.03 top(mark(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = top(proper(X)) 500.00/255.03 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 500.00/255.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 500.00/255.03 500.00/255.03 [1 1 1 0 1] [0] [1 1 0 0 0] [0] 500.00/255.03 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 500.00/255.03 top(ok(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = top(active(X)) 500.00/255.03 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 500.00/255.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 500.00/255.03 500.00/255.03 [1 1 2 0 1] [1 1 1 0 1] 500.00/255.03 [0 0 0 0 1] [0 0 0 0 1] 500.00/255.03 active(f(X)) = [0 0 0 0 0]X >= [0 0 0 0 0]X = f(active(X)) 500.00/255.03 [0 0 0 1 0] [0 0 0 1 0] 500.00/255.03 [0 0 0 0 0] [0 0 0 0 0] 500.00/255.04 500.00/255.04 [1 1 2 1 2] [1] [1 1 2 1 2] [1] 500.00/255.04 [0 0 0 0 1] [0] [0 0 0 0 1] [0] 500.00/255.04 f(mark(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = mark(f(X)) 500.00/255.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 500.00/255.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 500.00/255.04 500.00/255.04 [1 1 1 1 1] [1] [1 0 1 1 1] [1] 500.00/255.04 [0 0 0 0 1] [0] [0 0 0 0 1] [0] 500.00/255.04 proper(f(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = f(proper(X)) 500.00/255.04 [0 0 0 1 0] [1] [0 0 0 1 0] [1] 500.00/255.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 500.00/255.04 500.00/255.04 [1] [1] 500.00/255.04 [0] [0] 500.00/255.04 proper(a()) = [1] >= [1] = ok(a()) 500.00/255.04 [1] [1] 500.00/255.04 [0] [0] 500.00/255.04 500.00/255.04 [1 0 0 2 0] [2] [1 0 0 2 0] [2] 500.00/255.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 500.00/255.04 proper(g(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = g(proper(X)) 500.00/255.04 [0 0 0 1 0] [2] [0 0 0 1 0] [2] 500.00/255.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 500.00/255.04 500.00/255.04 [1 1 2 0 2] [0] [1 1 2 0 2] [0] 500.00/255.04 [0 0 0 0 1] [0] [0 0 0 0 1] [0] 500.00/255.04 f(ok(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = ok(f(X)) 500.00/255.04 [0 0 0 1 0] [1] [0 0 0 1 0] [1] 500.00/255.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 500.00/255.04 problem: 500.00/255.04 strict: 500.00/255.04 500.00/255.04 weak: 500.00/255.04 g(ok(X)) -> ok(g(X)) 500.00/255.04 active(f(f(a()))) -> mark(f(g(f(a())))) 500.00/255.04 top(mark(X)) -> top(proper(X)) 500.00/255.04 top(ok(X)) -> top(active(X)) 500.00/255.04 active(f(X)) -> f(active(X)) 500.00/255.04 f(mark(X)) -> mark(f(X)) 500.00/255.04 proper(f(X)) -> f(proper(X)) 500.00/255.04 proper(a()) -> ok(a()) 500.00/255.04 proper(g(X)) -> g(proper(X)) 500.00/255.04 f(ok(X)) -> ok(f(X)) 500.00/255.04 Qed 500.00/255.04 EOF