YES(?,O(n^1)) 7.59/2.18 YES(?,O(n^1)) 7.59/2.19 7.59/2.19 Problem: 7.59/2.19 0(4(x1)) -> 0(1(4(2(3(3(x1)))))) 7.59/2.19 0(4(x1)) -> 0(2(1(4(3(4(x1)))))) 7.59/2.19 0(0(4(x1))) -> 1(1(5(2(3(4(x1)))))) 7.59/2.19 0(1(1(x1))) -> 0(2(2(1(1(1(x1)))))) 7.59/2.19 0(1(3(x1))) -> 0(2(4(3(4(4(x1)))))) 7.59/2.19 0(2(4(x1))) -> 1(5(4(3(4(4(x1)))))) 7.59/2.19 0(4(0(x1))) -> 0(1(2(1(0(3(x1)))))) 7.59/2.19 1(2(3(x1))) -> 5(1(4(1(4(4(x1)))))) 7.59/2.19 1(3(3(x1))) -> 0(2(1(1(0(5(x1)))))) 7.59/2.19 1(3(3(x1))) -> 5(4(0(3(2(3(x1)))))) 7.59/2.19 1(3(5(x1))) -> 1(1(4(3(3(2(x1)))))) 7.59/2.19 2(0(0(x1))) -> 2(4(3(4(4(4(x1)))))) 7.59/2.19 2(0(1(x1))) -> 2(1(5(1(0(1(x1)))))) 7.59/2.19 2(0(1(x1))) -> 2(4(3(5(2(3(x1)))))) 7.59/2.19 2(0(4(x1))) -> 2(0(2(1(4(3(x1)))))) 7.59/2.19 2(0(4(x1))) -> 2(4(1(4(3(1(x1)))))) 7.59/2.19 3(0(1(x1))) -> 3(1(4(3(4(1(x1)))))) 7.59/2.19 3(0(5(x1))) -> 3(1(0(2(3(2(x1)))))) 7.59/2.19 4(0(0(x1))) -> 2(5(2(1(1(1(x1)))))) 7.59/2.19 4(0(5(x1))) -> 4(1(4(5(1(4(x1)))))) 7.59/2.19 4(0(5(x1))) -> 4(2(1(4(3(5(x1)))))) 7.59/2.19 5(0(2(x1))) -> 1(5(2(1(0(2(x1)))))) 7.59/2.19 5(0(4(x1))) -> 1(0(3(2(4(4(x1)))))) 7.59/2.19 5(0(4(x1))) -> 1(5(1(0(3(4(x1)))))) 7.59/2.19 7.59/2.19 Proof: 7.59/2.19 Bounds Processor: 7.59/2.19 bound: 3 7.59/2.19 enrichment: match 7.59/2.19 automaton: 7.59/2.19 final states: {6,5,4,3,2,1} 7.59/2.19 transitions: 7.59/2.19 13(612) -> 613* 7.59/2.19 11(651) -> 652* 7.59/2.19 11(172) -> 173* 7.59/2.19 11(167) -> 168* 7.59/2.19 11(329) -> 330* 7.59/2.19 11(112) -> 113* 7.59/2.19 11(309) -> 310* 7.59/2.19 11(294) -> 295* 7.59/2.19 11(269) -> 270* 7.59/2.19 11(57) -> 58* 7.59/2.19 11(249) -> 250* 7.59/2.19 11(12) -> 13* 7.59/2.19 11(386) -> 387* 7.59/2.19 11(184) -> 185* 7.59/2.19 11(139) -> 140* 7.59/2.19 11(316) -> 317* 7.59/2.19 11(306) -> 307* 7.59/2.19 11(493) -> 494* 7.59/2.19 11(468) -> 469* 7.59/2.19 11(665) -> 666* 7.59/2.19 11(251) -> 252* 7.59/2.19 11(211) -> 212* 7.59/2.19 11(590) -> 591* 7.59/2.19 11(141) -> 142* 7.59/2.19 11(126) -> 127* 7.59/2.19 11(111) -> 112* 7.59/2.19 11(101) -> 102* 7.59/2.19 11(500) -> 501* 7.59/2.19 11(495) -> 496* 7.59/2.19 11(278) -> 279* 7.59/2.19 11(263) -> 264* 7.59/2.19 11(128) -> 129* 7.59/2.19 11(659) -> 660* 7.59/2.19 11(210) -> 211* 7.59/2.19 11(387) -> 388* 7.59/2.19 11(185) -> 186* 7.59/2.19 11(170) -> 171* 7.59/2.19 11(115) -> 116* 7.59/2.19 11(110) -> 111* 7.59/2.19 11(302) -> 303* 7.59/2.19 11(100) -> 101* 7.59/2.19 11(297) -> 298* 7.59/2.19 11(494) -> 495* 7.59/2.19 53(611) -> 612* 7.59/2.19 51(197) -> 198* 7.59/2.19 51(384) -> 385* 7.59/2.19 51(182) -> 183* 7.59/2.19 51(576) -> 577* 7.59/2.19 51(364) -> 365* 7.59/2.19 51(638) -> 639* 7.59/2.19 51(199) -> 200* 7.59/2.19 51(189) -> 190* 7.59/2.19 51(578) -> 579* 7.59/2.19 51(99) -> 100* 7.59/2.19 51(291) -> 292* 7.59/2.19 51(308) -> 309* 7.59/2.19 51(253) -> 254* 7.59/2.19 51(193) -> 194* 7.59/2.19 51(173) -> 174* 7.59/2.19 51(497) -> 498* 7.59/2.19 51(295) -> 296* 7.59/2.19 51(250) -> 251* 7.59/2.19 51(195) -> 196* 7.59/2.19 51(155) -> 156* 7.59/2.19 43(608) -> 609* 7.59/2.19 43(610) -> 611* 7.59/2.19 43(607) -> 608* 7.59/2.19 01(282) -> 283* 7.59/2.19 01(409) -> 410* 7.59/2.19 01(389) -> 390* 7.59/2.19 01(187) -> 188* 7.59/2.19 01(673) -> 674* 7.59/2.19 01(443) -> 444* 7.59/2.19 01(166) -> 167* 7.59/2.19 01(565) -> 566* 7.59/2.19 01(313) -> 314* 7.59/2.19 01(248) -> 249* 7.59/2.19 01(445) -> 446* 7.59/2.19 01(642) -> 643* 7.59/2.19 01(203) -> 204* 7.59/2.19 01(385) -> 386* 7.59/2.19 01(183) -> 184* 7.59/2.19 01(315) -> 316* 7.59/2.19 01(305) -> 306* 7.59/2.19 01(265) -> 266* 7.59/2.19 01(13) -> 14* 7.59/2.19 33(609) -> 610* 7.59/2.19 31(267) -> 268* 7.59/2.19 31(464) -> 465* 7.59/2.19 31(55) -> 56* 7.59/2.19 31(237) -> 238* 7.59/2.19 31(636) -> 637* 7.59/2.19 31(30) -> 31* 7.59/2.19 31(207) -> 208* 7.59/2.19 31(202) -> 203* 7.59/2.19 31(152) -> 153* 7.59/2.19 31(279) -> 280* 7.59/2.19 31(476) -> 477* 7.59/2.19 31(466) -> 467* 7.59/2.19 31(52) -> 53* 7.59/2.19 31(42) -> 43* 7.59/2.19 31(618) -> 619* 7.59/2.19 31(276) -> 277* 7.59/2.19 31(453) -> 454* 7.59/2.19 31(44) -> 45* 7.59/2.19 31(428) -> 429* 7.59/2.19 31(9) -> 10* 7.59/2.19 31(580) -> 581* 7.59/2.19 31(208) -> 209* 7.59/2.19 31(380) -> 381* 7.59/2.19 31(320) -> 321* 7.59/2.19 31(300) -> 301* 7.59/2.19 31(482) -> 483* 7.59/2.19 31(462) -> 463* 7.59/2.19 31(649) -> 650* 7.59/2.19 31(28) -> 29* 7.59/2.19 31(8) -> 9* 7.59/2.19 31(382) -> 383* 7.59/2.19 31(312) -> 313* 7.59/2.19 41(277) -> 278* 7.59/2.19 41(262) -> 263* 7.59/2.19 41(82) -> 83* 7.59/2.19 41(426) -> 427* 7.59/2.19 41(209) -> 210* 7.59/2.19 41(204) -> 205* 7.59/2.19 41(528) -> 529* 7.59/2.19 41(301) -> 302* 7.59/2.19 41(296) -> 297* 7.59/2.19 41(84) -> 85* 7.59/2.19 41(69) -> 70* 7.59/2.19 41(54) -> 55* 7.59/2.19 41(640) -> 641* 7.59/2.19 41(236) -> 237* 7.59/2.19 41(171) -> 172* 7.59/2.19 41(151) -> 152* 7.59/2.19 41(348) -> 349* 7.59/2.19 41(298) -> 299* 7.59/2.19 41(96) -> 97* 7.59/2.19 41(71) -> 72* 7.59/2.19 41(268) -> 269* 7.59/2.19 41(657) -> 658* 7.59/2.19 41(56) -> 57* 7.59/2.19 41(238) -> 239* 7.59/2.19 41(425) -> 426* 7.59/2.19 41(11) -> 12* 7.59/2.19 41(153) -> 154* 7.59/2.19 41(522) -> 523* 7.59/2.19 41(275) -> 276* 7.59/2.19 41(432) -> 433* 7.59/2.19 41(427) -> 428* 7.59/2.19 41(599) -> 600* 7.59/2.19 41(362) -> 363* 7.59/2.19 21(217) -> 218* 7.59/2.19 21(10) -> 11* 7.59/2.19 21(496) -> 497* 7.59/2.19 21(264) -> 265* 7.59/2.19 21(239) -> 240* 7.59/2.19 21(234) -> 235* 7.59/2.19 21(331) -> 332* 7.59/2.19 21(311) -> 312* 7.59/2.19 21(498) -> 499* 7.59/2.19 21(281) -> 282* 7.59/2.19 21(206) -> 207* 7.59/2.19 21(201) -> 202* 7.59/2.19 21(388) -> 389* 7.59/2.19 21(186) -> 187* 7.59/2.19 21(333) -> 334* 7.59/2.19 21(303) -> 304* 7.59/2.19 21(223) -> 224* 7.59/2.19 21(415) -> 416* 7.59/2.19 21(168) -> 169* 7.59/2.19 21(335) -> 336* 7.59/2.19 21(113) -> 114* 7.59/2.19 21(98) -> 99* 7.59/2.19 21(58) -> 59* 7.59/2.19 21(225) -> 226* 7.59/2.19 21(215) -> 216* 7.59/2.19 21(307) -> 308* 7.59/2.19 21(292) -> 293* 7.59/2.19 12(434) -> 435* 7.59/2.19 12(586) -> 587* 7.59/2.19 12(556) -> 557* 7.59/2.19 12(344) -> 345* 7.59/2.19 12(339) -> 340* 7.59/2.19 12(436) -> 437* 7.59/2.19 12(588) -> 589* 7.59/2.19 12(553) -> 554* 7.59/2.19 12(346) -> 347* 7.59/2.19 12(685) -> 686* 7.59/2.19 12(473) -> 474* 7.59/2.19 12(438) -> 439* 7.59/2.19 12(378) -> 379* 7.59/2.19 12(338) -> 339* 7.59/2.19 12(582) -> 583* 7.59/2.19 12(360) -> 361* 7.59/2.19 12(584) -> 585* 7.59/2.19 12(337) -> 338* 7.59/2.19 00(5) -> 1* 7.59/2.19 00(2) -> 1* 7.59/2.19 00(4) -> 1* 7.59/2.19 00(6) -> 1* 7.59/2.19 00(1) -> 1* 7.59/2.19 00(3) -> 1* 7.59/2.19 52(449) -> 450* 7.59/2.19 52(359) -> 360* 7.59/2.19 52(555) -> 556* 7.59/2.19 52(437) -> 438* 7.59/2.19 52(377) -> 378* 7.59/2.19 40(5) -> 2* 7.59/2.19 40(2) -> 2* 7.59/2.19 40(4) -> 2* 7.59/2.19 40(6) -> 2* 7.59/2.19 40(1) -> 2* 7.59/2.19 40(3) -> 2* 7.59/2.19 22(439) -> 440* 7.59/2.19 22(551) -> 552* 7.59/2.19 22(341) -> 342* 7.59/2.19 22(675) -> 676* 7.59/2.19 22(448) -> 449* 7.59/2.19 22(667) -> 668* 7.59/2.19 22(567) -> 568* 7.59/2.19 22(340) -> 341* 7.59/2.19 22(554) -> 555* 7.59/2.19 10(5) -> 3* 7.59/2.19 10(2) -> 3* 7.59/2.19 10(4) -> 3* 7.59/2.19 10(6) -> 3* 7.59/2.19 10(1) -> 3* 7.59/2.19 10(3) -> 3* 7.59/2.19 02(435) -> 436* 7.59/2.19 02(552) -> 553* 7.59/2.19 02(342) -> 343* 7.59/2.19 20(5) -> 4* 7.59/2.19 20(2) -> 4* 7.59/2.19 20(4) -> 4* 7.59/2.19 20(6) -> 4* 7.59/2.19 20(1) -> 4* 7.59/2.19 20(3) -> 4* 7.59/2.19 32(474) -> 475* 7.59/2.19 32(471) -> 472* 7.59/2.19 32(450) -> 451* 7.59/2.19 32(375) -> 376* 7.59/2.19 32(447) -> 448* 7.59/2.19 32(357) -> 358* 7.59/2.19 32(352) -> 353* 7.59/2.19 30(5) -> 5* 7.59/2.19 30(2) -> 5* 7.59/2.19 30(4) -> 5* 7.59/2.19 30(6) -> 5* 7.59/2.19 30(1) -> 5* 7.59/2.19 30(3) -> 5* 7.59/2.19 42(626) -> 627* 7.59/2.19 42(374) -> 375* 7.59/2.19 42(451) -> 452* 7.59/2.19 42(628) -> 629* 7.59/2.19 42(376) -> 377* 7.59/2.19 42(356) -> 357* 7.59/2.19 42(351) -> 352* 7.59/2.19 42(620) -> 621* 7.59/2.19 42(605) -> 606* 7.59/2.19 42(373) -> 374* 7.59/2.19 42(358) -> 359* 7.59/2.19 42(353) -> 354* 7.59/2.19 42(470) -> 471* 7.59/2.19 42(632) -> 633* 7.59/2.19 42(355) -> 356* 7.59/2.19 42(350) -> 351* 7.59/2.19 42(472) -> 473* 7.59/2.19 50(5) -> 6* 7.59/2.19 50(2) -> 6* 7.59/2.19 50(4) -> 6* 7.59/2.19 50(6) -> 6* 7.59/2.19 50(1) -> 6* 7.59/2.19 50(3) -> 6* 7.59/2.19 1 -> 225,197,139,84,44 7.59/2.19 2 -> 215,189,115,69,28 7.59/2.19 3 -> 234,199,141,96,52 7.59/2.19 4 -> 217,193,126,71,30 7.59/2.19 5 -> 206,182,110,54,8 7.59/2.19 6 -> 223,195,128,82,42 7.59/2.19 9 -> 262,201,166 7.59/2.19 12 -> 466,447,434 7.59/2.19 13 -> 493,425,380 7.59/2.19 14 -> 249,1 7.59/2.19 29 -> 9* 7.59/2.19 31 -> 9* 7.59/2.19 43 -> 9* 7.59/2.19 45 -> 9* 7.59/2.19 53 -> 9* 7.59/2.19 55 -> 294,151 7.59/2.19 56 -> 315,98 7.59/2.19 57 -> 364* 7.59/2.19 58 -> 567,476 7.59/2.19 59 -> 13* 7.59/2.19 70 -> 55* 7.59/2.19 72 -> 55* 7.59/2.19 83 -> 55* 7.59/2.19 85 -> 55* 7.59/2.19 97 -> 55* 7.59/2.19 100 -> 584* 7.59/2.19 101 -> 462,337 7.59/2.19 102 -> 445,306,1 7.59/2.19 111 -> 275,267,248 7.59/2.19 112 -> 333* 7.59/2.19 114 -> 291,58 7.59/2.19 116 -> 111* 7.59/2.19 127 -> 111* 7.59/2.19 129 -> 111* 7.59/2.19 140 -> 335,111 7.59/2.19 142 -> 331,111 7.59/2.19 152 -> 311,236,170 7.59/2.19 153 -> 355* 7.59/2.19 154 -> 155,58 7.59/2.19 156 -> 101* 7.59/2.19 169 -> 12* 7.59/2.19 173 -> 522,415 7.59/2.19 174 -> 127,111,248,275,3 7.59/2.19 183 -> 300* 7.59/2.19 186 -> 551* 7.59/2.19 187 -> 500,432,382 7.59/2.19 188 -> 111,267,248,275,3 7.59/2.20 190 -> 183* 7.59/2.20 194 -> 183* 7.59/2.20 196 -> 183* 7.59/2.20 198 -> 183* 7.59/2.20 200 -> 183* 7.59/2.20 202 -> 253* 7.59/2.20 204 -> 628* 7.59/2.20 205 -> 173* 7.59/2.20 207 -> 305* 7.59/2.20 208 -> 409,281 7.59/2.20 210 -> 586* 7.59/2.20 211 -> 464,344 7.59/2.20 212 -> 111,267,248,275,3 7.59/2.20 216 -> 207* 7.59/2.20 218 -> 207* 7.59/2.20 224 -> 207* 7.59/2.20 226 -> 207* 7.59/2.20 235 -> 207* 7.59/2.20 238 -> 626* 7.59/2.20 239 -> 362* 7.59/2.20 240 -> 226,207,305,4 7.59/2.20 252 -> 239* 7.59/2.20 254 -> 329,237 7.59/2.20 264 -> 675* 7.59/2.20 265 -> 528* 7.59/2.20 266 -> 1,84,197,225,139,44,239 7.59/2.20 270 -> 238* 7.59/2.20 279 -> 384,350,348 7.59/2.20 280 -> 45,9,166,262,5 7.59/2.20 283 -> 278* 7.59/2.20 293 -> 565,85,55,294,2 7.59/2.20 298 -> 468,373,320 7.59/2.20 299 -> 85,55,294,2 7.59/2.20 304 -> 298* 7.59/2.20 309 -> 453,346 7.59/2.20 310 -> 198,183,443,6 7.59/2.20 314 -> 309* 7.59/2.20 317 -> 308* 7.59/2.20 321 -> 9* 7.59/2.20 329 -> 582* 7.59/2.20 330 -> 101* 7.59/2.20 332 -> 576,58 7.59/2.20 334 -> 58* 7.59/2.20 336 -> 578,58 7.59/2.20 343 -> 446,249 7.59/2.20 345 -> 338* 7.59/2.20 347 -> 338* 7.59/2.20 349 -> 151* 7.59/2.20 353 -> 607* 7.59/2.20 354 -> 341* 7.59/2.20 360 -> 649,590 7.59/2.20 361 -> 553,588,14 7.59/2.20 363 -> 152* 7.59/2.20 365 -> 101* 7.59/2.20 379 -> 306* 7.59/2.20 381 -> 166* 7.59/2.20 383 -> 166* 7.59/2.20 388 -> 667* 7.59/2.20 389 -> 665,640,636 7.59/2.20 390 -> 111,267,3,199,96,52,141,234,248,275 7.59/2.20 410 -> 204* 7.59/2.20 416 -> 226,4,207 7.59/2.20 426 -> 482* 7.59/2.20 429 -> 204* 7.59/2.20 433 -> 151* 7.59/2.20 435 -> 470* 7.59/2.20 440 -> 226,207,305 7.59/2.20 444 -> 249* 7.59/2.20 446 -> 249* 7.59/2.20 452 -> 620,439 7.59/2.20 454 -> 201* 7.59/2.20 463 -> 201* 7.59/2.20 465 -> 201* 7.59/2.20 467 -> 201* 7.59/2.20 469 -> 267* 7.59/2.20 475 -> 45,9,166,262 7.59/2.20 476 -> 638,605,599 7.59/2.20 477 -> 45,9,5,166,262 7.59/2.20 483 -> 277* 7.59/2.20 499 -> 673,85,2,189,69,28,115,215,55,294 7.59/2.20 501 -> 111* 7.59/2.20 523 -> 618,294 7.59/2.20 528 -> 651,632,580 7.59/2.20 529 -> 85,2,189,69,28,115,215,55,294 7.59/2.20 557 -> 198,200 7.59/2.20 566 -> 306* 7.59/2.20 568 -> 552* 7.59/2.20 577 -> 309* 7.59/2.20 579 -> 309* 7.59/2.20 581 -> 9* 7.59/2.20 583 -> 338* 7.59/2.20 585 -> 338* 7.59/2.20 587 -> 338* 7.59/2.20 589 -> 339* 7.59/2.20 590 -> 685* 7.59/2.20 591 -> 657,642,101 7.59/2.20 600 -> 151* 7.59/2.20 606 -> 351* 7.59/2.20 613 -> 343* 7.59/2.20 619 -> 56* 7.59/2.20 621 -> 375* 7.59/2.20 627 -> 374* 7.59/2.20 629 -> 374* 7.59/2.20 633 -> 374* 7.59/2.20 637 -> 166* 7.59/2.20 639 -> 183* 7.59/2.20 641 -> 151* 7.59/2.20 643 -> 249* 7.59/2.20 650 -> 201* 7.59/2.20 652 -> 659,267 7.59/2.20 658 -> 55* 7.59/2.20 660 -> 112* 7.59/2.20 666 -> 111* 7.59/2.20 668 -> 552* 7.59/2.20 674 -> 139* 7.59/2.20 676 -> 552* 7.59/2.20 686 -> 338* 7.59/2.20 problem: 7.59/2.20 7.59/2.20 Qed 7.59/2.20 EOF