YES(?,O(n^4)) 1174.98/295.82 YES(?,O(n^4)) 1174.98/295.83 1174.98/295.83 Problem: 1174.98/295.83 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.83 active(g(X)) -> g(active(X)) 1174.98/295.83 g(mark(X)) -> mark(g(X)) 1174.98/295.83 proper(f(X)) -> f(proper(X)) 1174.98/295.83 proper(a()) -> ok(a()) 1174.98/295.83 proper(g(X)) -> g(proper(X)) 1174.98/295.83 f(ok(X)) -> ok(f(X)) 1174.98/295.83 g(ok(X)) -> ok(g(X)) 1174.98/295.83 top(mark(X)) -> top(proper(X)) 1174.98/295.83 top(ok(X)) -> top(active(X)) 1174.98/295.83 1174.98/295.83 Proof: 1174.98/295.83 Complexity Transformation Processor: 1174.98/295.83 strict: 1174.98/295.83 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.83 active(g(X)) -> g(active(X)) 1174.98/295.83 g(mark(X)) -> mark(g(X)) 1174.98/295.83 proper(f(X)) -> f(proper(X)) 1174.98/295.83 proper(a()) -> ok(a()) 1174.98/295.83 proper(g(X)) -> g(proper(X)) 1174.98/295.83 f(ok(X)) -> ok(f(X)) 1174.98/295.83 g(ok(X)) -> ok(g(X)) 1174.98/295.83 top(mark(X)) -> top(proper(X)) 1174.98/295.83 top(ok(X)) -> top(active(X)) 1174.98/295.83 weak: 1174.98/295.83 1174.98/295.83 Matrix Interpretation Processor: dim=1 1174.98/295.83 1174.98/295.83 max_matrix: 1174.98/295.83 1 1174.98/295.83 interpretation: 1174.98/295.83 [top](x0) = x0 + 9, 1174.98/295.83 1174.98/295.83 [ok](x0) = x0 + 2, 1174.98/295.83 1174.98/295.83 [proper](x0) = x0 + 3, 1174.98/295.83 1174.98/295.83 [mark](x0) = x0 + 4, 1174.98/295.83 1174.98/295.83 [g](x0) = x0 + 14, 1174.98/295.83 1174.98/295.83 [active](x0) = x0 + 1, 1174.98/295.83 1174.98/295.83 [f](x0) = x0 + 1, 1174.98/295.83 1174.98/295.83 [a] = 1 1174.98/295.83 orientation: 1174.98/295.83 active(f(f(a()))) = 4 >= 21 = mark(f(g(f(a())))) 1174.98/295.83 1174.98/295.83 active(g(X)) = X + 15 >= X + 15 = g(active(X)) 1174.98/295.83 1174.98/295.83 g(mark(X)) = X + 18 >= X + 18 = mark(g(X)) 1174.98/295.83 1174.98/295.83 proper(f(X)) = X + 4 >= X + 4 = f(proper(X)) 1174.98/295.83 1174.98/295.83 proper(a()) = 4 >= 3 = ok(a()) 1174.98/295.83 1174.98/295.83 proper(g(X)) = X + 17 >= X + 17 = g(proper(X)) 1174.98/295.83 1174.98/295.83 f(ok(X)) = X + 3 >= X + 3 = ok(f(X)) 1174.98/295.83 1174.98/295.83 g(ok(X)) = X + 16 >= X + 16 = ok(g(X)) 1174.98/295.83 1174.98/295.83 top(mark(X)) = X + 13 >= X + 12 = top(proper(X)) 1174.98/295.83 1174.98/295.83 top(ok(X)) = X + 11 >= X + 10 = top(active(X)) 1174.98/295.83 problem: 1174.98/295.83 strict: 1174.98/295.83 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.83 active(g(X)) -> g(active(X)) 1174.98/295.83 g(mark(X)) -> mark(g(X)) 1174.98/295.83 proper(f(X)) -> f(proper(X)) 1174.98/295.83 proper(g(X)) -> g(proper(X)) 1174.98/295.83 f(ok(X)) -> ok(f(X)) 1174.98/295.83 g(ok(X)) -> ok(g(X)) 1174.98/295.83 weak: 1174.98/295.83 proper(a()) -> ok(a()) 1174.98/295.83 top(mark(X)) -> top(proper(X)) 1174.98/295.83 top(ok(X)) -> top(active(X)) 1174.98/295.83 Splitting Processor: 1174.98/295.83 strict: 1174.98/295.83 f(ok(X)) -> ok(f(X)) 1174.98/295.83 weak: 1174.98/295.83 proper(a()) -> ok(a()) 1174.98/295.83 top(mark(X)) -> top(proper(X)) 1174.98/295.83 top(ok(X)) -> top(active(X)) 1174.98/295.83 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.83 active(g(X)) -> g(active(X)) 1174.98/295.83 g(mark(X)) -> mark(g(X)) 1174.98/295.83 proper(f(X)) -> f(proper(X)) 1174.98/295.83 proper(g(X)) -> g(proper(X)) 1174.98/295.83 g(ok(X)) -> ok(g(X)) 1174.98/295.83 Splitting Processor: 1174.98/295.83 strict: 1174.98/295.83 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.83 weak: 1174.98/295.83 f(ok(X)) -> ok(f(X)) 1174.98/295.83 proper(a()) -> ok(a()) 1174.98/295.83 top(mark(X)) -> top(proper(X)) 1174.98/295.83 top(ok(X)) -> top(active(X)) 1174.98/295.83 active(g(X)) -> g(active(X)) 1174.98/295.83 g(mark(X)) -> mark(g(X)) 1174.98/295.83 proper(f(X)) -> f(proper(X)) 1174.98/295.83 proper(g(X)) -> g(proper(X)) 1174.98/295.83 g(ok(X)) -> ok(g(X)) 1174.98/295.83 Bounds Processor: 1174.98/295.83 bound: 1 1174.98/295.83 enrichment: match 1174.98/295.83 automaton: 1174.98/295.83 final states: {9} 1174.98/295.83 transitions: 1174.98/295.83 mark1(18) -> 19* 1174.98/295.83 f1(15) -> 16* 1174.98/295.83 f1(47) -> 48* 1174.98/295.83 f1(17) -> 18* 1174.98/295.83 f1(41) -> 42* 1174.98/295.83 f1(26) -> 27* 1174.98/295.83 f1(58) -> 59* 1174.98/295.83 g1(50) -> 51* 1174.98/295.83 g1(32) -> 33* 1174.98/295.83 g1(79) -> 80* 1174.98/295.83 g1(76) -> 77* 1174.98/295.83 g1(16) -> 17* 1174.98/295.83 g1(68) -> 69* 1174.98/295.83 g1(38) -> 39* 1174.98/295.83 g1(23) -> 24* 1174.98/295.83 a1() -> 15* 1174.98/295.83 top1(21) -> 22* 1174.98/295.83 proper1(40) -> 41* 1174.98/295.83 proper1(25) -> 26* 1174.98/295.83 proper1(20) -> 21* 1174.98/295.83 proper1(37) -> 38* 1174.98/295.83 proper1(31) -> 32* 1174.98/295.83 ok1(69) -> 70* 1174.98/295.83 ok1(59) -> 60* 1174.98/295.83 ok1(51) -> 52* 1174.98/295.83 ok1(48) -> 49* 1174.98/295.83 ok1(43) -> 44* 1174.98/295.83 active1(84) -> 85* 1174.98/295.83 active1(71) -> 72* 1174.98/295.83 active1(61) -> 62* 1174.98/295.83 active1(78) -> 79* 1174.98/295.83 active0(9) -> 9* 1174.98/295.83 f0(9) -> 9* 1174.98/295.83 a0() -> 9* 1174.98/295.83 mark0(9) -> 9* 1174.98/295.83 g0(9) -> 9* 1174.98/295.83 ok0(9) -> 9* 1174.98/295.83 proper0(9) -> 9* 1174.98/295.83 top0(9) -> 9* 1174.98/295.83 15 -> 43,40 1174.98/295.83 16 -> 37* 1174.98/295.83 17 -> 25* 1174.98/295.83 18 -> 23,20 1174.98/295.83 19 -> 9* 1174.98/295.83 22 -> 9* 1174.98/295.83 23 -> 31* 1174.98/295.83 24 -> 18* 1174.98/295.83 27 -> 32,21 1174.98/295.83 33 -> 32,21 1174.98/295.83 39 -> 26* 1174.98/295.83 42 -> 38* 1174.98/295.83 43 -> 47* 1174.98/295.83 44 -> 41* 1174.98/295.83 48 -> 50* 1174.98/295.83 49 -> 42* 1174.98/295.83 51 -> 58* 1174.98/295.83 52 -> 39* 1174.98/295.83 59 -> 68,61 1174.98/295.83 60 -> 27* 1174.98/295.83 62 -> 21* 1174.98/295.83 68 -> 84* 1174.98/295.83 69 -> 76,71 1174.98/295.83 70 -> 33* 1174.98/295.83 72 -> 21* 1174.98/295.83 76 -> 78* 1174.98/295.83 77 -> 69* 1174.98/295.83 80 -> 79,72 1174.98/295.83 85 -> 79* 1174.98/295.83 problem: 1174.98/295.83 strict: 1174.98/295.83 1174.98/295.83 weak: 1174.98/295.83 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.83 f(ok(X)) -> ok(f(X)) 1174.98/295.83 proper(a()) -> ok(a()) 1174.98/295.83 top(mark(X)) -> top(proper(X)) 1174.98/295.83 top(ok(X)) -> top(active(X)) 1174.98/295.83 active(g(X)) -> g(active(X)) 1174.98/295.83 g(mark(X)) -> mark(g(X)) 1174.98/295.83 proper(f(X)) -> f(proper(X)) 1174.98/295.83 proper(g(X)) -> g(proper(X)) 1174.98/295.83 g(ok(X)) -> ok(g(X)) 1174.98/295.83 Qed 1174.98/295.83 1174.98/295.83 strict: 1174.98/295.83 active(g(X)) -> g(active(X)) 1174.98/295.83 g(mark(X)) -> mark(g(X)) 1174.98/295.83 proper(f(X)) -> f(proper(X)) 1174.98/295.83 proper(g(X)) -> g(proper(X)) 1174.98/295.83 g(ok(X)) -> ok(g(X)) 1174.98/295.83 weak: 1174.98/295.83 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.83 f(ok(X)) -> ok(f(X)) 1174.98/295.83 proper(a()) -> ok(a()) 1174.98/295.83 top(mark(X)) -> top(proper(X)) 1174.98/295.83 top(ok(X)) -> top(active(X)) 1174.98/295.83 Splitting Processor: 1174.98/295.83 strict: 1174.98/295.83 g(mark(X)) -> mark(g(X)) 1174.98/295.83 weak: 1174.98/295.83 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.83 f(ok(X)) -> ok(f(X)) 1174.98/295.83 proper(a()) -> ok(a()) 1174.98/295.83 top(mark(X)) -> top(proper(X)) 1174.98/295.83 top(ok(X)) -> top(active(X)) 1174.98/295.83 active(g(X)) -> g(active(X)) 1174.98/295.83 proper(f(X)) -> f(proper(X)) 1174.98/295.83 proper(g(X)) -> g(proper(X)) 1174.98/295.83 g(ok(X)) -> ok(g(X)) 1174.98/295.83 Splitting Processor: 1174.98/295.83 strict: 1174.98/295.83 proper(f(X)) -> f(proper(X)) 1174.98/295.83 weak: 1174.98/295.83 g(mark(X)) -> mark(g(X)) 1174.98/295.83 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.83 f(ok(X)) -> ok(f(X)) 1174.98/295.83 proper(a()) -> ok(a()) 1174.98/295.83 top(mark(X)) -> top(proper(X)) 1174.98/295.83 top(ok(X)) -> top(active(X)) 1174.98/295.83 active(g(X)) -> g(active(X)) 1174.98/295.83 proper(g(X)) -> g(proper(X)) 1174.98/295.83 g(ok(X)) -> ok(g(X)) 1174.98/295.83 Matrix Interpretation Processor: dim=3 1174.98/295.83 1174.98/295.83 max_matrix: 1174.98/295.83 [1 2 2] 1174.98/295.83 [0 1 3] 1174.98/295.83 [0 0 1] 1174.98/295.83 interpretation: 1174.98/295.83 [1 0 0] [0] 1174.98/295.83 [top](x0) = [0 0 0]x0 + [0] 1174.98/295.83 [0 0 0] [1], 1174.98/295.83 1174.98/295.83 1174.98/295.83 [ok](x0) = x0 1174.98/295.83 , 1174.98/295.83 1174.98/295.83 [1 0 2] 1174.98/295.83 [proper](x0) = [0 1 0]x0 1174.98/295.83 [0 0 1] , 1174.98/295.83 1174.98/295.83 [1 0 2] 1174.98/295.83 [mark](x0) = [0 0 0]x0 1174.98/295.83 [0 0 0] , 1174.98/295.83 1174.98/295.83 [1 0 0] 1174.98/295.83 [g](x0) = [0 0 0]x0 1174.98/295.83 [0 0 1] , 1174.98/295.83 1174.98/295.83 [1 0 0] 1174.98/295.83 [active](x0) = [0 0 0]x0 1174.98/295.83 [0 0 0] , 1174.98/295.83 1174.98/295.83 [1 2 0] [0] 1174.98/295.83 [f](x0) = [0 0 3]x0 + [0] 1174.98/295.83 [0 0 1] [1], 1174.98/295.83 1174.98/295.83 [0] 1174.98/295.83 [a] = [0] 1174.98/295.83 [1] 1174.98/295.83 orientation: 1174.98/295.83 [1 2 2] [2] [1 2 2] [0] 1174.98/295.83 proper(f(X)) = [0 0 3]X + [0] >= [0 0 3]X + [0] = f(proper(X)) 1174.98/295.83 [0 0 1] [1] [0 0 1] [1] 1174.98/295.83 1174.98/295.83 [1 0 2] [1 0 2] 1174.98/295.83 g(mark(X)) = [0 0 0]X >= [0 0 0]X = mark(g(X)) 1174.98/295.83 [0 0 0] [0 0 0] 1174.98/295.83 1174.98/295.83 [6] [6] 1174.98/295.83 active(f(f(a()))) = [0] >= [0] = mark(f(g(f(a())))) 1174.98/295.83 [0] [0] 1174.98/295.83 1174.98/295.83 [1 2 0] [0] [1 2 0] [0] 1174.98/295.83 f(ok(X)) = [0 0 3]X + [0] >= [0 0 3]X + [0] = ok(f(X)) 1174.98/295.83 [0 0 1] [1] [0 0 1] [1] 1174.98/295.83 1174.98/295.83 [2] [0] 1174.98/295.83 proper(a()) = [0] >= [0] = ok(a()) 1174.98/295.83 [1] [1] 1174.98/295.83 1174.98/295.83 [1 0 2] [0] [1 0 2] [0] 1174.98/295.83 top(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = top(proper(X)) 1174.98/295.83 [0 0 0] [1] [0 0 0] [1] 1174.98/295.83 1174.98/295.83 [1 0 0] [0] [1 0 0] [0] 1174.98/295.83 top(ok(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = top(active(X)) 1174.98/295.83 [0 0 0] [1] [0 0 0] [1] 1174.98/295.83 1174.98/295.83 [1 0 0] [1 0 0] 1174.98/295.84 active(g(X)) = [0 0 0]X >= [0 0 0]X = g(active(X)) 1174.98/295.84 [0 0 0] [0 0 0] 1174.98/295.84 1174.98/295.84 [1 0 2] [1 0 2] 1174.98/295.84 proper(g(X)) = [0 0 0]X >= [0 0 0]X = g(proper(X)) 1174.98/295.84 [0 0 1] [0 0 1] 1174.98/295.84 1174.98/295.84 [1 0 0] [1 0 0] 1174.98/295.84 g(ok(X)) = [0 0 0]X >= [0 0 0]X = ok(g(X)) 1174.98/295.84 [0 0 1] [0 0 1] 1174.98/295.84 problem: 1174.98/295.84 strict: 1174.98/295.84 1174.98/295.84 weak: 1174.98/295.84 proper(f(X)) -> f(proper(X)) 1174.98/295.84 g(mark(X)) -> mark(g(X)) 1174.98/295.84 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.84 f(ok(X)) -> ok(f(X)) 1174.98/295.84 proper(a()) -> ok(a()) 1174.98/295.84 top(mark(X)) -> top(proper(X)) 1174.98/295.84 top(ok(X)) -> top(active(X)) 1174.98/295.84 active(g(X)) -> g(active(X)) 1174.98/295.84 proper(g(X)) -> g(proper(X)) 1174.98/295.84 g(ok(X)) -> ok(g(X)) 1174.98/295.84 Qed 1174.98/295.84 1174.98/295.84 strict: 1174.98/295.84 active(g(X)) -> g(active(X)) 1174.98/295.84 proper(g(X)) -> g(proper(X)) 1174.98/295.84 g(ok(X)) -> ok(g(X)) 1174.98/295.84 weak: 1174.98/295.84 proper(f(X)) -> f(proper(X)) 1174.98/295.84 g(mark(X)) -> mark(g(X)) 1174.98/295.84 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.84 f(ok(X)) -> ok(f(X)) 1174.98/295.84 proper(a()) -> ok(a()) 1174.98/295.84 top(mark(X)) -> top(proper(X)) 1174.98/295.84 top(ok(X)) -> top(active(X)) 1174.98/295.84 Splitting Processor: 1174.98/295.84 strict: 1174.98/295.84 proper(g(X)) -> g(proper(X)) 1174.98/295.84 weak: 1174.98/295.84 proper(f(X)) -> f(proper(X)) 1174.98/295.84 g(mark(X)) -> mark(g(X)) 1174.98/295.84 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.84 f(ok(X)) -> ok(f(X)) 1174.98/295.84 proper(a()) -> ok(a()) 1174.98/295.84 top(mark(X)) -> top(proper(X)) 1174.98/295.84 top(ok(X)) -> top(active(X)) 1174.98/295.84 active(g(X)) -> g(active(X)) 1174.98/295.84 g(ok(X)) -> ok(g(X)) 1174.98/295.84 Splitting Processor: 1174.98/295.84 strict: 1174.98/295.84 g(ok(X)) -> ok(g(X)) 1174.98/295.84 weak: 1174.98/295.84 proper(g(X)) -> g(proper(X)) 1174.98/295.84 proper(f(X)) -> f(proper(X)) 1174.98/295.84 g(mark(X)) -> mark(g(X)) 1174.98/295.84 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.84 f(ok(X)) -> ok(f(X)) 1174.98/295.84 proper(a()) -> ok(a()) 1174.98/295.84 top(mark(X)) -> top(proper(X)) 1174.98/295.84 top(ok(X)) -> top(active(X)) 1174.98/295.84 active(g(X)) -> g(active(X)) 1174.98/295.84 Matrix Interpretation Processor: dim=4 1174.98/295.84 1174.98/295.84 max_matrix: 1174.98/295.84 [1 1 1 0] 1174.98/295.84 [0 1 1 1] 1174.98/295.84 [0 0 1 1] 1174.98/295.84 [0 0 0 0] 1174.98/295.84 interpretation: 1174.98/295.84 [1 1 0 0] [0] 1174.98/295.84 [0 0 0 0] [1] 1174.98/295.84 [top](x0) = [0 0 0 1]x0 + [1] 1174.98/295.84 [0 0 0 0] [0], 1174.98/295.84 1174.98/295.84 [1 0 0 0] [0] 1174.98/295.84 [0 1 0 0] [1] 1174.98/295.84 [ok](x0) = [0 0 1 1]x0 + [0] 1174.98/295.84 [0 0 0 0] [0], 1174.98/295.84 1174.98/295.84 [1 1 0 0] [0] 1174.98/295.84 [0 1 0 0] [1] 1174.98/295.84 [proper](x0) = [0 0 1 1]x0 + [0] 1174.98/295.84 [0 0 0 0] [0], 1174.98/295.84 1174.98/295.84 [1 1 0 0] [0] 1174.98/295.84 [0 1 0 0] [1] 1174.98/295.84 [mark](x0) = [0 0 0 0]x0 + [0] 1174.98/295.84 [0 0 0 0] [0], 1174.98/295.84 1174.98/295.84 [1 1 0 0] [0] 1174.98/295.84 [0 1 0 0] [1] 1174.98/295.84 [g](x0) = [0 0 0 0]x0 + [0] 1174.98/295.84 [0 0 0 0] [0], 1174.98/295.84 1174.98/295.84 [1 0 0 0] [1] 1174.98/295.84 [0 1 0 0] [0] 1174.98/295.84 [active](x0) = [0 0 0 0]x0 + [0] 1174.98/295.84 [0 0 0 0] [0], 1174.98/295.84 1174.98/295.84 [1 0 1 0] [0] 1174.98/295.84 [0 1 1 1] [0] 1174.98/295.84 [f](x0) = [0 0 1 1]x0 + [1] 1174.98/295.84 [0 0 0 0] [0], 1174.98/295.84 1174.98/295.84 [0] 1174.98/295.84 [0] 1174.98/295.84 [a] = [0] 1174.98/295.84 [1] 1174.98/295.84 orientation: 1174.98/295.84 [1 1 0 0] [1] [1 1 0 0] [0] 1174.98/295.84 [0 1 0 0] [2] [0 1 0 0] [2] 1174.98/295.84 g(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = ok(g(X)) 1174.98/295.84 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.84 1174.98/295.84 [1 2 0 0] [1] [1 2 0 0] [1] 1174.98/295.84 [0 1 0 0] [2] [0 1 0 0] [2] 1174.98/295.84 proper(g(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = g(proper(X)) 1174.98/295.84 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.84 1174.98/295.84 [1 1 2 1] [0] [1 1 1 1] [0] 1174.98/295.84 [0 1 1 1] [1] [0 1 1 1] [1] 1174.98/295.84 proper(f(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = f(proper(X)) 1174.98/295.84 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.84 1174.98/295.84 [1 2 0 0] [1] [1 2 0 0] [1] 1174.98/295.84 [0 1 0 0] [2] [0 1 0 0] [2] 1174.98/295.84 g(mark(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = mark(g(X)) 1174.98/295.84 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.84 1174.98/295.84 [3] [3] 1174.98/295.84 [3] [3] 1174.98/295.84 active(f(f(a()))) = [0] >= [0] = mark(f(g(f(a())))) 1174.98/295.84 [0] [0] 1174.98/295.84 1174.98/295.84 [1 0 1 1] [0] [1 0 1 0] [0] 1174.98/295.84 [0 1 1 1] [1] [0 1 1 1] [1] 1174.98/295.84 f(ok(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = ok(f(X)) 1174.98/295.84 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.84 1174.98/295.84 [0] [0] 1174.98/295.84 [1] [1] 1174.98/295.84 proper(a()) = [1] >= [1] = ok(a()) 1174.98/295.84 [0] [0] 1174.98/295.84 1174.98/295.84 [1 2 0 0] [1] [1 2 0 0] [1] 1174.98/295.84 [0 0 0 0] [1] [0 0 0 0] [1] 1174.98/295.84 top(mark(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(proper(X)) 1174.98/295.84 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.84 1174.98/295.84 [1 1 0 0] [1] [1 1 0 0] [1] 1174.98/295.84 [0 0 0 0] [1] [0 0 0 0] [1] 1174.98/295.84 top(ok(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(active(X)) 1174.98/295.84 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.84 1174.98/295.84 [1 1 0 0] [1] [1 1 0 0] [1] 1174.98/295.84 [0 1 0 0] [1] [0 1 0 0] [1] 1174.98/295.84 active(g(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = g(active(X)) 1174.98/295.84 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.84 problem: 1174.98/295.84 strict: 1174.98/295.84 1174.98/295.84 weak: 1174.98/295.84 g(ok(X)) -> ok(g(X)) 1174.98/295.84 proper(g(X)) -> g(proper(X)) 1174.98/295.84 proper(f(X)) -> f(proper(X)) 1174.98/295.84 g(mark(X)) -> mark(g(X)) 1174.98/295.84 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.84 f(ok(X)) -> ok(f(X)) 1174.98/295.84 proper(a()) -> ok(a()) 1174.98/295.84 top(mark(X)) -> top(proper(X)) 1174.98/295.84 top(ok(X)) -> top(active(X)) 1174.98/295.84 active(g(X)) -> g(active(X)) 1174.98/295.84 Qed 1174.98/295.84 1174.98/295.84 strict: 1174.98/295.84 active(g(X)) -> g(active(X)) 1174.98/295.84 weak: 1174.98/295.84 g(ok(X)) -> ok(g(X)) 1174.98/295.84 proper(g(X)) -> g(proper(X)) 1174.98/295.84 proper(f(X)) -> f(proper(X)) 1174.98/295.84 g(mark(X)) -> mark(g(X)) 1174.98/295.84 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.84 f(ok(X)) -> ok(f(X)) 1174.98/295.84 proper(a()) -> ok(a()) 1174.98/295.84 top(mark(X)) -> top(proper(X)) 1174.98/295.84 top(ok(X)) -> top(active(X)) 1174.98/295.84 Matrix Interpretation Processor: dim=4 1174.98/295.84 1174.98/295.84 max_matrix: 1174.98/295.84 [1 1 1 1] 1174.98/295.84 [0 1 0 0] 1174.98/295.84 [0 0 1 1] 1174.98/295.84 [0 0 0 1] 1174.98/295.84 interpretation: 1174.98/295.84 [1 0 0 0] [0] 1174.98/295.84 [0 0 0 0] [0] 1174.98/295.84 [top](x0) = [0 0 0 0]x0 + [0] 1174.98/295.84 [0 0 0 0] [1], 1174.98/295.84 1174.98/295.84 [1 1 0 0] [0] 1174.98/295.84 [0 1 0 0] [0] 1174.98/295.84 [ok](x0) = [0 0 1 0]x0 + [1] 1174.98/295.84 [0 0 0 1] [0], 1174.98/295.84 1174.98/295.84 [1 1 0 0] [0] 1174.98/295.85 [0 1 0 0] [0] 1174.98/295.85 [proper](x0) = [0 0 1 0]x0 + [1] 1174.98/295.85 [0 0 0 1] [0], 1174.98/295.85 1174.98/295.85 [1 1 0 0] [0] 1174.98/295.85 [0 0 0 0] [0] 1174.98/295.85 [mark](x0) = [0 0 1 0]x0 + [1] 1174.98/295.85 [0 0 0 0] [0], 1174.98/295.85 1174.98/295.85 [1 0 1 0] [0] 1174.98/295.85 [0 1 0 0] [1] 1174.98/295.85 [g](x0) = [0 0 1 0]x0 + [0] 1174.98/295.85 [0 0 0 0] [0], 1174.98/295.85 1174.98/295.85 [1 1 0 0] 1174.98/295.85 [0 1 0 0] 1174.98/295.85 [active](x0) = [0 0 1 0]x0 1174.98/295.85 [0 0 0 0] , 1174.98/295.85 1174.98/295.85 [1 0 0 1] [0] 1174.98/295.85 [0 1 0 0] [0] 1174.98/295.85 [f](x0) = [0 0 1 1]x0 + [0] 1174.98/295.85 [0 0 0 0] [1], 1174.98/295.85 1174.98/295.85 [1] 1174.98/295.85 [0] 1174.98/295.85 [a] = [0] 1174.98/295.85 [0] 1174.98/295.85 orientation: 1174.98/295.85 [1 1 1 0] [1] [1 1 1 0] [0] 1174.98/295.85 [0 1 0 0] [1] [0 1 0 0] [1] 1174.98/295.85 active(g(X)) = [0 0 1 0]X + [0] >= [0 0 1 0]X + [0] = g(active(X)) 1174.98/295.85 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.85 1174.98/295.85 [1 1 1 0] [1] [1 1 1 0] [1] 1174.98/295.85 [0 1 0 0] [1] [0 1 0 0] [1] 1174.98/295.85 g(ok(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = ok(g(X)) 1174.98/295.85 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.85 1174.98/295.85 [1 1 1 0] [1] [1 1 1 0] [1] 1174.98/295.85 [0 1 0 0] [1] [0 1 0 0] [1] 1174.98/295.85 proper(g(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = g(proper(X)) 1174.98/295.85 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.85 1174.98/295.85 [1 1 0 1] [0] [1 1 0 1] [0] 1174.98/295.85 [0 1 0 0] [0] [0 1 0 0] [0] 1174.98/295.85 proper(f(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = f(proper(X)) 1174.98/295.85 [0 0 0 0] [1] [0 0 0 0] [1] 1174.98/295.85 1174.98/295.85 [1 1 1 0] [1] [1 1 1 0] [1] 1174.98/295.85 [0 0 0 0] [1] [0 0 0 0] [0] 1174.98/295.85 g(mark(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = mark(g(X)) 1174.98/295.85 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.85 1174.98/295.85 [2] [2] 1174.98/295.85 [0] [0] 1174.98/295.85 active(f(f(a()))) = [1] >= [1] = mark(f(g(f(a())))) 1174.98/295.85 [0] [0] 1174.98/295.85 1174.98/295.85 [1 1 0 1] [0] [1 1 0 1] [0] 1174.98/295.85 [0 1 0 0] [0] [0 1 0 0] [0] 1174.98/295.85 f(ok(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = ok(f(X)) 1174.98/295.85 [0 0 0 0] [1] [0 0 0 0] [1] 1174.98/295.85 1174.98/295.85 [1] [1] 1174.98/295.85 [0] [0] 1174.98/295.85 proper(a()) = [1] >= [1] = ok(a()) 1174.98/295.85 [0] [0] 1174.98/295.85 1174.98/295.85 [1 1 0 0] [0] [1 1 0 0] [0] 1174.98/295.85 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.85 top(mark(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = top(proper(X)) 1174.98/295.85 [0 0 0 0] [1] [0 0 0 0] [1] 1174.98/295.85 1174.98/295.85 [1 1 0 0] [0] [1 1 0 0] [0] 1174.98/295.85 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.85 top(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = top(active(X)) 1174.98/295.85 [0 0 0 0] [1] [0 0 0 0] [1] 1174.98/295.85 problem: 1174.98/295.85 strict: 1174.98/295.85 1174.98/295.85 weak: 1174.98/295.85 active(g(X)) -> g(active(X)) 1174.98/295.85 g(ok(X)) -> ok(g(X)) 1174.98/295.85 proper(g(X)) -> g(proper(X)) 1174.98/295.86 proper(f(X)) -> f(proper(X)) 1174.98/295.86 g(mark(X)) -> mark(g(X)) 1174.98/295.86 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.86 f(ok(X)) -> ok(f(X)) 1174.98/295.86 proper(a()) -> ok(a()) 1174.98/295.86 top(mark(X)) -> top(proper(X)) 1174.98/295.86 top(ok(X)) -> top(active(X)) 1174.98/295.86 Qed 1174.98/295.86 1174.98/295.86 strict: 1174.98/295.86 active(g(X)) -> g(active(X)) 1174.98/295.86 g(ok(X)) -> ok(g(X)) 1174.98/295.86 weak: 1174.98/295.86 proper(g(X)) -> g(proper(X)) 1174.98/295.86 proper(f(X)) -> f(proper(X)) 1174.98/295.86 g(mark(X)) -> mark(g(X)) 1174.98/295.86 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.86 f(ok(X)) -> ok(f(X)) 1174.98/295.86 proper(a()) -> ok(a()) 1174.98/295.86 top(mark(X)) -> top(proper(X)) 1174.98/295.86 top(ok(X)) -> top(active(X)) 1174.98/295.86 Matrix Interpretation Processor: dim=3 1174.98/295.86 1174.98/295.86 max_matrix: 1174.98/295.86 [1 2 2] 1174.98/295.86 [0 1 2] 1174.98/295.86 [0 0 1] 1174.98/295.86 interpretation: 1174.98/295.86 [1 0 0] 1174.98/295.86 [top](x0) = [0 0 0]x0 1174.98/295.86 [0 0 0] , 1174.98/295.86 1174.98/295.86 1174.98/295.86 [ok](x0) = x0 1174.98/295.86 , 1174.98/295.86 1174.98/295.86 [1 2 0] 1174.98/295.86 [proper](x0) = [0 1 0]x0 1174.98/295.86 [0 0 1] , 1174.98/295.86 1174.98/295.86 [1 2 0] [0] 1174.98/295.86 [mark](x0) = [0 1 0]x0 + [1] 1174.98/295.86 [0 0 0] [0], 1174.98/295.86 1174.98/295.86 [1 2 0] [0] 1174.98/295.86 [g](x0) = [0 1 0]x0 + [1] 1174.98/295.86 [0 0 0] [0], 1174.98/295.86 1174.98/295.86 [1 0 0] 1174.98/295.86 [active](x0) = [0 1 0]x0 1174.98/295.86 [0 0 0] , 1174.98/295.86 1174.98/295.86 [1 0 2] [1] 1174.98/295.86 [f](x0) = [0 1 2]x0 + [0] 1174.98/295.86 [0 0 0] [1], 1174.98/295.86 1174.98/295.86 [1] 1174.98/295.86 [a] = [0] 1174.98/295.86 [0] 1174.98/295.86 orientation: 1174.98/295.86 [1 4 0] [2] [1 4 0] [0] 1174.98/295.86 proper(g(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = g(proper(X)) 1174.98/295.86 [0 0 0] [0] [0 0 0] [0] 1174.98/295.86 1174.98/295.86 [1 2 6] [1] [1 2 2] [1] 1174.98/295.86 proper(f(X)) = [0 1 2]X + [0] >= [0 1 2]X + [0] = f(proper(X)) 1174.98/295.86 [0 0 0] [1] [0 0 0] [1] 1174.98/295.86 1174.98/295.86 [1 4 0] [2] [1 4 0] [2] 1174.98/295.86 g(mark(X)) = [0 1 0]X + [2] >= [0 1 0]X + [2] = mark(g(X)) 1174.98/295.86 [0 0 0] [0] [0 0 0] [0] 1174.98/295.86 1174.98/295.86 [5] [5] 1174.98/295.86 active(f(f(a()))) = [2] >= [2] = mark(f(g(f(a())))) 1174.98/295.86 [0] [0] 1174.98/295.86 1174.98/295.86 [1 0 2] [1] [1 0 2] [1] 1174.98/295.86 f(ok(X)) = [0 1 2]X + [0] >= [0 1 2]X + [0] = ok(f(X)) 1174.98/295.86 [0 0 0] [1] [0 0 0] [1] 1174.98/295.86 1174.98/295.86 [1] [1] 1174.98/295.86 proper(a()) = [0] >= [0] = ok(a()) 1174.98/295.86 [0] [0] 1174.98/295.86 1174.98/295.86 [1 2 0] [1 2 0] 1174.98/295.86 top(mark(X)) = [0 0 0]X >= [0 0 0]X = top(proper(X)) 1174.98/295.86 [0 0 0] [0 0 0] 1174.98/295.86 1174.98/295.86 [1 0 0] [1 0 0] 1174.98/295.86 top(ok(X)) = [0 0 0]X >= [0 0 0]X = top(active(X)) 1174.98/295.86 [0 0 0] [0 0 0] 1174.98/295.86 1174.98/295.86 [1 2 0] [0] [1 2 0] [0] 1174.98/295.86 active(g(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = g(active(X)) 1174.98/295.86 [0 0 0] [0] [0 0 0] [0] 1174.98/295.86 1174.98/295.86 [1 2 0] [0] [1 2 0] [0] 1174.98/295.86 g(ok(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = ok(g(X)) 1174.98/295.86 [0 0 0] [0] [0 0 0] [0] 1174.98/295.86 problem: 1174.98/295.86 strict: 1174.98/295.86 1174.98/295.86 weak: 1174.98/295.86 proper(g(X)) -> g(proper(X)) 1174.98/295.86 proper(f(X)) -> f(proper(X)) 1174.98/295.86 g(mark(X)) -> mark(g(X)) 1174.98/295.86 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.86 f(ok(X)) -> ok(f(X)) 1174.98/295.86 proper(a()) -> ok(a()) 1174.98/295.86 top(mark(X)) -> top(proper(X)) 1174.98/295.86 top(ok(X)) -> top(active(X)) 1174.98/295.86 active(g(X)) -> g(active(X)) 1174.98/295.86 g(ok(X)) -> ok(g(X)) 1174.98/295.86 Qed 1174.98/295.86 1174.98/295.86 strict: 1174.98/295.86 active(g(X)) -> g(active(X)) 1174.98/295.86 proper(f(X)) -> f(proper(X)) 1174.98/295.86 proper(g(X)) -> g(proper(X)) 1174.98/295.86 g(ok(X)) -> ok(g(X)) 1174.98/295.86 weak: 1174.98/295.86 g(mark(X)) -> mark(g(X)) 1174.98/295.86 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.86 f(ok(X)) -> ok(f(X)) 1174.98/295.86 proper(a()) -> ok(a()) 1174.98/295.86 top(mark(X)) -> top(proper(X)) 1174.98/295.86 top(ok(X)) -> top(active(X)) 1174.98/295.86 Matrix Interpretation Processor: dim=4 1174.98/295.86 1174.98/295.86 max_matrix: 1174.98/295.86 [1 1 1 1] 1174.98/295.86 [0 1 1 1] 1174.98/295.86 [0 0 1 1] 1174.98/295.86 [0 0 0 0] 1174.98/295.86 interpretation: 1174.98/295.86 [1 0 0 0] 1174.98/295.86 [0 1 0 0] 1174.98/295.86 [top](x0) = [0 0 0 0]x0 1174.98/295.86 [0 0 0 0] , 1174.98/295.86 1174.98/295.86 [1 0 0 0] 1174.98/295.86 [0 1 0 0] 1174.98/295.86 [ok](x0) = [0 0 1 1]x0 1174.98/295.86 [0 0 0 0] , 1174.98/295.86 1174.98/295.86 [1 0 0 0] 1174.98/295.86 [0 1 0 0] 1174.98/295.86 [proper](x0) = [0 0 1 1]x0 1174.98/295.86 [0 0 0 0] , 1174.98/295.86 1174.98/295.86 [1 0 0 0] [1] 1174.98/295.86 [0 1 0 0] [1] 1174.98/295.86 [mark](x0) = [0 0 0 0]x0 + [0] 1174.98/295.86 [0 0 0 0] [0], 1174.98/295.86 1174.98/295.86 [1 1 0 0] 1174.98/295.86 [0 1 0 0] 1174.98/295.86 [g](x0) = [0 0 0 0]x0 1174.98/295.86 [0 0 0 0] , 1174.98/295.86 1174.98/295.86 [1 0 0 0] 1174.98/295.86 [0 1 0 0] 1174.98/295.86 [active](x0) = [0 0 0 0]x0 1174.98/295.86 [0 0 0 0] , 1174.98/295.86 1174.98/295.86 [1 0 1 1] [0] 1174.98/295.86 [0 0 1 1] [0] 1174.98/295.86 [f](x0) = [0 0 1 1]x0 + [1] 1174.98/295.86 [0 0 0 0] [0], 1174.98/295.86 1174.98/295.86 [0] 1174.98/295.86 [0] 1174.98/295.86 [a] = [0] 1174.98/295.86 [1] 1174.98/295.86 orientation: 1174.98/295.86 [1 1 0 0] [2] [1 1 0 0] [1] 1174.98/295.86 [0 1 0 0] [1] [0 1 0 0] [1] 1174.98/295.86 g(mark(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = mark(g(X)) 1174.98/295.86 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.86 1174.98/295.86 [3] [3] 1174.98/295.86 [2] [1] 1174.98/295.86 active(f(f(a()))) = [0] >= [0] = mark(f(g(f(a())))) 1174.98/295.86 [0] [0] 1174.98/295.86 1174.98/295.86 [1 0 1 1] [0] [1 0 1 1] [0] 1174.98/295.86 [0 0 1 1] [0] [0 0 1 1] [0] 1174.98/295.86 f(ok(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = ok(f(X)) 1174.98/295.86 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.86 1174.98/295.86 [0] [0] 1174.98/295.86 [0] [0] 1174.98/295.86 proper(a()) = [1] >= [1] = ok(a()) 1174.98/295.86 [0] [0] 1174.98/295.86 1174.98/295.86 [1 0 0 0] [1] [1 0 0 0] 1174.98/295.86 [0 1 0 0] [1] [0 1 0 0] 1174.98/295.86 top(mark(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X = top(proper(X)) 1174.98/295.86 [0 0 0 0] [0] [0 0 0 0] 1174.98/295.86 1174.98/295.86 [1 0 0 0] [1 0 0 0] 1174.98/295.86 [0 1 0 0] [0 1 0 0] 1174.98/295.86 top(ok(X)) = [0 0 0 0]X >= [0 0 0 0]X = top(active(X)) 1174.98/295.86 [0 0 0 0] [0 0 0 0] 1174.98/295.86 1174.98/295.86 [1 1 0 0] [1 1 0 0] 1174.98/295.86 [0 1 0 0] [0 1 0 0] 1174.98/295.86 active(g(X)) = [0 0 0 0]X >= [0 0 0 0]X = g(active(X)) 1174.98/295.86 [0 0 0 0] [0 0 0 0] 1174.98/295.86 1174.98/295.86 [1 0 1 1] [0] [1 0 1 1] [0] 1174.98/295.86 [0 0 1 1] [0] [0 0 1 1] [0] 1174.98/295.86 proper(f(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = f(proper(X)) 1174.98/295.86 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.86 1174.98/295.86 [1 1 0 0] [1 1 0 0] 1174.98/295.86 [0 1 0 0] [0 1 0 0] 1174.98/295.86 proper(g(X)) = [0 0 0 0]X >= [0 0 0 0]X = g(proper(X)) 1174.98/295.87 [0 0 0 0] [0 0 0 0] 1174.98/295.87 1174.98/295.87 [1 1 0 0] [1 1 0 0] 1174.98/295.87 [0 1 0 0] [0 1 0 0] 1174.98/295.87 g(ok(X)) = [0 0 0 0]X >= [0 0 0 0]X = ok(g(X)) 1174.98/295.87 [0 0 0 0] [0 0 0 0] 1174.98/295.87 problem: 1174.98/295.87 strict: 1174.98/295.87 1174.98/295.87 weak: 1174.98/295.87 g(mark(X)) -> mark(g(X)) 1174.98/295.87 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.87 f(ok(X)) -> ok(f(X)) 1174.98/295.87 proper(a()) -> ok(a()) 1174.98/295.87 top(mark(X)) -> top(proper(X)) 1174.98/295.87 top(ok(X)) -> top(active(X)) 1174.98/295.87 active(g(X)) -> g(active(X)) 1174.98/295.87 proper(f(X)) -> f(proper(X)) 1174.98/295.87 proper(g(X)) -> g(proper(X)) 1174.98/295.87 g(ok(X)) -> ok(g(X)) 1174.98/295.87 Qed 1174.98/295.87 1174.98/295.87 strict: 1174.98/295.87 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.87 active(g(X)) -> g(active(X)) 1174.98/295.87 g(mark(X)) -> mark(g(X)) 1174.98/295.87 proper(f(X)) -> f(proper(X)) 1174.98/295.87 proper(g(X)) -> g(proper(X)) 1174.98/295.87 g(ok(X)) -> ok(g(X)) 1174.98/295.87 weak: 1174.98/295.87 f(ok(X)) -> ok(f(X)) 1174.98/295.87 proper(a()) -> ok(a()) 1174.98/295.87 top(mark(X)) -> top(proper(X)) 1174.98/295.87 top(ok(X)) -> top(active(X)) 1174.98/295.87 Matrix Interpretation Processor: dim=4 1174.98/295.87 1174.98/295.87 max_matrix: 1174.98/295.87 [1 2 2 0] 1174.98/295.87 [0 1 2 2] 1174.98/295.87 [0 0 1 1] 1174.98/295.87 [0 0 0 0] 1174.98/295.87 interpretation: 1174.98/295.87 [1 2 2 0] [0] 1174.98/295.87 [0 0 0 2] [3] 1174.98/295.87 [top](x0) = [0 0 0 0]x0 + [1] 1174.98/295.87 [0 0 0 0] [2], 1174.98/295.87 1174.98/295.87 [1 0 0 0] [0] 1174.98/295.87 [0 1 0 0] [1] 1174.98/295.87 [ok](x0) = [0 0 1 0]x0 + [0] 1174.98/295.87 [0 0 0 0] [0], 1174.98/295.87 1174.98/295.87 [1 1 1 0] [0] 1174.98/295.87 [0 1 0 0] [1] 1174.98/295.87 [proper](x0) = [0 0 1 0]x0 + [0] 1174.98/295.87 [0 0 0 0] [0], 1174.98/295.87 1174.98/295.87 [1 1 1 0] [0] 1174.98/295.87 [0 1 1 0] [1] 1174.98/295.87 [mark](x0) = [0 0 0 1]x0 + [0] 1174.98/295.87 [0 0 0 0] [0], 1174.98/295.87 1174.98/295.87 [1 0 0 0] 1174.98/295.87 [0 1 1 0] 1174.98/295.87 [g](x0) = [0 0 0 0]x0 1174.98/295.87 [0 0 0 0] , 1174.98/295.87 1174.98/295.87 [1 0 0 0] [2] 1174.98/295.87 [0 1 1 0] [0] 1174.98/295.87 [active](x0) = [0 0 0 0]x0 + [0] 1174.98/295.87 [0 0 0 0] [0], 1174.98/295.87 1174.98/295.87 [1 1 1 0] [0] 1174.98/295.87 [0 1 2 0] [0] 1174.98/295.87 [f](x0) = [0 0 0 0]x0 + [1] 1174.98/295.87 [0 0 0 0] [0], 1174.98/295.87 1174.98/295.87 [0] 1174.98/295.87 [0] 1174.98/295.87 [a] = [0] 1174.98/295.87 [0] 1174.98/295.87 orientation: 1174.98/295.87 [1 1 1 0] [1] [1 1 1 0] [0] 1174.98/295.87 [0 1 2 0] [1] [0 1 2 0] [1] 1174.98/295.87 f(ok(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = ok(f(X)) 1174.98/295.87 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.87 1174.98/295.87 [0] [0] 1174.98/295.87 [1] [1] 1174.98/295.87 proper(a()) = [0] >= [0] = ok(a()) 1174.98/295.87 [0] [0] 1174.98/295.87 1174.98/295.87 [1 3 3 2] [2] [1 3 3 0] [2] 1174.98/295.87 [0 0 0 0] [3] [0 0 0 0] [3] 1174.98/295.87 top(mark(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(proper(X)) 1174.98/295.87 [0 0 0 0] [2] [0 0 0 0] [2] 1174.98/295.87 1174.98/295.87 [1 2 2 0] [2] [1 2 2 0] [2] 1174.98/295.87 [0 0 0 0] [3] [0 0 0 0] [3] 1174.98/295.87 top(ok(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(active(X)) 1174.98/295.87 [0 0 0 0] [2] [0 0 0 0] [2] 1174.98/295.87 1174.98/295.87 [3] [3] 1174.98/295.87 [3] [3] 1174.98/295.87 active(f(f(a()))) = [0] >= [0] = mark(f(g(f(a())))) 1174.98/295.87 [0] [0] 1174.98/295.87 1174.98/295.87 [1 0 0 0] [2] [1 0 0 0] [2] 1174.98/295.87 [0 1 1 0] [0] [0 1 1 0] [0] 1174.98/295.87 active(g(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = g(active(X)) 1174.98/295.87 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.87 1174.98/295.87 [1 1 1 0] [0] [1 1 1 0] [0] 1174.98/295.87 [0 1 1 1] [1] [0 1 1 0] [1] 1174.98/295.87 g(mark(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = mark(g(X)) 1174.98/295.87 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.87 1174.98/295.87 [1 2 3 0] [1] [1 2 2 0] [1] 1174.98/295.87 [0 1 2 0] [1] [0 1 2 0] [1] 1174.98/295.87 proper(f(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = f(proper(X)) 1174.98/295.87 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.87 1174.98/295.87 [1 1 1 0] [0] [1 1 1 0] [0] 1174.98/295.87 [0 1 1 0] [1] [0 1 1 0] [1] 1174.98/295.87 proper(g(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = g(proper(X)) 1174.98/295.87 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.87 1174.98/295.87 [1 0 0 0] [0] [1 0 0 0] [0] 1174.98/295.87 [0 1 1 0] [1] [0 1 1 0] [1] 1174.98/295.87 g(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = ok(g(X)) 1174.98/295.87 [0 0 0 0] [0] [0 0 0 0] [0] 1174.98/295.87 problem: 1174.98/295.87 strict: 1174.98/295.87 1174.98/295.87 weak: 1174.98/295.87 f(ok(X)) -> ok(f(X)) 1174.98/295.87 proper(a()) -> ok(a()) 1174.98/295.87 top(mark(X)) -> top(proper(X)) 1174.98/295.87 top(ok(X)) -> top(active(X)) 1174.98/295.87 active(f(f(a()))) -> mark(f(g(f(a())))) 1174.98/295.87 active(g(X)) -> g(active(X)) 1174.98/295.87 g(mark(X)) -> mark(g(X)) 1174.98/295.87 proper(f(X)) -> f(proper(X)) 1174.98/295.87 proper(g(X)) -> g(proper(X)) 1174.98/295.87 g(ok(X)) -> ok(g(X)) 1174.98/295.87 Qed 1174.98/295.88 EOF