YES(?,O(n^1)) 5.93/1.99 YES(?,O(n^1)) 5.93/2.00 5.93/2.00 Problem: 5.93/2.00 active(c()) -> mark(f(g(c()))) 5.93/2.00 active(f(g(X))) -> mark(g(X)) 5.93/2.00 mark(c()) -> active(c()) 5.93/2.00 mark(f(X)) -> active(f(X)) 5.93/2.00 mark(g(X)) -> active(g(X)) 5.93/2.00 f(mark(X)) -> f(X) 5.93/2.00 f(active(X)) -> f(X) 5.93/2.00 g(mark(X)) -> g(X) 5.93/2.00 g(active(X)) -> g(X) 5.93/2.00 5.93/2.00 Proof: 5.93/2.00 Bounds Processor: 5.93/2.00 bound: 4 5.93/2.00 enrichment: match 5.93/2.00 automaton: 5.93/2.00 final states: {6} 5.93/2.00 transitions: 5.93/2.00 active3(112) -> 113* 5.93/2.00 active3(169) -> 170* 5.93/2.00 active3(171) -> 172* 5.93/2.00 active3(165) -> 166* 5.93/2.00 f3(111) -> 112* 5.93/2.00 g4(309) -> 310* 5.93/2.00 g4(284) -> 285* 5.93/2.00 g4(303) -> 304* 5.93/2.00 g4(305) -> 306* 5.93/2.00 g4(240) -> 241* 5.93/2.00 g4(392) -> 393* 5.93/2.00 g4(307) -> 308* 5.93/2.00 mark3(163) -> 164* 5.93/2.00 active4(285) -> 286* 5.93/2.00 active0(6) -> 6* 5.93/2.00 c0() -> 6* 5.93/2.00 mark0(6) -> 6* 5.93/2.00 f0(6) -> 6* 5.93/2.00 g0(6) -> 6* 5.93/2.00 g1(15) -> 16* 5.93/2.00 g1(11) -> 12* 5.93/2.00 f1(12) -> 13* 5.93/2.00 f1(23) -> 24* 5.93/2.00 active1(29) -> 30* 5.93/2.00 active1(21) -> 22* 5.93/2.00 c1() -> 11* 5.93/2.00 mark1(13) -> 14* 5.93/2.00 g2(35) -> 36* 5.93/2.00 g2(84) -> 85* 5.93/2.00 g2(76) -> 77* 5.93/2.00 g2(43) -> 44* 5.93/2.00 g2(90) -> 91* 5.93/2.00 f2(70) -> 71* 5.93/2.00 f2(197) -> 198* 5.93/2.00 f2(132) -> 133* 5.93/2.00 f2(299) -> 300* 5.93/2.00 f2(62) -> 63* 5.93/2.00 f2(209) -> 210* 5.93/2.00 f2(396) -> 397* 5.93/2.00 f2(189) -> 190* 5.93/2.00 f2(134) -> 135* 5.93/2.00 f2(124) -> 125* 5.93/2.00 f2(301) -> 302* 5.93/2.00 f2(291) -> 292* 5.93/2.00 f2(49) -> 50* 5.93/2.00 f2(201) -> 202* 5.93/2.00 f2(191) -> 192* 5.93/2.00 f2(333) -> 334* 5.93/2.00 f2(323) -> 324* 5.93/2.00 f2(36) -> 37* 5.93/2.00 f2(203) -> 204* 5.93/2.00 f2(193) -> 194* 5.93/2.00 f2(325) -> 326* 5.93/2.00 f2(315) -> 316* 5.93/2.00 f2(68) -> 69* 5.93/2.00 f2(317) -> 318* 5.93/2.00 f2(297) -> 298* 5.93/2.00 active2(50) -> 51* 5.93/2.00 active2(116) -> 117* 5.93/2.00 active2(56) -> 57* 5.93/2.00 active2(118) -> 119* 5.93/2.00 active2(120) -> 121* 5.93/2.00 mark2(272) -> 273* 5.93/2.00 mark2(394) -> 395* 5.93/2.00 mark2(107) -> 108* 5.93/2.00 mark2(274) -> 275* 5.93/2.00 mark2(37) -> 38* 5.93/2.00 mark2(109) -> 110* 5.93/2.00 mark2(276) -> 277* 5.93/2.00 mark2(101) -> 102* 5.93/2.00 mark2(278) -> 279* 5.93/2.00 c2() -> 35* 5.93/2.00 g3(252) -> 253* 5.93/2.00 g3(222) -> 223* 5.93/2.00 g3(217) -> 218* 5.93/2.00 g3(177) -> 178* 5.93/2.00 g3(162) -> 163* 5.93/2.00 g3(344) -> 345* 5.93/2.00 g3(254) -> 255* 5.93/2.00 g3(179) -> 180* 5.93/2.00 g3(154) -> 155* 5.93/2.00 g3(114) -> 115* 5.93/2.00 g3(246) -> 247* 5.93/2.00 g3(398) -> 399* 5.93/2.00 g3(156) -> 157* 5.93/2.00 g3(228) -> 229* 5.93/2.00 g3(340) -> 341* 5.93/2.00 g3(335) -> 336* 5.93/2.00 g3(185) -> 186* 5.93/2.00 g3(160) -> 161* 5.93/2.00 g3(342) -> 343* 5.93/2.00 6 -> 23,15 5.93/2.00 11 -> 21* 5.93/2.00 12 -> 49* 5.93/2.00 13 -> 76,62 5.93/2.00 14 -> 6* 5.93/2.00 15 -> 43* 5.93/2.00 16 -> 6,29,13 5.93/2.00 21 -> 90,70 5.93/2.00 22 -> 6* 5.93/2.00 24 -> 6,21 5.93/2.00 29 -> 84,68 5.93/2.00 30 -> 6* 5.93/2.00 35 -> 162* 5.93/2.00 36 -> 111* 5.93/2.00 37 -> 154,124 5.93/2.00 38 -> 22,6 5.93/2.00 43 -> 114* 5.93/2.00 44 -> 56,37 5.93/2.00 50 -> 156,132 5.93/2.00 51 -> 14,6 5.93/2.00 56 -> 160,134 5.93/2.00 57 -> 14,6 5.93/2.00 63 -> 24,6,15,23,21 5.93/2.00 69 -> 24,6,15,23,21 5.93/2.00 71 -> 24,6,15,23,21 5.93/2.00 76 -> 179* 5.93/2.00 77 -> 115,44,37,56,118,107,16,13,6,29 5.93/2.00 84 -> 177* 5.93/2.00 85 -> 115,44,37,56,120,109,16,13,6,29 5.93/2.00 90 -> 185* 5.93/2.00 91 -> 115,44,37,56,116,101,16,13,6,29 5.93/2.00 101 -> 228,193 5.93/2.00 102 -> 51,22,14 5.93/2.00 107 -> 217,189 5.93/2.00 108 -> 22,6 5.93/2.00 109 -> 222,191 5.93/2.00 110 -> 22,6 5.93/2.00 112 -> 240,197 5.93/2.00 113 -> 277,279,275,273,108,110,102,38,22 5.93/2.00 115 -> 276,112 5.93/2.00 116 -> 246,201 5.93/2.00 117 -> 14,6 5.93/2.00 118 -> 252,203 5.93/2.00 119 -> 14,6 5.93/2.00 120 -> 254,209 5.93/2.00 121 -> 14,6 5.93/2.00 125 -> 24,6,23,15,43,21,90 5.93/2.00 133 -> 24,6,23,15,43,21,90 5.93/2.00 135 -> 24,6,23,15,43,21,90 5.93/2.00 155 -> 115,112,165,44,37,16,56 5.93/2.00 157 -> 115,112,169,44,37,16,56 5.93/2.00 161 -> 115,112,171,44,37,16,56 5.93/2.00 162 -> 284* 5.93/2.00 163 -> 303,291 5.93/2.00 164 -> 113,38 5.93/2.00 165 -> 309,301 5.93/2.00 166 -> 38* 5.93/2.00 169 -> 305,297 5.93/2.00 170 -> 38* 5.93/2.00 171 -> 307,299 5.93/2.00 172 -> 38* 5.93/2.00 178 -> 272,112 5.93/2.00 180 -> 274,112 5.93/2.00 186 -> 278,112 5.93/2.00 190 -> 24,6,15,23,114,21,90 5.93/2.00 192 -> 24,6,15,23,114,21,90 5.93/2.00 194 -> 24,6,15,23,114,21,90 5.93/2.00 198 -> 24,6,15,23,114,21,90 5.93/2.00 202 -> 24,6,15,23,114,21,90 5.93/2.00 204 -> 24,6,15,23,114,21,90 5.93/2.00 210 -> 24,6,15,23,114,21,90 5.93/2.00 218 -> 115,44,37,16,56,160,154,112 5.93/2.00 223 -> 115,44,37,16,56,160,154,112 5.93/2.00 229 -> 115,44,37,16,56,160,154,112 5.93/2.00 241 -> 115,44,37,16,56,160,154,112 5.93/2.00 247 -> 115,44,37,16,56,160,154,112 5.93/2.00 253 -> 115,44,37,16,56,160,154,112 5.93/2.00 255 -> 115,44,37,16,56,160,154,112 5.93/2.00 272 -> 335,315 5.93/2.00 273 -> 22* 5.93/2.00 274 -> 340,317 5.93/2.00 275 -> 22* 5.93/2.00 276 -> 342,323 5.93/2.00 277 -> 22* 5.93/2.00 278 -> 344,325 5.93/2.00 279 -> 22* 5.93/2.00 285 -> 394,392,333 5.93/2.00 286 -> 395,164,113 5.93/2.00 292 -> 24,21,6,70,185 5.93/2.00 298 -> 24,21,6,70,185 5.93/2.00 300 -> 24,21,6,70,185 5.93/2.00 302 -> 24,21,6,70,185 5.93/2.00 304 -> 115,44,37,16,56,160,154,112,240 5.93/2.00 306 -> 115,44,37,16,56,160,154,112,240 5.93/2.00 308 -> 115,44,37,16,56,160,154,112,240 5.93/2.00 310 -> 115,44,37,16,56,160,154,112,240 5.93/2.00 316 -> 24,21,6,70,185 5.93/2.00 318 -> 24,21,6,70,185 5.93/2.00 324 -> 24,21,6,70,185 5.93/2.00 326 -> 24,21,6,70,185 5.93/2.00 334 -> 24,21,6,70,185 5.93/2.00 336 -> 115,112,16,13,6,29,84,76,177,44,276,240 5.93/2.00 341 -> 115,112,16,13,6,29,84,76,177,44,276,240 5.93/2.00 343 -> 115,112,16,13,6,29,84,76,177,44,276,240 5.93/2.00 345 -> 115,112,16,13,6,29,84,76,177,44,276,240 5.93/2.00 393 -> 115,112,16,13,6,29,84,76,177,44,276,240 5.93/2.00 394 -> 398,396 5.93/2.00 395 -> 22* 5.93/2.00 397 -> 24,21,6,70,185 5.93/2.00 399 -> 115,112,16,13,6,29,84,76,177,44,276,342,240 5.93/2.00 problem: 5.93/2.00 5.93/2.00 Qed 6.91/2.00 EOF