YES(?,O(n^2)) 243.91/87.64 YES(?,O(n^2)) 243.91/87.65 243.91/87.65 Problem: 243.91/87.65 active(g(X)) -> mark(h(X)) 243.91/87.65 active(c()) -> mark(d()) 243.91/87.65 active(h(d())) -> mark(g(c())) 243.91/87.65 proper(g(X)) -> g(proper(X)) 243.91/87.65 proper(h(X)) -> h(proper(X)) 243.91/87.65 proper(c()) -> ok(c()) 243.91/87.65 proper(d()) -> ok(d()) 243.91/87.65 g(ok(X)) -> ok(g(X)) 243.91/87.65 h(ok(X)) -> ok(h(X)) 243.91/87.65 top(mark(X)) -> top(proper(X)) 243.91/87.65 top(ok(X)) -> top(active(X)) 243.91/87.65 243.91/87.65 Proof: 243.91/87.65 Complexity Transformation Processor: 243.91/87.65 strict: 243.91/87.65 active(g(X)) -> mark(h(X)) 243.91/87.65 active(c()) -> mark(d()) 243.91/87.65 active(h(d())) -> mark(g(c())) 243.91/87.65 proper(g(X)) -> g(proper(X)) 243.91/87.65 proper(h(X)) -> h(proper(X)) 243.91/87.65 proper(c()) -> ok(c()) 243.91/87.65 proper(d()) -> ok(d()) 243.91/87.65 g(ok(X)) -> ok(g(X)) 243.91/87.65 h(ok(X)) -> ok(h(X)) 243.91/87.65 top(mark(X)) -> top(proper(X)) 243.91/87.65 top(ok(X)) -> top(active(X)) 243.91/87.65 weak: 243.91/87.65 243.91/87.65 Matrix Interpretation Processor: dim=1 243.91/87.65 243.91/87.65 max_matrix: 243.91/87.65 1 243.91/87.65 interpretation: 243.91/87.65 [top](x0) = x0 + 23, 243.91/87.65 243.91/87.65 [ok](x0) = x0 + 20, 243.91/87.65 243.91/87.65 [proper](x0) = x0 + 9, 243.91/87.65 243.91/87.65 [d] = 16, 243.91/87.65 243.91/87.65 [c] = 18, 243.91/87.65 243.91/87.65 [mark](x0) = x0 + 10, 243.91/87.65 243.91/87.65 [h](x0) = x0 + 16, 243.91/87.65 243.91/87.65 [active](x0) = x0 + 26, 243.91/87.65 243.91/87.65 [g](x0) = x0 + 4 243.91/87.65 orientation: 243.91/87.65 active(g(X)) = X + 30 >= X + 26 = mark(h(X)) 243.91/87.65 243.91/87.65 active(c()) = 44 >= 26 = mark(d()) 243.91/87.65 243.91/87.65 active(h(d())) = 58 >= 32 = mark(g(c())) 243.91/87.65 243.91/87.65 proper(g(X)) = X + 13 >= X + 13 = g(proper(X)) 243.91/87.65 243.91/87.65 proper(h(X)) = X + 25 >= X + 25 = h(proper(X)) 243.91/87.65 243.91/87.65 proper(c()) = 27 >= 38 = ok(c()) 243.91/87.65 243.91/87.65 proper(d()) = 25 >= 36 = ok(d()) 243.91/87.65 243.91/87.65 g(ok(X)) = X + 24 >= X + 24 = ok(g(X)) 243.91/87.65 243.91/87.65 h(ok(X)) = X + 36 >= X + 36 = ok(h(X)) 243.91/87.65 243.91/87.65 top(mark(X)) = X + 33 >= X + 32 = top(proper(X)) 243.91/87.65 243.91/87.65 top(ok(X)) = X + 43 >= X + 49 = top(active(X)) 243.91/87.65 problem: 243.91/87.65 strict: 243.91/87.65 proper(g(X)) -> g(proper(X)) 243.91/87.65 proper(h(X)) -> h(proper(X)) 243.91/87.65 proper(c()) -> ok(c()) 243.91/87.65 proper(d()) -> ok(d()) 243.91/87.65 g(ok(X)) -> ok(g(X)) 243.91/87.65 h(ok(X)) -> ok(h(X)) 243.91/87.65 top(ok(X)) -> top(active(X)) 243.91/87.65 weak: 243.91/87.65 active(g(X)) -> mark(h(X)) 243.91/87.65 active(c()) -> mark(d()) 243.91/87.65 active(h(d())) -> mark(g(c())) 243.91/87.65 top(mark(X)) -> top(proper(X)) 243.91/87.65 Matrix Interpretation Processor: dim=1 243.91/87.65 243.91/87.65 max_matrix: 243.91/87.65 1 243.91/87.65 interpretation: 243.91/87.65 [top](x0) = x0 + 6, 243.91/87.65 243.91/87.65 [ok](x0) = x0 + 1, 243.91/87.65 243.91/87.65 [proper](x0) = x0, 243.91/87.65 243.91/87.65 [d] = 5, 243.91/87.65 243.91/87.65 [c] = 5, 243.91/87.65 243.91/87.65 [mark](x0) = x0, 243.91/87.65 243.91/87.65 [h](x0) = x0 + 13, 243.91/87.65 243.91/87.65 [active](x0) = x0, 243.91/87.65 243.91/87.65 [g](x0) = x0 + 13 243.91/87.65 orientation: 243.91/87.65 proper(g(X)) = X + 13 >= X + 13 = g(proper(X)) 243.91/87.65 243.91/87.65 proper(h(X)) = X + 13 >= X + 13 = h(proper(X)) 243.91/87.65 243.91/87.65 proper(c()) = 5 >= 6 = ok(c()) 243.91/87.65 243.91/87.65 proper(d()) = 5 >= 6 = ok(d()) 243.91/87.65 243.91/87.65 g(ok(X)) = X + 14 >= X + 14 = ok(g(X)) 243.91/87.65 243.91/87.65 h(ok(X)) = X + 14 >= X + 14 = ok(h(X)) 243.91/87.65 243.91/87.65 top(ok(X)) = X + 7 >= X + 6 = top(active(X)) 243.91/87.65 243.91/87.65 active(g(X)) = X + 13 >= X + 13 = mark(h(X)) 243.91/87.65 243.91/87.65 active(c()) = 5 >= 5 = mark(d()) 243.91/87.65 243.91/87.65 active(h(d())) = 18 >= 18 = mark(g(c())) 243.91/87.65 243.91/87.65 top(mark(X)) = X + 6 >= X + 6 = top(proper(X)) 243.91/87.65 problem: 243.91/87.65 strict: 243.91/87.65 proper(g(X)) -> g(proper(X)) 243.91/87.65 proper(h(X)) -> h(proper(X)) 243.91/87.65 proper(c()) -> ok(c()) 243.91/87.65 proper(d()) -> ok(d()) 243.91/87.65 g(ok(X)) -> ok(g(X)) 243.91/87.65 h(ok(X)) -> ok(h(X)) 243.91/87.65 weak: 243.91/87.65 top(ok(X)) -> top(active(X)) 243.91/87.65 active(g(X)) -> mark(h(X)) 243.91/87.65 active(c()) -> mark(d()) 243.91/87.65 active(h(d())) -> mark(g(c())) 243.91/87.65 top(mark(X)) -> top(proper(X)) 243.91/87.65 Splitting Processor: 243.91/87.65 strict: 243.91/87.65 proper(d()) -> ok(d()) 243.91/87.65 weak: 243.91/87.65 top(ok(X)) -> top(active(X)) 243.91/87.65 active(g(X)) -> mark(h(X)) 243.91/87.65 active(c()) -> mark(d()) 243.91/87.65 active(h(d())) -> mark(g(c())) 243.91/87.65 top(mark(X)) -> top(proper(X)) 243.91/87.65 proper(g(X)) -> g(proper(X)) 243.91/87.65 proper(h(X)) -> h(proper(X)) 243.91/87.65 proper(c()) -> ok(c()) 243.91/87.65 g(ok(X)) -> ok(g(X)) 243.91/87.65 h(ok(X)) -> ok(h(X)) 243.91/87.65 Bounds Processor: 243.91/87.65 bound: 2 243.91/87.65 enrichment: match 243.91/87.65 automaton: 243.91/87.65 final states: {10} 243.91/87.65 transitions: 243.91/87.65 ok1(57) -> 58* 243.91/87.65 ok1(79) -> 80* 243.91/87.65 ok1(13) -> 14* 243.91/87.65 ok1(155) -> 156* 243.91/87.65 c1() -> 28* 243.91/87.65 top1(16) -> 17* 243.91/87.65 active1(15) -> 16* 243.91/87.65 active1(157) -> 158* 243.91/87.65 active1(89) -> 90* 243.91/87.65 g1(21) -> 22* 243.91/87.65 g1(78) -> 79* 243.91/87.65 g1(48) -> 49* 243.91/87.65 g1(33) -> 34* 243.91/87.65 g1(28) -> 29* 243.91/87.65 h1(25) -> 26* 243.91/87.65 h1(39) -> 40* 243.91/87.65 h1(136) -> 137* 243.91/87.65 h1(116) -> 117* 243.91/87.65 h1(51) -> 52* 243.91/87.65 h1(23) -> 24* 243.91/87.65 mark1(117) -> 118* 243.91/87.65 mark1(26) -> 27* 243.91/87.65 d1() -> 13* 243.91/87.65 proper1(50) -> 51* 243.91/87.65 proper1(30) -> 31* 243.91/87.65 proper1(32) -> 33* 243.91/87.65 proper1(38) -> 39* 243.91/87.65 proper1(135) -> 136* 243.91/87.65 proper1(125) -> 126* 243.91/87.65 ok2(82) -> 83* 243.91/87.65 ok2(64) -> 65* 243.91/87.65 ok2(41) -> 42* 243.91/87.65 ok2(148) -> 149* 243.91/87.65 ok2(175) -> 176* 243.91/87.65 ok2(140) -> 141* 243.91/87.65 proper0(10) -> 10* 243.91/87.65 c2() -> 96* 243.91/87.65 c0() -> 10* 243.91/87.65 h2(159) -> 160* 243.91/87.65 h2(114) -> 115* 243.91/87.65 h2(171) -> 172* 243.91/87.65 h2(108) -> 109* 243.91/87.65 h2(63) -> 64* 243.91/87.65 ok0(10) -> 10* 243.91/87.65 top2(67) -> 68* 243.91/87.65 h0(10) -> 10* 243.91/87.65 active2(177) -> 178* 243.91/87.65 active2(66) -> 67* 243.91/87.65 active2(150) -> 151* 243.91/87.65 g0(10) -> 10* 243.91/87.65 g2(147) -> 148* 243.91/87.65 g2(99) -> 100* 243.91/87.65 g2(106) -> 107* 243.91/87.65 g2(96) -> 97* 243.91/87.65 g2(81) -> 82* 243.91/87.65 g2(133) -> 134* 243.91/87.65 d0() -> 10* 243.91/87.65 d2() -> 41* 243.91/87.65 top0(10) -> 10* 243.91/87.65 mark2(97) -> 98* 243.91/87.65 mark2(160) -> 161* 243.91/87.65 active0(10) -> 10* 243.91/87.65 proper2(162) -> 163* 243.91/87.65 proper2(132) -> 133* 243.91/87.65 proper2(123) -> 124* 243.91/87.65 proper2(170) -> 171* 243.91/87.65 mark0(10) -> 10* 243.91/87.65 13 -> 23,21,15 243.91/87.65 14 -> 10* 243.91/87.65 17 -> 10* 243.91/87.65 21 -> 25* 243.91/87.65 22 -> 13* 243.91/87.65 23 -> 50* 243.91/87.65 24 -> 13* 243.91/87.65 25 -> 38* 243.91/87.65 26 -> 30* 243.91/87.65 27 -> 16* 243.91/87.65 28 -> 57,32 243.91/87.65 29 -> 26* 243.91/87.65 31 -> 16* 243.91/87.65 34 -> 31* 243.91/87.65 39 -> 48* 243.91/87.65 40 -> 31* 243.91/87.65 41 -> 81,63 243.91/87.65 42 -> 51,39 243.91/87.65 49 -> 51,39 243.91/87.65 52 -> 51,39 243.91/87.65 57 -> 78* 243.91/87.65 58 -> 136,33 243.91/87.65 64 -> 114,106,66 243.91/87.65 65 -> 52,40 243.91/87.65 68 -> 17* 243.91/87.65 78 -> 116* 243.91/87.65 79 -> 89* 243.91/87.65 80 -> 34* 243.91/87.65 82 -> 108,99 243.91/87.65 83 -> 49* 243.91/87.65 90 -> 16* 243.91/87.65 96 -> 140,132 243.91/87.65 97 -> 123* 243.91/87.65 98 -> 67* 243.91/87.65 100 -> 82* 243.91/87.65 107 -> 82* 243.91/87.65 109 -> 64* 243.91/87.65 115 -> 64* 243.91/87.65 116 -> 135* 243.91/87.65 117 -> 155,125 243.91/87.65 118 -> 90* 243.91/87.65 124 -> 67* 243.91/87.65 126 -> 16* 243.91/87.65 134 -> 124* 243.91/87.65 137 -> 126* 243.91/87.65 140 -> 147* 243.91/87.65 141 -> 171,133 243.91/87.65 147 -> 159* 243.91/87.65 148 -> 150* 243.91/87.65 149 -> 134* 243.91/87.65 151 -> 67* 243.91/87.65 155 -> 157* 243.91/87.65 156 -> 137* 243.91/87.65 158 -> 16* 243.91/87.65 159 -> 170* 243.91/87.65 160 -> 175,162 243.91/87.65 161 -> 151* 243.91/87.65 163 -> 67* 243.91/87.65 172 -> 163* 243.91/87.65 175 -> 177* 243.91/87.65 176 -> 172* 243.91/87.65 178 -> 67* 243.91/87.65 problem: 243.91/87.65 strict: 243.91/87.65 243.91/87.65 weak: 243.91/87.65 proper(d()) -> ok(d()) 243.91/87.65 top(ok(X)) -> top(active(X)) 243.91/87.65 active(g(X)) -> mark(h(X)) 243.91/87.65 active(c()) -> mark(d()) 243.91/87.65 active(h(d())) -> mark(g(c())) 243.91/87.65 top(mark(X)) -> top(proper(X)) 243.91/87.65 proper(g(X)) -> g(proper(X)) 243.91/87.65 proper(h(X)) -> h(proper(X)) 243.91/87.65 proper(c()) -> ok(c()) 243.91/87.65 g(ok(X)) -> ok(g(X)) 243.91/87.65 h(ok(X)) -> ok(h(X)) 243.91/87.65 Qed 243.91/87.65 243.91/87.65 strict: 243.91/87.65 proper(g(X)) -> g(proper(X)) 243.91/87.65 proper(h(X)) -> h(proper(X)) 243.91/87.65 proper(c()) -> ok(c()) 243.91/87.65 g(ok(X)) -> ok(g(X)) 243.91/87.65 h(ok(X)) -> ok(h(X)) 243.91/87.65 weak: 243.91/87.65 proper(d()) -> ok(d()) 243.91/87.65 top(ok(X)) -> top(active(X)) 243.91/87.65 active(g(X)) -> mark(h(X)) 243.91/87.65 active(c()) -> mark(d()) 243.91/87.65 active(h(d())) -> mark(g(c())) 243.91/87.65 top(mark(X)) -> top(proper(X)) 243.91/87.65 Splitting Processor: 243.91/87.65 strict: 243.91/87.65 g(ok(X)) -> ok(g(X)) 243.91/87.65 weak: 243.91/87.65 proper(d()) -> ok(d()) 243.91/87.65 top(ok(X)) -> top(active(X)) 243.91/87.65 active(g(X)) -> mark(h(X)) 243.91/87.65 active(c()) -> mark(d()) 243.91/87.65 active(h(d())) -> mark(g(c())) 243.91/87.65 top(mark(X)) -> top(proper(X)) 243.91/87.65 proper(g(X)) -> g(proper(X)) 243.91/87.65 proper(h(X)) -> h(proper(X)) 243.91/87.65 proper(c()) -> ok(c()) 243.91/87.65 h(ok(X)) -> ok(h(X)) 243.91/87.65 Splitting Processor: 243.91/87.65 strict: 243.91/87.65 proper(g(X)) -> g(proper(X)) 243.91/87.65 weak: 243.91/87.65 g(ok(X)) -> ok(g(X)) 243.91/87.65 proper(d()) -> ok(d()) 243.91/87.65 top(ok(X)) -> top(active(X)) 243.91/87.65 active(g(X)) -> mark(h(X)) 243.91/87.65 active(c()) -> mark(d()) 243.91/87.65 active(h(d())) -> mark(g(c())) 243.91/87.65 top(mark(X)) -> top(proper(X)) 243.91/87.66 proper(h(X)) -> h(proper(X)) 243.91/87.66 proper(c()) -> ok(c()) 243.91/87.66 h(ok(X)) -> ok(h(X)) 243.91/87.66 Splitting Processor: 243.91/87.66 strict: 243.91/87.66 proper(h(X)) -> h(proper(X)) 243.91/87.66 weak: 243.91/87.66 proper(g(X)) -> g(proper(X)) 243.91/87.66 g(ok(X)) -> ok(g(X)) 243.91/87.66 proper(d()) -> ok(d()) 243.91/87.66 top(ok(X)) -> top(active(X)) 243.91/87.66 active(g(X)) -> mark(h(X)) 243.91/87.66 active(c()) -> mark(d()) 243.91/87.66 active(h(d())) -> mark(g(c())) 243.91/87.66 top(mark(X)) -> top(proper(X)) 243.91/87.66 proper(c()) -> ok(c()) 243.91/87.66 h(ok(X)) -> ok(h(X)) 243.91/87.66 Splitting Processor: 243.91/87.66 strict: 243.91/87.66 h(ok(X)) -> ok(h(X)) 243.91/87.66 weak: 243.91/87.66 proper(h(X)) -> h(proper(X)) 243.91/87.66 proper(g(X)) -> g(proper(X)) 243.91/87.66 g(ok(X)) -> ok(g(X)) 243.91/87.66 proper(d()) -> ok(d()) 243.91/87.66 top(ok(X)) -> top(active(X)) 243.91/87.66 active(g(X)) -> mark(h(X)) 243.91/87.66 active(c()) -> mark(d()) 243.91/87.66 active(h(d())) -> mark(g(c())) 243.91/87.66 top(mark(X)) -> top(proper(X)) 243.91/87.66 proper(c()) -> ok(c()) 243.91/87.66 Matrix Interpretation Processor: dim=5 243.91/87.66 243.91/87.66 max_matrix: 243.91/87.66 [1 1 1 1 1] 243.91/87.66 [0 0 1 0 1] 243.91/87.66 [0 0 0 1 1] 243.91/87.66 [0 0 0 0 1] 243.91/87.66 [0 0 0 0 1] 243.91/87.66 interpretation: 243.91/87.66 [1 0 1 0 0] [0] 243.91/87.66 [0 0 1 0 0] [1] 243.91/87.66 [top](x0) = [0 0 0 0 0]x0 + [0] 243.91/87.66 [0 0 0 0 0] [1] 243.91/87.66 [0 0 0 0 0] [0], 243.91/87.66 243.91/87.66 [1 1 0 0 0] [0] 243.91/87.66 [0 0 0 0 0] [0] 243.91/87.66 [ok](x0) = [0 0 0 1 0]x0 + [1] 243.91/87.66 [0 0 0 0 0] [0] 243.91/87.66 [0 0 0 0 1] [1], 243.91/87.66 243.91/87.66 [1 0 0 0 1] [0] 243.91/87.66 [0 0 0 0 1] [0] 243.91/87.66 [proper](x0) = [0 0 0 1 0]x0 + [1] 243.91/87.66 [0 0 0 0 1] [0] 243.91/87.66 [0 0 0 0 1] [1], 243.91/87.66 243.91/87.66 [1] 243.91/87.66 [0] 243.91/87.66 [d] = [0] 243.91/87.66 [0] 243.91/87.66 [1], 243.91/87.66 243.91/87.66 [1] 243.91/87.66 [0] 243.91/87.66 [c] = [0] 243.91/87.66 [1] 243.91/87.66 [0], 243.91/87.66 243.91/87.66 [1 0 0 0 1] [0] 243.91/87.66 [0 0 0 0 0] [0] 243.91/87.66 [mark](x0) = [0 0 0 1 0]x0 + [1] 243.91/87.66 [0 0 0 0 1] [0] 243.91/87.66 [0 0 0 0 0] [0], 243.91/87.66 243.91/87.66 [1 0 0 0 1] [0] 243.91/87.66 [0 0 0 0 0] [0] 243.91/87.66 [h](x0) = [0 0 0 0 0]x0 + [1] 243.91/87.66 [0 0 0 0 0] [0] 243.91/87.66 [0 0 0 0 1] [1], 243.91/87.66 243.91/87.66 [1 1 0 1 0] [0] 243.91/87.66 [0 0 0 0 0] [0] 243.91/87.66 [active](x0) = [0 0 0 0 0]x0 + [1] 243.91/87.66 [0 0 0 0 1] [1] 243.91/87.66 [0 0 0 0 0] [0], 243.91/87.66 243.91/87.66 [1 0 0 0 1] [0] 243.91/87.66 [0 0 0 0 0] [1] 243.91/87.66 [g](x0) = [0 0 0 0 1]x0 + [0] 243.91/87.66 [0 0 0 0 1] [0] 243.91/87.66 [0 0 0 0 1] [1] 243.91/87.66 orientation: 243.91/87.66 [1 1 0 0 1] [1] [1 0 0 0 1] [0] 243.91/87.66 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 243.91/87.66 h(ok(X)) = [0 0 0 0 0]X + [1] >= [0 0 0 0 0]X + [1] = ok(h(X)) 243.91/87.66 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 243.91/87.66 [0 0 0 0 1] [2] [0 0 0 0 1] [2] 243.91/87.66 243.91/87.66 [1 0 0 0 2] [1] [1 0 0 0 2] [1] 243.91/87.66 [0 0 0 0 1] [1] [0 0 0 0 0] [0] 243.91/87.66 proper(h(X)) = [0 0 0 0 0]X + [1] >= [0 0 0 0 0]X + [1] = h(proper(X)) 243.91/87.66 [0 0 0 0 1] [1] [0 0 0 0 0] [0] 243.91/87.66 [0 0 0 0 1] [2] [0 0 0 0 1] [2] 243.91/87.66 243.91/87.66 [1 0 0 0 2] [1] [1 0 0 0 2] [1] 243.91/87.66 [0 0 0 0 1] [1] [0 0 0 0 0] [1] 243.91/87.66 proper(g(X)) = [0 0 0 0 1]X + [1] >= [0 0 0 0 1]X + [1] = g(proper(X)) 243.91/87.67 [0 0 0 0 1] [1] [0 0 0 0 1] [1] 243.91/87.67 [0 0 0 0 1] [2] [0 0 0 0 1] [2] 243.91/87.67 243.91/87.67 [1 1 0 0 1] [1] [1 0 0 0 1] [1] 243.91/87.67 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 243.91/87.67 g(ok(X)) = [0 0 0 0 1]X + [1] >= [0 0 0 0 1]X + [1] = ok(g(X)) 243.91/87.67 [0 0 0 0 1] [1] [0 0 0 0 0] [0] 243.91/87.67 [0 0 0 0 1] [2] [0 0 0 0 1] [2] 243.91/87.67 243.91/87.67 [2] [1] 243.91/87.67 [1] [0] 243.91/87.67 proper(d()) = [1] >= [1] = ok(d()) 243.91/87.67 [1] [0] 243.91/87.67 [2] [2] 243.91/87.67 243.91/87.67 [1 1 0 1 0] [1] [1 1 0 1 0] [1] 243.91/87.67 [0 0 0 1 0] [2] [0 0 0 0 0] [2] 243.91/87.67 top(ok(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = top(active(X)) 243.91/87.67 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 243.91/87.67 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 243.91/87.67 243.91/87.67 [1 0 0 0 2] [1] [1 0 0 0 2] [1] 243.91/87.67 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 243.91/87.67 active(g(X)) = [0 0 0 0 0]X + [1] >= [0 0 0 0 0]X + [1] = mark(h(X)) 243.91/87.67 [0 0 0 0 1] [2] [0 0 0 0 1] [1] 243.91/87.67 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 243.91/87.67 243.91/87.67 [2] [2] 243.91/87.67 [0] [0] 243.91/87.67 active(c()) = [1] >= [1] = mark(d()) 243.91/87.67 [1] [1] 243.91/87.67 [0] [0] 243.91/87.67 243.91/87.67 [2] [2] 243.91/87.67 [0] [0] 243.91/87.67 active(h(d())) = [1] >= [1] = mark(g(c())) 243.91/87.67 [3] [1] 243.91/87.67 [0] [0] 243.91/87.67 243.91/87.67 [1 0 0 1 1] [1] [1 0 0 1 1] [1] 243.91/87.67 [0 0 0 1 0] [2] [0 0 0 1 0] [2] 243.91/87.67 top(mark(X)) = [0 0 0 0 0]X + [0] >= [0 0 0 0 0]X + [0] = top(proper(X)) 243.91/87.67 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 243.91/87.67 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 243.91/87.67 243.91/87.67 [1] [1] 243.91/87.67 [0] [0] 243.91/87.67 proper(c()) = [2] >= [2] = ok(c()) 243.91/87.67 [0] [0] 243.91/87.67 [1] [1] 243.91/87.67 problem: 243.91/87.67 strict: 243.91/87.67 243.91/87.67 weak: 243.91/87.67 h(ok(X)) -> ok(h(X)) 243.91/87.67 proper(h(X)) -> h(proper(X)) 243.91/87.67 proper(g(X)) -> g(proper(X)) 243.91/87.67 g(ok(X)) -> ok(g(X)) 243.91/87.67 proper(d()) -> ok(d()) 243.91/87.67 top(ok(X)) -> top(active(X)) 243.91/87.67 active(g(X)) -> mark(h(X)) 243.91/87.67 active(c()) -> mark(d()) 243.91/87.67 active(h(d())) -> mark(g(c())) 243.91/87.67 top(mark(X)) -> top(proper(X)) 243.91/87.67 proper(c()) -> ok(c()) 243.91/87.67 Qed 243.91/87.67 243.91/87.67 strict: 243.91/87.67 proper(c()) -> ok(c()) 243.91/87.67 weak: 243.91/87.67 h(ok(X)) -> ok(h(X)) 243.91/87.67 proper(h(X)) -> h(proper(X)) 243.91/87.67 proper(g(X)) -> g(proper(X)) 243.91/87.67 g(ok(X)) -> ok(g(X)) 243.91/87.67 proper(d()) -> ok(d()) 243.91/87.67 top(ok(X)) -> top(active(X)) 243.91/87.67 active(g(X)) -> mark(h(X)) 243.91/87.67 active(c()) -> mark(d()) 243.91/87.67 active(h(d())) -> mark(g(c())) 243.91/87.67 top(mark(X)) -> top(proper(X)) 243.91/87.67 Bounds Processor: 243.91/87.67 bound: 2 243.91/87.67 enrichment: match 243.91/87.67 automaton: 243.91/87.67 final states: {10} 243.91/87.67 transitions: 243.91/87.67 ok1(42) -> 43* 243.91/87.67 ok1(13) -> 14* 243.91/87.67 c1() -> 13* 243.91/87.67 top1(23) -> 24* 243.91/87.67 active1(22) -> 23* 243.91/87.67 active1(64) -> 65* 243.91/87.67 g1(20) -> 21* 243.91/87.67 g1(58) -> 59* 243.91/87.67 h1(35) -> 36* 243.91/87.67 h1(25) -> 26* 243.91/87.67 h1(15) -> 16* 243.91/87.67 h1(52) -> 53* 243.91/87.67 mark1(26) -> 27* 243.91/87.67 d1() -> 28* 243.91/87.67 proper1(32) -> 33* 243.91/87.67 proper1(34) -> 35* 243.91/87.67 proper1(51) -> 52* 243.91/87.67 ok2(40) -> 41* 243.91/87.67 ok2(49) -> 50* 243.91/87.67 ok2(76) -> 77* 243.91/87.67 proper0(10) -> 10* 243.91/87.67 c2() -> 40* 243.91/87.67 c0() -> 10* 243.91/87.67 h2(85) -> 86* 243.91/87.67 h2(87) -> 88* 243.91/87.67 h2(48) -> 49* 243.91/87.67 ok0(10) -> 10* 243.91/87.67 top2(79) -> 80* 243.91/87.67 h0(10) -> 10* 243.91/87.67 active2(78) -> 79* 243.91/87.67 g0(10) -> 10* 243.91/87.67 g2(75) -> 76* 243.91/87.67 g2(94) -> 95* 243.91/87.67 g2(96) -> 97* 243.91/87.67 d0() -> 10* 243.91/87.67 top0(10) -> 10* 243.91/87.67 active0(10) -> 10* 243.91/87.67 mark0(10) -> 10* 243.91/87.67 13 -> 22,20,15 243.91/87.67 14 -> 10* 243.91/87.67 15 -> 51* 243.91/87.67 16 -> 13* 243.91/87.67 20 -> 25* 243.91/87.67 21 -> 13* 243.91/87.67 24 -> 10* 243.91/87.67 25 -> 34* 243.91/87.67 26 -> 32* 243.91/87.67 27 -> 23* 243.91/87.67 28 -> 42,26 243.91/87.67 33 -> 23* 243.91/87.67 35 -> 58* 243.91/87.67 36 -> 33* 243.91/87.67 40 -> 75,48 243.91/87.67 41 -> 52,35 243.91/87.67 42 -> 64* 243.91/87.67 43 -> 33* 243.91/87.67 49 -> 94,85,78 243.91/87.67 50 -> 53,36 243.91/87.67 53 -> 52,35 243.91/87.67 59 -> 52,35 243.91/87.67 65 -> 23* 243.91/87.67 76 -> 96,87 243.91/87.67 77 -> 59* 243.91/87.67 80 -> 24* 243.91/87.67 86 -> 49* 243.91/87.67 88 -> 49* 243.91/87.67 95 -> 76* 243.91/87.67 97 -> 76* 243.91/87.67 problem: 243.91/87.67 strict: 243.91/87.67 243.91/87.67 weak: 243.91/87.67 proper(c()) -> ok(c()) 243.91/87.67 h(ok(X)) -> ok(h(X)) 243.91/87.67 proper(h(X)) -> h(proper(X)) 243.91/87.67 proper(g(X)) -> g(proper(X)) 243.91/87.67 g(ok(X)) -> ok(g(X)) 243.91/87.67 proper(d()) -> ok(d()) 243.91/87.67 top(ok(X)) -> top(active(X)) 243.91/87.67 active(g(X)) -> mark(h(X)) 243.91/87.67 active(c()) -> mark(d()) 243.91/87.67 active(h(d())) -> mark(g(c())) 243.91/87.67 top(mark(X)) -> top(proper(X)) 243.91/87.67 Qed 243.91/87.67 243.91/87.67 strict: 243.91/87.67 proper(c()) -> ok(c()) 243.91/87.67 h(ok(X)) -> ok(h(X)) 243.91/87.67 weak: 243.91/87.67 proper(h(X)) -> h(proper(X)) 243.91/87.67 proper(g(X)) -> g(proper(X)) 243.91/87.67 g(ok(X)) -> ok(g(X)) 243.91/87.67 proper(d()) -> ok(d()) 243.91/87.67 top(ok(X)) -> top(active(X)) 243.91/87.67 active(g(X)) -> mark(h(X)) 243.91/87.67 active(c()) -> mark(d()) 243.91/87.67 active(h(d())) -> mark(g(c())) 243.91/87.67 top(mark(X)) -> top(proper(X)) 243.91/87.67 Matrix Interpretation Processor: dim=4 243.91/87.67 243.91/87.67 max_matrix: 243.91/87.67 [1 1 1 1] 243.91/87.67 [0 1 1 1] 243.91/87.67 [0 0 0 1] 243.91/87.67 [0 0 0 0] 243.91/87.67 interpretation: 243.91/87.67 [1 0 1 0] 243.91/87.67 [0 0 1 0] 243.91/87.67 [top](x0) = [0 0 0 0]x0 243.91/87.67 [0 0 0 0] , 243.91/87.67 243.91/87.67 [1 0 0 0] [1] 243.91/87.67 [0 1 1 0] [0] 243.91/87.67 [ok](x0) = [0 0 0 1]x0 + [0] 243.91/87.67 [0 0 0 0] [0], 243.91/87.67 243.91/87.67 [1 1 0 1] 243.91/87.67 [0 1 0 0] 243.91/87.67 [proper](x0) = [0 0 0 1]x0 243.91/87.67 [0 0 0 0] , 243.91/87.67 243.91/87.67 [1] 243.91/87.67 [1] 243.91/87.67 [d] = [0] 243.91/87.67 [0], 243.91/87.67 243.91/87.67 [0] 243.91/87.67 [0] 243.91/87.67 [c] = [0] 243.91/87.67 [1], 243.91/87.67 243.91/87.67 [1 1 0 1] 243.91/87.67 [0 0 0 0] 243.91/87.67 [mark](x0) = [0 0 0 1]x0 243.91/87.67 [0 0 0 0] , 243.91/87.67 243.91/87.67 [1 0 0 0] [1] 243.91/87.67 [0 1 1 1] [1] 243.91/87.67 [h](x0) = [0 0 0 0]x0 + [0] 243.91/87.67 [0 0 0 0] [0], 243.91/87.67 243.91/87.67 [1 0 0 1] [1] 243.91/87.67 [0 0 0 0] [0] 243.91/87.67 [active](x0) = [0 0 0 0]x0 + [0] 243.91/87.67 [0 0 0 0] [0], 243.91/87.67 243.91/87.67 [1 1 1 1] [1] 243.91/87.67 [0 1 1 1] [0] 243.91/87.67 [g](x0) = [0 0 0 0]x0 + [0] 243.91/87.67 [0 0 0 0] [0] 243.91/87.67 orientation: 243.91/87.67 [1 1 1 1] [2] [1 1 0 1] [1] 243.91/87.68 [0 1 1 1] [1] [0 1 0 1] [1] 243.91/87.68 proper(h(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = h(proper(X)) 243.91/87.68 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.68 243.91/87.68 [1 2 2 2] [1] [1 2 0 2] [1] 243.91/87.68 [0 1 1 1] [0] [0 1 0 1] [0] 243.91/87.68 proper(g(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = g(proper(X)) 243.91/87.68 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.68 243.91/87.68 [1 1 1 1] [2] [1 1 1 1] [2] 243.91/87.68 [0 1 1 1] [0] [0 1 1 1] [0] 243.91/87.68 g(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = ok(g(X)) 243.91/87.68 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.68 243.91/87.68 [2] [2] 243.91/87.68 [1] [1] 243.91/87.68 proper(d()) = [0] >= [0] = ok(d()) 243.91/87.68 [0] [0] 243.91/87.68 243.91/87.68 [1 0 0 1] [1] [1 0 0 1] [1] 243.91/87.68 [0 0 0 1] [0] [0 0 0 0] [0] 243.91/87.68 top(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = top(active(X)) 243.91/87.68 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.68 243.91/87.68 [1 1 1 1] [2] [1 1 1 1] [2] 243.91/87.68 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.68 active(g(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = mark(h(X)) 243.91/87.68 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.68 243.91/87.68 [2] [2] 243.91/87.68 [0] [0] 243.91/87.68 active(c()) = [0] >= [0] = mark(d()) 243.91/87.68 [0] [0] 243.91/87.68 243.91/87.68 [3] [3] 243.91/87.68 [0] [0] 243.91/87.68 active(h(d())) = [0] >= [0] = mark(g(c())) 243.91/87.68 [0] [0] 243.91/87.68 243.91/87.68 [1 1 0 2] [1 1 0 2] 243.91/87.68 [0 0 0 1] [0 0 0 1] 243.91/87.68 top(mark(X)) = [0 0 0 0]X >= [0 0 0 0]X = top(proper(X)) 243.91/87.68 [0 0 0 0] [0 0 0 0] 243.91/87.68 243.91/87.68 [1] [1] 243.91/87.68 [0] [0] 243.91/87.68 proper(c()) = [1] >= [1] = ok(c()) 243.91/87.68 [0] [0] 243.91/87.68 243.91/87.68 [1 0 0 0] [2] [1 0 0 0] [2] 243.91/87.68 [0 1 1 1] [1] [0 1 1 1] [1] 243.91/87.68 h(ok(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = ok(h(X)) 243.91/87.68 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.68 problem: 243.91/87.68 strict: 243.91/87.68 243.91/87.68 weak: 243.91/87.68 proper(h(X)) -> h(proper(X)) 243.91/87.68 proper(g(X)) -> g(proper(X)) 243.91/87.68 g(ok(X)) -> ok(g(X)) 243.91/87.68 proper(d()) -> ok(d()) 243.91/87.68 top(ok(X)) -> top(active(X)) 243.91/87.68 active(g(X)) -> mark(h(X)) 243.91/87.68 active(c()) -> mark(d()) 243.91/87.68 active(h(d())) -> mark(g(c())) 243.91/87.68 top(mark(X)) -> top(proper(X)) 243.91/87.68 proper(c()) -> ok(c()) 243.91/87.68 h(ok(X)) -> ok(h(X)) 243.91/87.68 Qed 243.91/87.68 243.91/87.68 strict: 243.91/87.68 proper(h(X)) -> h(proper(X)) 243.91/87.68 proper(c()) -> ok(c()) 243.91/87.68 h(ok(X)) -> ok(h(X)) 243.91/87.68 weak: 243.91/87.68 proper(g(X)) -> g(proper(X)) 243.91/87.68 g(ok(X)) -> ok(g(X)) 243.91/87.68 proper(d()) -> ok(d()) 243.91/87.68 top(ok(X)) -> top(active(X)) 243.91/87.68 active(g(X)) -> mark(h(X)) 243.91/87.68 active(c()) -> mark(d()) 243.91/87.68 active(h(d())) -> mark(g(c())) 243.91/87.68 top(mark(X)) -> top(proper(X)) 243.91/87.68 Matrix Interpretation Processor: dim=4 243.91/87.68 243.91/87.68 max_matrix: 243.91/87.68 [1 1 1 1] 243.91/87.68 [0 0 0 1] 243.91/87.68 [0 0 1 1] 243.91/87.68 [0 0 0 0] 243.91/87.68 interpretation: 243.91/87.68 [1 1 0 0] 243.91/87.68 [0 0 0 0] 243.91/87.68 [top](x0) = [0 0 0 1]x0 243.91/87.68 [0 0 0 0] , 243.91/87.68 243.91/87.68 [1 0 0 0] 243.91/87.68 [0 0 0 1] 243.91/87.68 [ok](x0) = [0 0 1 0]x0 243.91/87.68 [0 0 0 0] , 243.91/87.68 243.91/87.68 [1 0 1 0] 243.91/87.68 [0 0 0 1] 243.91/87.68 [proper](x0) = [0 0 1 0]x0 243.91/87.68 [0 0 0 0] , 243.91/87.68 243.91/87.68 [1] 243.91/87.68 [0] 243.91/87.68 [d] = [0] 243.91/87.68 [0], 243.91/87.68 243.91/87.68 [0] 243.91/87.68 [0] 243.91/87.68 [c] = [0] 243.91/87.68 [1], 243.91/87.68 243.91/87.68 [1 0 1 0] 243.91/87.68 [0 0 0 1] 243.91/87.68 [mark](x0) = [0 0 0 0]x0 243.91/87.68 [0 0 0 0] , 243.91/87.68 243.91/87.68 [1 0 0 0] 243.91/87.68 [0 0 0 0] 243.91/87.68 [h](x0) = [0 0 1 0]x0 243.91/87.68 [0 0 0 0] , 243.91/87.68 243.91/87.68 [1 0 0 1] 243.91/87.68 [0 0 0 0] 243.91/87.68 [active](x0) = [0 0 0 0]x0 243.91/87.68 [0 0 0 0] , 243.91/87.68 243.91/87.68 [1 0 1 0] [0] 243.91/87.68 [0 0 0 0] [0] 243.91/87.68 [g](x0) = [0 0 1 0]x0 + [1] 243.91/87.68 [0 0 0 0] [0] 243.91/87.68 orientation: 243.91/87.68 [1 0 2 0] [1] [1 0 2 0] [0] 243.91/87.68 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.68 proper(g(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = g(proper(X)) 243.91/87.68 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.68 243.91/87.68 [1 0 1 0] [0] [1 0 1 0] [0] 243.91/87.68 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.68 g(ok(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = ok(g(X)) 243.91/87.68 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.68 243.91/87.68 [1] [1] 243.91/87.68 [0] [0] 243.91/87.68 proper(d()) = [0] >= [0] = ok(d()) 243.91/87.68 [0] [0] 243.91/87.68 243.91/87.68 [1 0 0 1] [1 0 0 1] 243.91/87.68 [0 0 0 0] [0 0 0 0] 243.91/87.68 top(ok(X)) = [0 0 0 0]X >= [0 0 0 0]X = top(active(X)) 243.91/87.68 [0 0 0 0] [0 0 0 0] 243.91/87.69 243.91/87.69 [1 0 1 0] [1 0 1 0] 243.91/87.69 [0 0 0 0] [0 0 0 0] 243.91/87.69 active(g(X)) = [0 0 0 0]X >= [0 0 0 0]X = mark(h(X)) 243.91/87.69 [0 0 0 0] [0 0 0 0] 243.91/87.69 243.91/87.69 [1] [1] 243.91/87.69 [0] [0] 243.91/87.69 active(c()) = [0] >= [0] = mark(d()) 243.91/87.69 [0] [0] 243.91/87.69 243.91/87.69 [1] [1] 243.91/87.69 [0] [0] 243.91/87.69 active(h(d())) = [0] >= [0] = mark(g(c())) 243.91/87.69 [0] [0] 243.91/87.69 243.91/87.69 [1 0 1 1] [1 0 1 1] 243.91/87.69 [0 0 0 0] [0 0 0 0] 243.91/87.69 top(mark(X)) = [0 0 0 0]X >= [0 0 0 0]X = top(proper(X)) 243.91/87.69 [0 0 0 0] [0 0 0 0] 243.91/87.69 243.91/87.69 [1 0 1 0] [1 0 1 0] 243.91/87.69 [0 0 0 0] [0 0 0 0] 243.91/87.69 proper(h(X)) = [0 0 1 0]X >= [0 0 1 0]X = h(proper(X)) 243.91/87.69 [0 0 0 0] [0 0 0 0] 243.91/87.69 243.91/87.69 [0] [0] 243.91/87.69 [1] [1] 243.91/87.69 proper(c()) = [0] >= [0] = ok(c()) 243.91/87.69 [0] [0] 243.91/87.69 243.91/87.69 [1 0 0 0] [1 0 0 0] 243.91/87.69 [0 0 0 0] [0 0 0 0] 243.91/87.69 h(ok(X)) = [0 0 1 0]X >= [0 0 1 0]X = ok(h(X)) 243.91/87.69 [0 0 0 0] [0 0 0 0] 243.91/87.69 problem: 243.91/87.69 strict: 243.91/87.69 243.91/87.69 weak: 243.91/87.69 proper(g(X)) -> g(proper(X)) 243.91/87.69 g(ok(X)) -> ok(g(X)) 243.91/87.69 proper(d()) -> ok(d()) 243.91/87.69 top(ok(X)) -> top(active(X)) 243.91/87.69 active(g(X)) -> mark(h(X)) 243.91/87.69 active(c()) -> mark(d()) 243.91/87.69 active(h(d())) -> mark(g(c())) 243.91/87.69 top(mark(X)) -> top(proper(X)) 243.91/87.69 proper(h(X)) -> h(proper(X)) 243.91/87.69 proper(c()) -> ok(c()) 243.91/87.69 h(ok(X)) -> ok(h(X)) 243.91/87.69 Qed 243.91/87.69 243.91/87.69 strict: 243.91/87.69 proper(g(X)) -> g(proper(X)) 243.91/87.69 proper(h(X)) -> h(proper(X)) 243.91/87.69 proper(c()) -> ok(c()) 243.91/87.69 h(ok(X)) -> ok(h(X)) 243.91/87.69 weak: 243.91/87.69 g(ok(X)) -> ok(g(X)) 243.91/87.69 proper(d()) -> ok(d()) 243.91/87.69 top(ok(X)) -> top(active(X)) 243.91/87.69 active(g(X)) -> mark(h(X)) 243.91/87.69 active(c()) -> mark(d()) 243.91/87.69 active(h(d())) -> mark(g(c())) 243.91/87.69 top(mark(X)) -> top(proper(X)) 243.91/87.69 Matrix Interpretation Processor: dim=4 243.91/87.69 243.91/87.69 max_matrix: 243.91/87.69 [1 1 1 1] 243.91/87.69 [0 0 0 1] 243.91/87.69 [0 0 1 1] 243.91/87.69 [0 0 0 0] 243.91/87.69 interpretation: 243.91/87.69 [1 1 0 0] [0] 243.91/87.69 [0 0 0 0] [0] 243.91/87.69 [top](x0) = [0 0 0 1]x0 + [1] 243.91/87.69 [0 0 0 0] [0], 243.91/87.69 243.91/87.69 [1 0 0 0] [1] 243.91/87.69 [0 0 0 1] [1] 243.91/87.69 [ok](x0) = [0 0 1 0]x0 + [1] 243.91/87.69 [0 0 0 0] [0], 243.91/87.69 243.91/87.69 [1 0 1 0] [0] 243.91/87.69 [0 0 0 1] [1] 243.91/87.69 [proper](x0) = [0 0 1 0]x0 + [1] 243.91/87.69 [0 0 0 0] [0], 243.91/87.69 243.91/87.69 [1] 243.91/87.69 [0] 243.91/87.69 [d] = [1] 243.91/87.69 [0], 243.91/87.69 243.91/87.69 [0] 243.91/87.69 [0] 243.91/87.69 [c] = [1] 243.91/87.69 [1], 243.91/87.69 243.91/87.69 [1 0 1 0] [0] 243.91/87.69 [0 0 0 1] [1] 243.91/87.69 [mark](x0) = [0 0 0 0]x0 + [0] 243.91/87.69 [0 0 0 0] [0], 243.91/87.69 243.91/87.69 [1 0 0 0] [1] 243.91/87.69 [0 0 0 0] [1] 243.91/87.69 [h](x0) = [0 0 1 0]x0 + [0] 243.91/87.69 [0 0 0 0] [0], 243.91/87.69 243.91/87.69 [1 0 0 1] [1] 243.91/87.69 [0 0 0 0] [1] 243.91/87.69 [active](x0) = [0 0 0 0]x0 + [1] 243.91/87.69 [0 0 0 0] [0], 243.91/87.69 243.91/87.69 [1 0 1 0] [0] 243.91/87.69 [0 0 0 0] [1] 243.91/87.69 [g](x0) = [0 0 1 0]x0 + [1] 243.91/87.69 [0 0 0 0] [0] 243.91/87.69 orientation: 243.91/87.69 [1 0 1 0] [2] [1 0 1 0] [1] 243.91/87.69 [0 0 0 0] [1] [0 0 0 0] [1] 243.91/87.69 g(ok(X)) = [0 0 1 0]X + [2] >= [0 0 1 0]X + [2] = ok(g(X)) 243.91/87.69 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.69 243.91/87.69 [2] [2] 243.91/87.69 [1] [1] 243.91/87.69 proper(d()) = [2] >= [2] = ok(d()) 243.91/87.69 [0] [0] 243.91/87.69 243.91/87.69 [1 0 0 1] [2] [1 0 0 1] [2] 243.91/87.69 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.69 top(ok(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(active(X)) 243.91/87.69 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.69 243.91/87.69 [1 0 1 0] [1] [1 0 1 0] [1] 243.91/87.69 [0 0 0 0] [1] [0 0 0 0] [1] 243.91/87.69 active(g(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [0] = mark(h(X)) 243.91/87.69 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.69 243.91/87.69 [2] [2] 243.91/87.69 [1] [1] 243.91/87.69 active(c()) = [1] >= [0] = mark(d()) 243.91/87.69 [0] [0] 243.91/87.69 243.91/87.69 [3] [3] 243.91/87.69 [1] [1] 243.91/87.69 active(h(d())) = [1] >= [0] = mark(g(c())) 243.91/87.69 [0] [0] 243.91/87.69 243.91/87.69 [1 0 1 1] [1] [1 0 1 1] [1] 243.91/87.69 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.69 top(mark(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = top(proper(X)) 243.91/87.69 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.69 243.91/87.69 [1 0 2 0] [1] [1 0 2 0] [1] 243.91/87.69 [0 0 0 0] [1] [0 0 0 0] [1] 243.91/87.69 proper(g(X)) = [0 0 1 0]X + [2] >= [0 0 1 0]X + [2] = g(proper(X)) 243.91/87.69 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.69 243.91/87.69 [1 0 1 0] [1] [1 0 1 0] [1] 243.91/87.69 [0 0 0 0] [1] [0 0 0 0] [1] 243.91/87.69 proper(h(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = h(proper(X)) 243.91/87.69 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.69 243.91/87.69 [1] [1] 243.91/87.69 [2] [2] 243.91/87.69 proper(c()) = [2] >= [2] = ok(c()) 243.91/87.69 [0] [0] 243.91/87.69 243.91/87.69 [1 0 0 0] [2] [1 0 0 0] [2] 243.91/87.69 [0 0 0 0] [1] [0 0 0 0] [1] 243.91/87.69 h(ok(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = ok(h(X)) 243.91/87.69 [0 0 0 0] [0] [0 0 0 0] [0] 243.91/87.69 problem: 243.91/87.69 strict: 243.91/87.69 243.91/87.69 weak: 243.91/87.69 g(ok(X)) -> ok(g(X)) 243.91/87.69 proper(d()) -> ok(d()) 243.91/87.69 top(ok(X)) -> top(active(X)) 243.91/87.69 active(g(X)) -> mark(h(X)) 243.91/87.69 active(c()) -> mark(d()) 243.91/87.69 active(h(d())) -> mark(g(c())) 243.91/87.69 top(mark(X)) -> top(proper(X)) 243.91/87.69 proper(g(X)) -> g(proper(X)) 243.91/87.69 proper(h(X)) -> h(proper(X)) 243.91/87.69 proper(c()) -> ok(c()) 243.91/87.69 h(ok(X)) -> ok(h(X)) 243.91/87.69 Qed 244.01/87.70 EOF