YES(?,O(n^2)) 208.55/74.92 YES(?,O(n^2)) 208.55/74.93 208.55/74.93 Problem: 208.55/74.93 active(c()) -> mark(f(g(c()))) 208.55/74.93 active(f(g(X))) -> mark(g(X)) 208.55/74.93 proper(c()) -> ok(c()) 208.55/74.93 proper(f(X)) -> f(proper(X)) 208.55/74.93 proper(g(X)) -> g(proper(X)) 208.55/74.93 f(ok(X)) -> ok(f(X)) 208.55/74.93 g(ok(X)) -> ok(g(X)) 208.55/74.93 top(mark(X)) -> top(proper(X)) 208.55/74.93 top(ok(X)) -> top(active(X)) 208.55/74.93 208.55/74.93 Proof: 208.55/74.93 Complexity Transformation Processor: 208.55/74.93 strict: 208.55/74.93 active(c()) -> mark(f(g(c()))) 208.55/74.93 active(f(g(X))) -> mark(g(X)) 208.55/74.93 proper(c()) -> ok(c()) 208.55/74.93 proper(f(X)) -> f(proper(X)) 208.55/74.93 proper(g(X)) -> g(proper(X)) 208.55/74.93 f(ok(X)) -> ok(f(X)) 208.55/74.93 g(ok(X)) -> ok(g(X)) 208.55/74.93 top(mark(X)) -> top(proper(X)) 208.55/74.93 top(ok(X)) -> top(active(X)) 208.55/74.93 weak: 208.55/74.93 208.55/74.93 Matrix Interpretation Processor: dim=1 208.55/74.93 208.55/74.93 max_matrix: 208.55/74.93 1 208.55/74.93 interpretation: 208.55/74.93 [top](x0) = x0 + 18, 208.55/74.93 208.55/74.93 [ok](x0) = x0 + 11, 208.55/74.93 208.55/74.93 [proper](x0) = x0 + 12, 208.55/74.93 208.55/74.93 [mark](x0) = x0, 208.55/74.93 208.55/74.93 [f](x0) = x0 + 16, 208.55/74.93 208.55/74.93 [g](x0) = x0 + 22, 208.55/74.93 208.55/74.93 [active](x0) = x0 + 6, 208.55/74.93 208.55/74.93 [c] = 0 208.55/74.93 orientation: 208.55/74.93 active(c()) = 6 >= 38 = mark(f(g(c()))) 208.55/74.93 208.55/74.93 active(f(g(X))) = X + 44 >= X + 22 = mark(g(X)) 208.55/74.93 208.55/74.93 proper(c()) = 12 >= 11 = ok(c()) 208.55/74.93 208.55/74.93 proper(f(X)) = X + 28 >= X + 28 = f(proper(X)) 208.55/74.93 208.55/74.93 proper(g(X)) = X + 34 >= X + 34 = g(proper(X)) 208.55/74.93 208.55/74.93 f(ok(X)) = X + 27 >= X + 27 = ok(f(X)) 208.55/74.93 208.55/74.93 g(ok(X)) = X + 33 >= X + 33 = ok(g(X)) 208.55/74.93 208.55/74.93 top(mark(X)) = X + 18 >= X + 30 = top(proper(X)) 208.55/74.93 208.55/74.93 top(ok(X)) = X + 29 >= X + 24 = top(active(X)) 208.55/74.93 problem: 208.55/74.93 strict: 208.55/74.93 active(c()) -> mark(f(g(c()))) 208.55/74.93 proper(f(X)) -> f(proper(X)) 208.55/74.93 proper(g(X)) -> g(proper(X)) 208.55/74.93 f(ok(X)) -> ok(f(X)) 208.55/74.93 g(ok(X)) -> ok(g(X)) 208.55/74.93 top(mark(X)) -> top(proper(X)) 208.55/74.93 weak: 208.55/74.93 active(f(g(X))) -> mark(g(X)) 208.55/74.93 proper(c()) -> ok(c()) 208.55/74.93 top(ok(X)) -> top(active(X)) 208.55/74.93 Matrix Interpretation Processor: dim=1 208.55/74.93 208.55/74.93 max_matrix: 208.55/74.93 1 208.55/74.93 interpretation: 208.55/74.93 [top](x0) = x0 + 3, 208.55/74.93 208.55/74.93 [ok](x0) = x0 + 7, 208.55/74.93 208.55/74.93 [proper](x0) = x0 + 7, 208.55/74.93 208.55/74.93 [mark](x0) = x0 + 8, 208.55/74.93 208.55/74.93 [f](x0) = x0 + 1, 208.55/74.93 208.55/74.93 [g](x0) = x0, 208.55/74.93 208.55/74.93 [active](x0) = x0 + 7, 208.55/74.93 208.55/74.93 [c] = 8 208.55/74.93 orientation: 208.55/74.93 active(c()) = 15 >= 17 = mark(f(g(c()))) 208.55/74.93 208.55/74.93 proper(f(X)) = X + 8 >= X + 8 = f(proper(X)) 208.55/74.93 208.55/74.93 proper(g(X)) = X + 7 >= X + 7 = g(proper(X)) 208.55/74.93 208.55/74.93 f(ok(X)) = X + 8 >= X + 8 = ok(f(X)) 208.55/74.93 208.55/74.93 g(ok(X)) = X + 7 >= X + 7 = ok(g(X)) 208.55/74.93 208.55/74.93 top(mark(X)) = X + 11 >= X + 10 = top(proper(X)) 208.55/74.93 208.55/74.93 active(f(g(X))) = X + 8 >= X + 8 = mark(g(X)) 208.55/74.93 208.55/74.93 proper(c()) = 15 >= 15 = ok(c()) 208.55/74.93 208.55/74.93 top(ok(X)) = X + 10 >= X + 10 = top(active(X)) 208.55/74.93 problem: 208.55/74.93 strict: 208.55/74.93 active(c()) -> mark(f(g(c()))) 208.55/74.93 proper(f(X)) -> f(proper(X)) 208.55/74.93 proper(g(X)) -> g(proper(X)) 208.55/74.93 f(ok(X)) -> ok(f(X)) 208.55/74.93 g(ok(X)) -> ok(g(X)) 208.55/74.93 weak: 208.55/74.93 top(mark(X)) -> top(proper(X)) 208.55/74.93 active(f(g(X))) -> mark(g(X)) 208.55/74.93 proper(c()) -> ok(c()) 208.55/74.93 top(ok(X)) -> top(active(X)) 208.55/74.93 Splitting Processor: 208.55/74.93 strict: 208.55/74.93 proper(f(X)) -> f(proper(X)) 208.55/74.93 weak: 208.55/74.93 top(mark(X)) -> top(proper(X)) 208.55/74.93 active(f(g(X))) -> mark(g(X)) 208.55/74.93 proper(c()) -> ok(c()) 208.55/74.93 top(ok(X)) -> top(active(X)) 208.55/74.93 active(c()) -> mark(f(g(c()))) 208.55/74.93 proper(g(X)) -> g(proper(X)) 208.55/74.93 f(ok(X)) -> ok(f(X)) 208.55/74.93 g(ok(X)) -> ok(g(X)) 208.55/74.93 Splitting Processor: 208.55/74.93 strict: 208.55/74.93 active(c()) -> mark(f(g(c()))) 208.55/74.93 weak: 208.55/74.93 proper(f(X)) -> f(proper(X)) 208.55/74.93 top(mark(X)) -> top(proper(X)) 208.55/74.93 active(f(g(X))) -> mark(g(X)) 208.55/74.93 proper(c()) -> ok(c()) 208.55/74.93 top(ok(X)) -> top(active(X)) 208.55/74.93 proper(g(X)) -> g(proper(X)) 208.55/74.93 f(ok(X)) -> ok(f(X)) 208.55/74.93 g(ok(X)) -> ok(g(X)) 208.55/74.93 Bounds Processor: 208.55/74.93 bound: 1 208.55/74.93 enrichment: match 208.55/74.93 automaton: 208.55/74.93 final states: {9} 208.55/74.93 transitions: 208.55/74.93 mark1(16) -> 17* 208.55/74.93 mark1(43) -> 44* 208.55/74.93 f1(35) -> 36* 208.55/74.93 f1(25) -> 26* 208.55/74.93 f1(15) -> 16* 208.55/74.93 g1(32) -> 33* 208.55/74.93 g1(14) -> 15* 208.55/74.93 g1(53) -> 54* 208.55/74.93 g1(28) -> 29* 208.55/74.93 c1() -> 14* 208.55/74.93 top1(19) -> 20* 208.55/74.93 proper1(45) -> 46* 208.55/74.93 proper1(52) -> 53* 208.55/74.93 proper1(27) -> 28* 208.55/74.93 proper1(24) -> 25* 208.55/74.93 proper1(18) -> 19* 208.55/74.93 ok1(30) -> 31* 208.55/74.93 ok1(36) -> 37* 208.55/74.93 ok1(33) -> 34* 208.55/74.93 active1(61) -> 62* 208.55/74.93 active1(38) -> 39* 208.55/74.93 active0(9) -> 9* 208.55/74.93 c0() -> 9* 208.55/74.93 mark0(9) -> 9* 208.55/74.93 f0(9) -> 9* 208.55/74.93 g0(9) -> 9* 208.55/74.93 proper0(9) -> 9* 208.55/74.93 top0(9) -> 9* 208.55/74.93 ok0(9) -> 9* 208.55/74.93 14 -> 30,27 208.55/74.93 15 -> 24* 208.55/74.93 16 -> 18* 208.55/74.93 17 -> 9* 208.55/74.93 20 -> 9* 208.55/74.93 26 -> 19* 208.55/74.93 29 -> 25* 208.55/74.93 30 -> 32* 208.55/74.93 31 -> 53,28 208.55/74.93 32 -> 52* 208.55/74.93 33 -> 61,43,35 208.55/74.93 34 -> 54,29 208.55/74.93 36 -> 38* 208.55/74.93 37 -> 26* 208.55/74.93 39 -> 19* 208.55/74.93 43 -> 45* 208.55/74.93 44 -> 39* 208.55/74.93 46 -> 19* 208.55/74.93 54 -> 46* 208.55/74.93 62 -> 19* 208.55/74.93 problem: 208.55/74.93 strict: 208.55/74.93 208.55/74.93 weak: 208.55/74.93 active(c()) -> mark(f(g(c()))) 208.55/74.93 proper(f(X)) -> f(proper(X)) 208.55/74.93 top(mark(X)) -> top(proper(X)) 208.55/74.93 active(f(g(X))) -> mark(g(X)) 208.55/74.93 proper(c()) -> ok(c()) 208.55/74.93 top(ok(X)) -> top(active(X)) 208.55/74.93 proper(g(X)) -> g(proper(X)) 208.55/74.93 f(ok(X)) -> ok(f(X)) 208.55/74.93 g(ok(X)) -> ok(g(X)) 208.55/74.93 Qed 208.55/74.93 208.55/74.93 strict: 208.55/74.93 proper(g(X)) -> g(proper(X)) 208.55/74.93 f(ok(X)) -> ok(f(X)) 208.55/74.93 g(ok(X)) -> ok(g(X)) 208.55/74.93 weak: 208.55/74.93 active(c()) -> mark(f(g(c()))) 208.55/74.93 proper(f(X)) -> f(proper(X)) 208.55/74.93 top(mark(X)) -> top(proper(X)) 208.55/74.93 active(f(g(X))) -> mark(g(X)) 208.55/74.93 proper(c()) -> ok(c()) 208.55/74.93 top(ok(X)) -> top(active(X)) 208.55/74.93 Splitting Processor: 208.55/74.93 strict: 208.55/74.93 proper(g(X)) -> g(proper(X)) 208.55/74.93 weak: 208.55/74.93 active(c()) -> mark(f(g(c()))) 208.55/74.93 proper(f(X)) -> f(proper(X)) 208.55/74.93 top(mark(X)) -> top(proper(X)) 208.55/74.93 active(f(g(X))) -> mark(g(X)) 208.55/74.93 proper(c()) -> ok(c()) 208.55/74.93 top(ok(X)) -> top(active(X)) 208.55/74.93 f(ok(X)) -> ok(f(X)) 208.55/74.93 g(ok(X)) -> ok(g(X)) 208.55/74.93 Splitting Processor: 208.55/74.93 strict: 208.55/74.93 f(ok(X)) -> ok(f(X)) 208.55/74.93 weak: 208.55/74.93 proper(g(X)) -> g(proper(X)) 208.55/74.93 active(c()) -> mark(f(g(c()))) 208.55/74.93 proper(f(X)) -> f(proper(X)) 208.55/74.93 top(mark(X)) -> top(proper(X)) 208.55/74.93 active(f(g(X))) -> mark(g(X)) 208.55/74.93 proper(c()) -> ok(c()) 208.55/74.93 top(ok(X)) -> top(active(X)) 208.55/74.93 g(ok(X)) -> ok(g(X)) 208.55/74.93 Matrix Interpretation Processor: dim=4 208.55/74.93 208.55/74.93 max_matrix: 208.55/74.93 [1 1 1 1] 208.55/74.93 [0 1 0 0] 208.55/74.93 [0 0 0 1] 208.55/74.93 [0 0 0 0] 208.55/74.93 interpretation: 208.55/74.93 [1 0 1 0] [0] 208.55/74.93 [0 0 0 0] [0] 208.55/74.93 [top](x0) = [0 0 0 0]x0 + [1] 208.55/74.93 [0 0 0 0] [0], 208.55/74.93 208.55/74.93 [1 0 0 0] [0] 208.55/74.93 [0 1 0 0] [1] 208.55/74.93 [ok](x0) = [0 0 0 1]x0 + [0] 208.55/74.93 [0 0 0 0] [0], 208.55/74.93 208.55/74.93 [1 1 0 0] [0] 208.55/74.93 [0 1 0 0] [1] 208.55/74.93 [proper](x0) = [0 0 0 1]x0 + [0] 208.55/74.93 [0 0 0 0] [0], 208.55/74.93 208.55/74.93 [1 1 1 1] 208.55/74.93 [0 0 0 0] 208.55/74.93 [mark](x0) = [0 0 0 0]x0 208.55/74.93 [0 0 0 0] , 208.55/74.93 208.55/74.93 [1 1 0 0] [0] 208.55/74.93 [0 1 0 0] [1] 208.55/74.93 [f](x0) = [0 0 0 0]x0 + [0] 208.55/74.93 [0 0 0 0] [0], 208.55/74.93 208.55/74.93 [1 0 0 0] 208.55/74.93 [0 1 0 0] 208.55/74.93 [g](x0) = [0 0 0 0]x0 208.55/74.93 [0 0 0 0] , 208.55/74.93 208.55/74.93 [1 0 0 1] 208.55/74.93 [0 0 0 0] 208.55/74.93 [active](x0) = [0 0 0 0]x0 208.55/74.93 [0 0 0 0] , 208.55/74.93 208.55/74.93 [1] 208.55/74.93 [0] 208.55/74.93 [c] = [0] 208.55/74.93 [1] 208.55/74.93 orientation: 208.55/74.93 [1 1 0 0] [1] [1 1 0 0] [0] 208.55/74.93 [0 1 0 0] [2] [0 1 0 0] [2] 208.55/74.93 f(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = ok(f(X)) 208.55/74.93 [0 0 0 0] [0] [0 0 0 0] [0] 208.55/74.93 208.55/74.93 [1 1 0 0] [0] [1 1 0 0] [0] 208.55/74.93 [0 1 0 0] [1] [0 1 0 0] [1] 208.55/74.93 proper(g(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = g(proper(X)) 208.55/74.94 [0 0 0 0] [0] [0 0 0 0] [0] 208.55/74.94 208.55/74.94 [2] [2] 208.55/74.94 [0] [0] 208.55/74.94 active(c()) = [0] >= [0] = mark(f(g(c()))) 208.55/74.94 [0] [0] 208.55/74.94 208.55/74.94 [1 2 0 0] [1] [1 2 0 0] [1] 208.55/74.94 [0 1 0 0] [2] [0 1 0 0] [2] 208.55/74.94 proper(f(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = f(proper(X)) 208.55/74.94 [0 0 0 0] [0] [0 0 0 0] [0] 208.55/74.94 208.55/74.94 [1 1 1 1] [0] [1 1 0 1] [0] 208.55/74.94 [0 0 0 0] [0] [0 0 0 0] [0] 208.55/74.94 top(mark(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(proper(X)) 208.55/74.94 [0 0 0 0] [0] [0 0 0 0] [0] 208.55/74.94 208.55/74.94 [1 1 0 0] [1 1 0 0] 208.55/74.94 [0 0 0 0] [0 0 0 0] 208.55/74.94 active(f(g(X))) = [0 0 0 0]X >= [0 0 0 0]X = mark(g(X)) 208.55/74.94 [0 0 0 0] [0 0 0 0] 208.55/74.94 208.55/74.94 [1] [1] 208.55/74.94 [1] [1] 208.55/74.94 proper(c()) = [1] >= [1] = ok(c()) 208.55/74.94 [0] [0] 208.55/74.94 208.55/74.94 [1 0 0 1] [0] [1 0 0 1] [0] 208.55/74.94 [0 0 0 0] [0] [0 0 0 0] [0] 208.55/74.94 top(ok(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(active(X)) 208.55/74.94 [0 0 0 0] [0] [0 0 0 0] [0] 208.55/74.94 208.55/74.94 [1 0 0 0] [0] [1 0 0 0] [0] 208.55/74.94 [0 1 0 0] [1] [0 1 0 0] [1] 208.55/74.94 g(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = ok(g(X)) 208.55/74.94 [0 0 0 0] [0] [0 0 0 0] [0] 208.55/74.94 problem: 208.55/74.94 strict: 208.55/74.94 208.55/74.94 weak: 208.55/74.94 f(ok(X)) -> ok(f(X)) 208.55/74.94 proper(g(X)) -> g(proper(X)) 208.55/74.94 active(c()) -> mark(f(g(c()))) 208.55/74.94 proper(f(X)) -> f(proper(X)) 208.55/74.94 top(mark(X)) -> top(proper(X)) 208.55/74.94 active(f(g(X))) -> mark(g(X)) 208.55/74.94 proper(c()) -> ok(c()) 208.55/74.94 top(ok(X)) -> top(active(X)) 208.55/74.94 g(ok(X)) -> ok(g(X)) 208.55/74.94 Qed 208.55/74.94 208.55/74.94 strict: 208.55/74.94 g(ok(X)) -> ok(g(X)) 208.55/74.94 weak: 208.55/74.94 f(ok(X)) -> ok(f(X)) 208.55/74.94 proper(g(X)) -> g(proper(X)) 208.55/74.94 active(c()) -> mark(f(g(c()))) 208.55/74.94 proper(f(X)) -> f(proper(X)) 208.55/74.94 top(mark(X)) -> top(proper(X)) 208.55/74.94 active(f(g(X))) -> mark(g(X)) 208.55/74.94 proper(c()) -> ok(c()) 208.55/74.94 top(ok(X)) -> top(active(X)) 208.55/74.94 Matrix Interpretation Processor: dim=5 208.55/74.94 208.55/74.94 max_matrix: 208.55/74.94 [1 1 1 1 1] 208.55/74.94 [0 0 1 1 1] 208.55/74.94 [0 0 0 1 0] 208.55/74.94 [0 0 0 1 1] 208.55/74.94 [0 0 0 0 0] 208.55/74.94 interpretation: 208.55/74.94 [1 1 0 0 1] [0] 208.55/74.94 [0 0 0 0 0] [1] 208.55/74.94 [top](x0) = [0 0 0 0 0]x0 + [0] 208.55/74.94 [0 0 0 0 0] [1] 208.55/74.94 [0 0 0 0 0] [0], 208.55/74.94 208.55/74.94 [1 0 0 0 0] [1] 208.55/74.94 [0 0 1 0 1] [1] 208.55/74.94 [ok](x0) = [0 0 0 0 0]x0 + [0] 208.55/74.94 [0 0 0 1 0] [1] 208.55/74.94 [0 0 0 0 0] [0], 208.55/74.94 208.55/74.94 [1 0 0 1 0] [1] 208.55/74.94 [0 0 1 0 1] [1] 208.55/74.94 [proper](x0) = [0 0 0 1 0]x0 + [1] 208.55/74.94 [0 0 0 1 0] [1] 208.55/74.94 [0 0 0 0 0] [0], 208.55/74.94 208.55/74.94 [1 0 1 0 1] [0] 208.55/74.94 [0 0 0 1 0] [1] 208.55/74.94 [mark](x0) = [0 0 0 0 0]x0 + [0] 208.55/74.94 [0 0 0 0 0] [0] 208.55/74.94 [0 0 0 0 0] [1], 208.55/74.94 208.55/74.94 [1 0 0 0 0] 208.55/74.94 [0 0 0 1 0] 208.55/74.94 [f](x0) = [0 0 0 1 0]x0 208.55/74.94 [0 0 0 1 0] 208.55/74.94 [0 0 0 0 0] , 208.55/74.95 208.55/74.95 [1 0 0 1 0] [0] 208.55/74.95 [0 0 0 0 0] [1] 208.55/74.95 [g](x0) = [0 0 0 0 0]x0 + [0] 208.55/74.95 [0 0 0 1 0] [1] 208.55/74.95 [0 0 0 0 0] [0], 208.55/74.95 208.55/74.95 [1 0 0 0 1] [0] 208.55/74.95 [0 0 1 0 0] [1] 208.55/74.95 [active](x0) = [0 0 0 0 0]x0 + [0] 208.55/74.95 [0 0 0 0 1] [1] 208.55/74.95 [0 0 0 0 0] [1], 208.55/74.95 208.55/74.95 [1] 208.55/74.95 [0] 208.55/74.95 [c] = [1] 208.55/74.95 [0] 208.55/74.95 [1] 208.55/74.95 orientation: 208.55/74.95 [1 0 0 1 0] [2] [1 0 0 1 0] [1] 208.55/74.95 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 208.55/74.95 g(ok(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = ok(g(X)) 208.55/74.95 [0 0 0 1 0] [2] [0 0 0 1 0] [2] 208.55/74.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 208.55/74.95 208.55/74.95 [1 0 0 0 0] [1] [1 0 0 0 0] [1] 208.55/74.95 [0 0 0 1 0] [1] [0 0 0 1 0] [1] 208.55/74.95 f(ok(X)) = [0 0 0 1 0]X + [1] >= [0 0 0 0 0]X + [0] = ok(f(X)) 208.55/74.95 [0 0 0 1 0] [1] [0 0 0 1 0] [1] 208.55/74.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 208.55/74.95 208.55/74.95 [1 0 0 2 0] [2] [1 0 0 2 0] [2] 208.55/74.95 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 208.55/74.95 proper(g(X)) = [0 0 0 1 0]X + [2] >= [0 0 0 0 0]X + [0] = g(proper(X)) 208.55/74.95 [0 0 0 1 0] [2] [0 0 0 1 0] [2] 208.55/74.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 208.55/74.95 208.55/74.95 [2] [2] 208.55/74.95 [2] [2] 208.55/74.95 active(c()) = [0] >= [0] = mark(f(g(c()))) 208.55/74.95 [2] [0] 208.55/74.95 [1] [1] 208.55/74.95 208.55/74.95 [1 0 0 1 0] [1] [1 0 0 1 0] [1] 208.55/74.95 [0 0 0 1 0] [1] [0 0 0 1 0] [1] 208.55/74.95 proper(f(X)) = [0 0 0 1 0]X + [1] >= [0 0 0 1 0]X + [1] = f(proper(X)) 208.55/74.95 [0 0 0 1 0] [1] [0 0 0 1 0] [1] 208.55/74.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 208.55/74.95 208.55/74.95 [1 0 1 1 1] [2] [1 0 1 1 1] [2] 208.55/74.95 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 208.55/74.95 top(mark(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = top(proper(X)) 208.55/74.95 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 208.55/74.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 208.55/74.95 208.55/74.95 [1 0 0 1 0] [0] [1 0 0 1 0] [0] 208.55/74.95 [0 0 0 1 0] [2] [0 0 0 1 0] [2] 208.55/74.95 active(f(g(X))) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = mark(g(X)) 208.55/74.95 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 208.55/74.95 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 208.55/74.95 208.55/74.95 [2] [2] 208.55/74.95 [3] [3] 208.55/74.95 proper(c()) = [1] >= [0] = ok(c()) 208.55/74.95 [1] [1] 208.55/74.95 [0] [0] 208.55/74.95 208.55/74.95 [1 0 1 0 1] [2] [1 0 1 0 1] [2] 208.55/74.95 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 208.55/74.95 top(ok(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = top(active(X)) 208.55/74.95 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 208.55/74.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 208.55/74.95 problem: 208.55/74.95 strict: 208.55/74.95 208.55/74.95 weak: 208.55/74.95 g(ok(X)) -> ok(g(X)) 208.55/74.95 f(ok(X)) -> ok(f(X)) 208.55/74.95 proper(g(X)) -> g(proper(X)) 208.55/74.95 active(c()) -> mark(f(g(c()))) 208.55/74.95 proper(f(X)) -> f(proper(X)) 208.55/74.95 top(mark(X)) -> top(proper(X)) 208.55/74.95 active(f(g(X))) -> mark(g(X)) 208.55/74.95 proper(c()) -> ok(c()) 208.55/74.95 top(ok(X)) -> top(active(X)) 208.55/74.95 Qed 208.55/74.95 208.55/74.95 strict: 208.55/74.95 f(ok(X)) -> ok(f(X)) 208.55/74.95 g(ok(X)) -> ok(g(X)) 208.55/74.95 weak: 208.55/74.95 proper(g(X)) -> g(proper(X)) 208.55/74.95 active(c()) -> mark(f(g(c()))) 208.55/74.95 proper(f(X)) -> f(proper(X)) 208.55/74.95 top(mark(X)) -> top(proper(X)) 208.55/74.95 active(f(g(X))) -> mark(g(X)) 208.55/74.95 proper(c()) -> ok(c()) 208.55/74.95 top(ok(X)) -> top(active(X)) 208.55/74.95 Matrix Interpretation Processor: dim=5 208.55/74.95 208.55/74.95 max_matrix: 208.55/74.95 [1 1 1 1 1] 208.55/74.95 [0 0 1 1 0] 208.55/74.95 [0 0 0 1 0] 208.55/74.95 [0 0 0 0 0] 208.55/74.95 [0 0 0 0 1] 208.55/74.95 interpretation: 208.55/74.95 [1 1 0 0 0] [0] 208.55/74.95 [0 0 1 0 0] [0] 208.55/74.95 [top](x0) = [0 0 0 1 0]x0 + [0] 208.55/74.95 [0 0 0 0 0] [1] 208.55/74.95 [0 0 0 0 0] [0], 208.55/74.95 208.55/74.95 [1 0 0 0 0] 208.55/74.95 [0 0 1 1 0] 208.55/74.95 [ok](x0) = [0 0 0 0 0]x0 208.55/74.95 [0 0 0 0 0] 208.55/74.95 [0 0 0 0 1] , 208.55/74.95 208.55/74.95 [1 0 0 0 1] 208.55/74.95 [0 0 1 1 0] 208.55/74.95 [proper](x0) = [0 0 0 0 0]x0 208.55/74.95 [0 0 0 0 0] 208.55/74.95 [0 0 0 0 1] , 208.55/74.95 208.55/74.95 [1 0 1 0 1] [0] 208.55/74.95 [0 0 0 1 0] [0] 208.55/74.95 [mark](x0) = [0 0 0 0 0]x0 + [0] 208.55/74.95 [0 0 0 0 0] [0] 208.55/74.95 [0 0 0 0 0] [1], 208.55/74.95 208.55/74.95 [1 0 0 0 1] 208.55/74.95 [0 0 0 0 0] 208.55/74.95 [f](x0) = [0 0 0 0 0]x0 208.55/74.95 [0 0 0 0 0] 208.55/74.95 [0 0 0 0 1] , 208.55/74.95 208.55/74.95 [1 0 0 0 0] [0] 208.55/74.95 [0 0 0 0 0] [0] 208.55/74.95 [g](x0) = [0 0 0 0 0]x0 + [0] 208.55/74.95 [0 0 0 0 0] [0] 208.55/74.95 [0 0 0 0 1] [1], 208.55/74.95 208.55/74.95 [1 0 1 1 0] [0] 208.55/74.95 [0 0 0 0 0] [0] 208.55/74.95 [active](x0) = [0 0 0 0 0]x0 + [0] 208.55/74.95 [0 0 0 0 0] [0] 208.55/74.95 [0 0 0 0 0] [1], 208.55/74.95 208.55/74.95 [1] 208.55/74.95 [0] 208.55/74.95 [c] = [1] 208.55/74.95 [1] 208.55/74.95 [0] 208.55/74.95 orientation: 208.55/74.95 [1 0 0 0 1] [1] [1 0 0 0 1] [0] 208.55/74.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 208.55/74.95 proper(g(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = g(proper(X)) 208.55/74.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 208.55/74.95 [0 0 0 0 1] [1] [0 0 0 0 1] [1] 208.55/74.95 208.55/74.95 [3] [3] 208.55/74.95 [0] [0] 208.55/74.95 active(c()) = [0] >= [0] = mark(f(g(c()))) 208.55/74.95 [0] [0] 208.55/74.95 [1] [1] 208.55/74.95 208.55/74.95 [1 0 0 0 2] [1 0 0 0 2] 208.55/74.95 [0 0 0 0 0] [0 0 0 0 0] 208.55/74.95 proper(f(X)) = [0 0 0 0 0]X >= [0 0 0 0 0]X = f(proper(X)) 208.55/74.95 [0 0 0 0 0] [0 0 0 0 0] 208.55/74.95 [0 0 0 0 1] [0 0 0 0 1] 208.55/74.95 208.55/74.95 [1 0 1 1 1] [0] [1 0 1 1 1] [0] 208.55/74.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 208.55/74.95 top(mark(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = top(proper(X)) 208.55/74.95 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 208.55/74.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 208.55/74.95 208.55/74.95 [1 0 0 0 1] [1] [1 0 0 0 1] [1] 208.55/74.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 208.55/74.95 active(f(g(X))) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = mark(g(X)) 208.55/74.95 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 208.55/74.96 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 208.55/74.96 208.55/74.96 [1] [1] 208.55/74.96 [2] [2] 208.55/74.96 proper(c()) = [0] >= [0] = ok(c()) 208.55/74.96 [0] [0] 208.55/74.96 [0] [0] 208.55/74.96 208.55/74.96 [1 0 1 1 0] [0] [1 0 1 1 0] [0] 208.55/74.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 208.55/74.96 top(ok(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = top(active(X)) 208.55/74.96 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 208.55/74.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 208.55/74.96 208.55/74.96 [1 0 0 0 1] [1 0 0 0 1] 208.55/74.96 [0 0 0 0 0] [0 0 0 0 0] 208.55/74.96 f(ok(X)) = [0 0 0 0 0]X >= [0 0 0 0 0]X = ok(f(X)) 208.55/74.96 [0 0 0 0 0] [0 0 0 0 0] 208.55/74.96 [0 0 0 0 1] [0 0 0 0 1] 208.55/74.96 208.55/74.96 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 208.55/74.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 208.55/74.96 g(ok(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = ok(g(X)) 208.55/74.96 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 208.55/74.96 [0 0 0 0 1] [1] [0 0 0 0 1] [1] 208.55/74.96 problem: 208.55/74.96 strict: 208.55/74.96 208.55/74.96 weak: 208.55/74.96 proper(g(X)) -> g(proper(X)) 208.55/74.96 active(c()) -> mark(f(g(c()))) 208.55/74.96 proper(f(X)) -> f(proper(X)) 208.55/74.96 top(mark(X)) -> top(proper(X)) 208.55/74.96 active(f(g(X))) -> mark(g(X)) 208.55/74.96 proper(c()) -> ok(c()) 208.55/74.96 top(ok(X)) -> top(active(X)) 208.55/74.96 f(ok(X)) -> ok(f(X)) 208.55/74.96 g(ok(X)) -> ok(g(X)) 208.55/74.96 Qed 208.55/74.96 208.55/74.96 strict: 208.55/74.96 active(c()) -> mark(f(g(c()))) 208.55/74.96 proper(g(X)) -> g(proper(X)) 208.55/74.96 f(ok(X)) -> ok(f(X)) 208.55/74.96 g(ok(X)) -> ok(g(X)) 208.55/74.96 weak: 208.55/74.96 proper(f(X)) -> f(proper(X)) 208.55/74.96 top(mark(X)) -> top(proper(X)) 208.55/74.96 active(f(g(X))) -> mark(g(X)) 208.55/74.96 proper(c()) -> ok(c()) 208.55/74.96 top(ok(X)) -> top(active(X)) 208.55/74.96 Matrix Interpretation Processor: dim=4 208.55/74.96 208.55/74.96 max_matrix: 208.55/74.96 [1 1 0 1] 208.55/74.96 [0 0 1 1] 208.55/74.96 [0 0 0 1] 208.55/74.96 [0 0 0 1] 208.55/74.96 interpretation: 208.55/74.96 [1 1 0 0] [0] 208.55/74.96 [0 0 0 0] [0] 208.55/74.96 [top](x0) = [0 0 0 0]x0 + [1] 208.55/74.96 [0 0 0 0] [0], 208.55/74.96 208.55/74.96 [1 0 0 0] 208.55/74.96 [0 0 1 0] 208.55/74.96 [ok](x0) = [0 0 0 0]x0 208.55/74.96 [0 0 0 1] , 208.55/74.96 208.55/74.96 [1 0 0 1] 208.55/74.96 [0 0 1 0] 208.55/74.96 [proper](x0) = [0 0 0 1]x0 208.55/74.96 [0 0 0 1] , 208.55/74.96 208.55/74.96 [1 0 0 0] 208.55/74.96 [0 0 1 1] 208.55/74.96 [mark](x0) = [0 0 0 0]x0 208.55/74.96 [0 0 0 0] , 208.55/74.96 208.55/74.96 [1 0 0 0] [0] 208.55/74.96 [0 0 0 1] [0] 208.55/74.96 [f](x0) = [0 0 0 1]x0 + [0] 208.55/74.96 [0 0 0 1] [1], 208.55/74.96 208.55/74.96 [1 0 0 1] 208.55/74.96 [0 0 0 0] 208.55/74.96 [g](x0) = [0 0 0 0]x0 208.55/74.96 [0 0 0 1] , 208.55/74.96 208.55/74.96 [1 0 0 0] 208.55/74.96 [0 0 1 0] 208.55/74.96 [active](x0) = [0 0 0 0]x0 208.55/74.96 [0 0 0 0] , 208.55/74.96 208.55/74.96 [0] 208.55/74.96 [0] 208.55/74.96 [c] = [1] 208.55/74.96 [0] 208.55/74.96 orientation: 208.55/74.96 [1 0 0 1] [1] [1 0 0 1] [0] 208.55/74.96 [0 0 0 1] [0] [0 0 0 1] [0] 208.55/74.96 proper(f(X)) = [0 0 0 1]X + [1] >= [0 0 0 1]X + [0] = f(proper(X)) 208.55/74.96 [0 0 0 1] [1] [0 0 0 1] [1] 208.55/74.96 208.55/74.96 [1 0 1 1] [0] [1 0 1 1] [0] 208.55/74.96 [0 0 0 0] [0] [0 0 0 0] [0] 208.55/74.96 top(mark(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(proper(X)) 208.55/74.96 [0 0 0 0] [0] [0 0 0 0] [0] 208.55/74.96 208.55/74.96 [1 0 0 1] [1 0 0 1] 208.55/74.96 [0 0 0 1] [0 0 0 1] 208.55/74.96 active(f(g(X))) = [0 0 0 0]X >= [0 0 0 0]X = mark(g(X)) 208.55/74.96 [0 0 0 0] [0 0 0 0] 208.55/74.96 208.55/74.96 [0] [0] 208.55/74.96 [1] [1] 208.55/74.96 proper(c()) = [0] >= [0] = ok(c()) 208.55/74.96 [0] [0] 208.55/74.96 208.55/74.96 [1 0 1 0] [0] [1 0 1 0] [0] 208.55/74.96 [0 0 0 0] [0] [0 0 0 0] [0] 208.55/74.96 top(ok(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(active(X)) 208.55/74.96 [0 0 0 0] [0] [0 0 0 0] [0] 208.55/74.96 208.55/74.96 [0] [0] 208.55/74.96 [1] [1] 208.55/74.96 active(c()) = [0] >= [0] = mark(f(g(c()))) 208.55/74.96 [0] [0] 208.55/74.96 208.55/74.96 [1 0 0 2] [1 0 0 2] 208.55/74.96 [0 0 0 0] [0 0 0 0] 208.55/74.96 proper(g(X)) = [0 0 0 1]X >= [0 0 0 0]X = g(proper(X)) 208.55/74.96 [0 0 0 1] [0 0 0 1] 208.55/74.96 208.55/74.96 [1 0 0 0] [0] [1 0 0 0] [0] 208.55/74.96 [0 0 0 1] [0] [0 0 0 1] [0] 208.55/74.96 f(ok(X)) = [0 0 0 1]X + [0] >= [0 0 0 0]X + [0] = ok(f(X)) 208.55/74.96 [0 0 0 1] [1] [0 0 0 1] [1] 208.55/74.96 208.55/74.96 [1 0 0 1] [1 0 0 1] 208.55/74.96 [0 0 0 0] [0 0 0 0] 208.55/74.96 g(ok(X)) = [0 0 0 0]X >= [0 0 0 0]X = ok(g(X)) 208.55/74.96 [0 0 0 1] [0 0 0 1] 208.55/74.96 problem: 208.55/74.96 strict: 208.55/74.96 208.55/74.96 weak: 208.55/74.96 proper(f(X)) -> f(proper(X)) 208.55/74.96 top(mark(X)) -> top(proper(X)) 208.55/74.96 active(f(g(X))) -> mark(g(X)) 208.55/74.96 proper(c()) -> ok(c()) 208.55/74.96 top(ok(X)) -> top(active(X)) 208.55/74.96 active(c()) -> mark(f(g(c()))) 208.55/74.96 proper(g(X)) -> g(proper(X)) 208.55/74.96 f(ok(X)) -> ok(f(X)) 208.55/74.96 g(ok(X)) -> ok(g(X)) 208.55/74.96 Qed 208.55/74.97 EOF