YES(?,O(n^1)) Problem: R(2(x1)) -> 2(R(x1)) R(3(x1)) -> 3(R(x1)) R(1(x1)) -> L(3(x1)) 3(L(x1)) -> L(3(x1)) 2(L(x1)) -> L(2(x1)) 0(L(x1)) -> 2(R(x1)) R(b(x1)) -> c(1(b(x1))) 3(c(x1)) -> c(1(x1)) 2(c(1(x1))) -> c(0(R(1(x1)))) 2(c(0(x1))) -> c(0(0(x1))) Proof: Bounds Processor: bound: 6 enrichment: match automaton: final states: {8,7,6,5} transitions: R3(152) -> 153* R3(324) -> 325* R3(299) -> 300* R3(234) -> 235* R3(216) -> 217* R3(161) -> 162* R3(163) -> 164* R3(155) -> 156* 23(217) -> 218* 23(264) -> 265* 23(235) -> 236* 34(247) -> 248* 34(306) -> 307* 34(413) -> 414* 34(328) -> 329* 34(223) -> 224* R4(222) -> 223* R4(334) -> 335* R4(259) -> 260* R4(246) -> 247* R4(343) -> 344* R4(253) -> 254* R4(255) -> 256* R4(362) -> 363* c3(326) -> 327* c3(301) -> 302* c3(313) -> 314* 03(325) -> 326* 03(300) -> 301* 13(323) -> 324* 13(298) -> 299* 13(312) -> 313* b2(277) -> 278* b2(283) -> 284* b2(273) -> 274* b2(285) -> 286* L4(307) -> 308* L4(414) -> 415* L4(329) -> 330* L4(408) -> 409* L4(420) -> 421* R0(2) -> 5* R0(4) -> 5* R0(1) -> 5* R0(3) -> 5* c4(345) -> 346* 20(2) -> 7* 20(4) -> 7* 20(1) -> 7* 20(3) -> 7* 04(344) -> 345* 30(2) -> 6* 30(4) -> 6* 30(1) -> 6* 30(3) -> 6* 14(342) -> 343* 10(2) -> 1* 10(4) -> 1* 10(1) -> 1* 10(3) -> 1* 24(419) -> 420* 24(363) -> 364* 24(335) -> 336* 24(407) -> 408* L0(2) -> 2* L0(4) -> 2* L0(1) -> 2* L0(3) -> 2* L5(426) -> 427* L5(357) -> 358* 00(2) -> 8* 00(4) -> 8* 00(1) -> 8* 00(3) -> 8* 35(366) -> 367* 35(356) -> 357* 35(351) -> 352* b0(2) -> 3* b0(4) -> 3* b0(1) -> 3* b0(3) -> 3* R5(365) -> 366* R5(350) -> 351* R5(377) -> 378* c0(2) -> 4* c0(4) -> 4* c0(1) -> 4* c0(3) -> 4* 25(378) -> 379* 25(425) -> 426* c1(65) -> 66* c1(84) -> 85* c1(103) -> 104* 36(381) -> 382* 01(102) -> 103* R6(380) -> 381* R1(55) -> 56* R1(45) -> 46* R1(101) -> 102* R1(61) -> 62* R1(53) -> 54* 11(99) -> 100* 11(64) -> 65* 11(91) -> 92* 11(93) -> 94* 11(83) -> 84* b1(75) -> 76* b1(81) -> 82* b1(73) -> 74* b1(63) -> 64* 21(35) -> 36* 21(37) -> 38* 21(27) -> 28* 21(46) -> 47* 21(43) -> 44* L1(28) -> 29* L1(13) -> 14* 31(15) -> 16* 31(12) -> 13* 31(21) -> 22* 31(23) -> 24* L2(369) -> 370* L2(229) -> 230* L2(131) -> 132* L2(110) -> 111* 32(117) -> 118* 32(119) -> 120* 32(109) -> 110* 32(368) -> 369* 32(228) -> 229* 32(125) -> 126* c2(147) -> 148* c2(296) -> 297* c2(181) -> 182* c2(238) -> 239* c2(275) -> 276* 02(146) -> 147* 02(180) -> 181* R2(179) -> 180* R2(133) -> 134* R2(145) -> 146* 12(237) -> 238* 12(274) -> 275* 12(189) -> 190* 12(144) -> 145* 12(191) -> 192* 12(183) -> 184* 12(178) -> 179* 12(295) -> 296* 22(134) -> 135* 22(130) -> 131* L3(396) -> 397* L3(196) -> 197* L3(171) -> 172* L3(390) -> 391* L3(265) -> 266* L3(402) -> 403* 33(389) -> 390* 33(401) -> 402* 33(211) -> 212* 33(203) -> 204* 33(395) -> 396* 33(153) -> 154* 33(205) -> 206* 33(195) -> 196* 33(170) -> 171* 1 -> 93,75,55,37,21 2 -> 83,63,45,27,12 3 -> 99,81,61,43,23 4 -> 91,73,53,35,15 13 -> 228,130 14 -> 260,247,204,196,156,153,126,110,13,56,46,6,5 16 -> 13* 22 -> 13* 24 -> 13* 29 -> 28,7 36 -> 28* 38 -> 28* 44 -> 28* 47 -> 8* 54 -> 46* 56 -> 46* 62 -> 46* 63 -> 285* 64 -> 368,144 65 -> 237* 66 -> 247,162,153,62,46,5 73 -> 283* 74 -> 64* 75 -> 273* 76 -> 64* 81 -> 277* 82 -> 64* 83 -> 191,125 84 -> 295,101 85 -> 206,196,118,110,16,13,6 91 -> 183,117 92 -> 84* 93 -> 189,119 94 -> 84* 99 -> 178,109 100 -> 84* 104 -> 36,28,7 109 -> 161* 110 -> 401,133 111 -> 366,102 117 -> 152* 118 -> 110* 119 -> 155* 120 -> 110* 125 -> 163* 126 -> 110* 132 -> 131,47 135 -> 103* 144 -> 170* 148 -> 47,8 154 -> 134* 156 -> 153* 162 -> 153* 164 -> 153* 170 -> 222* 171 -> 216* 172 -> 146* 178 -> 211* 182 -> 131* 183 -> 205* 184 -> 179* 189 -> 195* 190 -> 179* 191 -> 203* 192 -> 179* 195 -> 259* 196 -> 234* 197 -> 180* 203 -> 253* 204 -> 196* 205 -> 255* 206 -> 196* 211 -> 246* 212 -> 196* 218 -> 147* 224 -> 217* 229 -> 264* 230 -> 402,248,235,229,154,134 236 -> 181* 237 -> 298* 239 -> 248,235,154,134 248 -> 235* 254 -> 247* 256 -> 247* 260 -> 247* 266 -> 420,236,265,135,103 274 -> 395* 275 -> 312* 276 -> 223* 278 -> 274* 284 -> 274* 286 -> 274* 295 -> 323* 297 -> 402,229 298 -> 306* 302 -> 236,135,103 306 -> 350* 307 -> 334* 308 -> 300* 312 -> 342* 314 -> 224,217 323 -> 328* 327 -> 420,265 328 -> 365* 329 -> 362* 330 -> 325* 336 -> 301* 342 -> 356* 346 -> 218,147 352 -> 335* 356 -> 380* 357 -> 377* 358 -> 344* 364 -> 326* 367 -> 363* 369 -> 389* 370 -> 351* 379 -> 345* 382 -> 378* 390 -> 407* 391 -> 352,335 396 -> 413* 397 -> 381* 402 -> 419* 403 -> 367,363 409 -> 336,301 414 -> 425* 415 -> 382,378 421 -> 364,326 427 -> 379,345 problem: Qed