YES(?,O(n^1))
9.33/3.16	YES(?,O(n^1))
9.33/3.17	
9.33/3.17	Problem:
9.33/3.17	 2(5(3(0(x1)))) -> 1(0(0(1(3(0(4(5(1(2(x1))))))))))
9.33/3.17	 1(3(5(4(3(x1))))) -> 2(1(4(1(4(0(3(0(1(1(x1))))))))))
9.33/3.17	 5(1(3(5(0(x1))))) -> 5(1(4(3(0(4(4(5(2(1(x1))))))))))
9.33/3.17	 5(4(4(2(5(x1))))) -> 4(3(1(1(1(1(5(3(3(5(x1))))))))))
9.33/3.17	 2(2(5(0(5(4(x1)))))) -> 2(1(4(1(3(3(2(2(5(4(x1))))))))))
9.33/3.17	 3(0(5(5(4(3(x1)))))) -> 3(3(0(3(2(3(5(5(1(0(x1))))))))))
9.33/3.17	 3(5(4(3(5(2(x1)))))) -> 2(0(5(2(0(5(2(2(3(2(x1))))))))))
9.33/3.17	 4(4(2(5(5(0(x1)))))) -> 4(4(0(0(3(3(3(2(2(3(x1))))))))))
9.33/3.17	 4(5(3(5(5(0(x1)))))) -> 4(2(2(3(0(2(4(1(1(5(x1))))))))))
9.33/3.17	 5(4(5(1(1(2(x1)))))) -> 5(4(0(3(3(3(3(2(5(5(x1))))))))))
9.33/3.17	 5(5(5(5(5(3(x1)))))) -> 5(5(0(1(4(0(0(5(0(1(x1))))))))))
9.33/3.17	 3(5(0(0(5(4(3(x1))))))) -> 0(1(2(1(1(5(5(2(1(0(x1))))))))))
9.33/3.17	 3(5(4(2(5(2(3(x1))))))) -> 4(0(4(0(0(2(2(3(4(4(x1))))))))))
9.33/3.17	 3(5(4(5(1(4(0(x1))))))) -> 1(1(1(0(0(3(3(1(2(5(x1))))))))))
9.33/3.17	
9.33/3.17	Proof:
9.33/3.17	 Bounds Processor:
9.33/3.17	  bound: 2
9.33/3.17	  enrichment: match
9.33/3.17	  automaton:
9.33/3.17	   final states: {7}
9.33/3.17	   transitions:
9.33/3.17	    11(277) -> 278*
9.33/3.17	    11(60) -> 61*
9.33/3.17	    11(247) -> 248*
9.33/3.17	    11(30) -> 31*
9.33/3.17	    11(25) -> 26*
9.33/3.17	    11(20) -> 21*
9.33/3.17	    11(192) -> 193*
9.33/3.17	    11(62) -> 63*
9.33/3.17	    11(456) -> 457*
9.33/3.17	    11(254) -> 255*
9.33/3.17	    11(52) -> 53*
9.33/3.17	    11(239) -> 240*
9.33/3.17	    11(391) -> 392*
9.33/3.17	    11(159) -> 160*
9.33/3.17	    11(124) -> 125*
9.33/3.17	    11(59) -> 60*
9.33/3.17	    11(216) -> 217*
9.33/3.17	    11(191) -> 192*
9.33/3.17	    11(186) -> 187*
9.33/3.17	    11(161) -> 162*
9.33/3.17	    11(151) -> 152*
9.33/3.17	    11(61) -> 62*
9.33/3.17	    11(455) -> 456*
9.33/3.17	    11(450) -> 451*
9.33/3.17	    11(36) -> 37*
9.33/3.17	    11(31) -> 32*
9.33/3.17	    11(213) -> 214*
9.33/3.17	    11(208) -> 209*
9.33/3.17	    11(158) -> 159*
9.33/3.17	    11(78) -> 79*
9.33/3.17	    11(457) -> 458*
9.33/3.17	    11(245) -> 246*
9.33/3.17	    11(240) -> 241*
9.33/3.17	    11(38) -> 39*
9.33/3.17	    11(28) -> 29*
9.33/3.17	    11(554) -> 555*
9.33/3.17	    11(125) -> 126*
9.33/3.17	    01(282) -> 283*
9.33/3.17	    01(454) -> 455*
9.33/3.17	    01(566) -> 567*
9.33/3.17	    01(162) -> 163*
9.33/3.17	    01(152) -> 153*
9.33/3.17	    01(117) -> 118*
9.33/3.17	    01(77) -> 78*
9.33/3.17	    01(32) -> 33*
9.33/3.17	    01(27) -> 28*
9.33/3.17	    01(426) -> 427*
9.33/3.17	    01(416) -> 417*
9.33/3.17	    01(214) -> 215*
9.33/3.17	    01(189) -> 190*
9.33/3.17	    01(149) -> 150*
9.33/3.17	    01(139) -> 140*
9.33/3.17	    01(84) -> 85*
9.33/3.17	    01(453) -> 454*
9.33/3.17	    01(49) -> 50*
9.33/3.17	    01(443) -> 444*
9.33/3.17	    01(241) -> 242*
9.33/3.17	    01(34) -> 35*
9.33/3.17	    01(211) -> 212*
9.33/3.17	    01(393) -> 394*
9.33/3.17	    01(181) -> 182*
9.33/3.17	    01(146) -> 147*
9.33/3.17	    01(116) -> 117*
9.33/3.17	    01(445) -> 446*
9.33/3.17	    01(243) -> 244*
9.33/3.17	    01(26) -> 27*
9.33/3.17	    01(395) -> 396*
9.33/3.17	    01(183) -> 184*
9.33/3.17	    01(148) -> 149*
9.33/3.17	    01(128) -> 129*
9.33/3.17	    01(108) -> 109*
9.33/3.17	    01(442) -> 443*
9.33/3.17	    01(23) -> 24*
9.33/3.17	    01(215) -> 216*
9.33/3.17	    01(190) -> 191*
9.33/3.17	    01(180) -> 181*
9.33/3.17	    01(105) -> 106*
9.33/3.17	    31(75) -> 76*
9.33/3.17	    31(50) -> 51*
9.33/3.17	    31(242) -> 243*
9.33/3.17	    31(439) -> 440*
9.33/3.17	    31(414) -> 415*
9.33/3.17	    31(212) -> 213*
9.33/3.17	    31(389) -> 390*
9.33/3.17	    31(187) -> 188*
9.33/3.17	    31(177) -> 178*
9.33/3.17	    31(137) -> 138*
9.33/3.17	    31(57) -> 58*
9.33/3.17	    31(451) -> 452*
9.33/3.17	    31(129) -> 130*
9.33/3.17	    31(114) -> 115*
9.33/3.17	    31(74) -> 75*
9.33/3.17	    31(24) -> 25*
9.33/3.17	    31(418) -> 419*
9.33/3.17	    31(413) -> 414*
9.33/3.17	    31(580) -> 581*
9.33/3.17	    31(136) -> 137*
9.33/3.17	    31(101) -> 102*
9.33/3.17	    31(86) -> 87*
9.33/3.17	    31(283) -> 284*
9.33/3.17	    31(81) -> 82*
9.33/3.17	    31(56) -> 57*
9.33/3.17	    31(415) -> 416*
9.33/3.17	    31(410) -> 411*
9.33/3.17	    31(390) -> 391*
9.33/3.17	    31(188) -> 189*
9.33/3.17	    31(138) -> 139*
9.33/3.17	    31(113) -> 114*
9.33/3.17	    31(83) -> 84*
9.33/3.17	    31(63) -> 64*
9.33/3.17	    31(452) -> 453*
9.33/3.17	    31(33) -> 34*
9.33/3.17	    31(135) -> 136*
9.33/3.17	    31(115) -> 116*
9.33/3.17	    31(110) -> 111*
9.33/3.17	    31(85) -> 86*
9.33/3.17	    21(459) -> 460*
9.33/3.17	    21(449) -> 450*
9.33/3.17	    21(45) -> 46*
9.33/3.17	    21(207) -> 208*
9.33/3.17	    21(127) -> 128*
9.33/3.17	    21(112) -> 113*
9.33/3.17	    21(102) -> 103*
9.33/3.17	    21(82) -> 83*
9.33/3.17	    21(72) -> 73*
9.33/3.17	    21(441) -> 442*
9.33/3.17	    21(411) -> 412*
9.33/3.17	    21(179) -> 180*
9.33/3.17	    21(134) -> 135*
9.33/3.17	    21(39) -> 40*
9.33/3.17	    21(19) -> 20*
9.33/3.17	    21(388) -> 389*
9.33/3.17	    21(131) -> 132*
9.33/3.17	    21(111) -> 112*
9.33/3.17	    21(106) -> 107*
9.33/3.17	    21(278) -> 279*
9.33/3.17	    21(248) -> 249*
9.33/3.17	    21(440) -> 441*
9.33/3.17	    21(178) -> 179*
9.33/3.17	    21(103) -> 104*
9.33/3.17	    21(73) -> 74*
9.33/3.17	    21(412) -> 413*
9.33/3.17	    21(185) -> 186*
9.33/3.17	    21(160) -> 161*
9.33/3.17	    21(155) -> 156*
9.33/3.17	    21(130) -> 131*
9.33/3.17	    51(80) -> 81*
9.33/3.17	    51(55) -> 56*
9.33/3.17	    51(424) -> 425*
9.33/3.17	    51(157) -> 158*
9.33/3.17	    51(556) -> 557*
9.33/3.17	    51(147) -> 148*
9.33/3.17	    51(516) -> 517*
9.33/3.17	    51(107) -> 108*
9.33/3.17	    51(279) -> 280*
9.33/3.17	    51(209) -> 210*
9.33/3.17	    51(518) -> 519*
9.33/3.17	    51(104) -> 105*
9.33/3.17	    51(79) -> 80*
9.33/3.17	    51(448) -> 449*
9.33/3.17	    51(156) -> 157*
9.33/3.17	    51(71) -> 72*
9.33/3.17	    51(46) -> 47*
9.33/3.17	    51(21) -> 22*
9.33/3.17	    51(420) -> 421*
9.33/3.17	    51(153) -> 154*
9.33/3.17	    51(552) -> 553*
9.33/3.17	    51(133) -> 134*
9.33/3.17	    51(58) -> 59*
9.33/3.17	    51(53) -> 54*
9.33/3.17	    51(422) -> 423*
9.33/3.17	    51(584) -> 585*
9.33/3.17	    51(494) -> 495*
9.33/3.17	    41(70) -> 71*
9.33/3.17	    41(444) -> 445*
9.33/3.17	    41(35) -> 36*
9.33/3.17	    41(182) -> 183*
9.33/3.17	    41(284) -> 285*
9.33/3.17	    41(47) -> 48*
9.33/3.17	    41(446) -> 447*
9.33/3.17	    41(244) -> 245*
9.33/3.17	    41(37) -> 38*
9.33/3.17	    41(22) -> 23*
9.33/3.17	    41(281) -> 282*
9.33/3.17	    41(64) -> 65*
9.33/3.17	    41(246) -> 247*
9.33/3.17	    41(438) -> 439*
9.33/3.17	    41(176) -> 177*
9.33/3.17	    41(560) -> 561*
9.33/3.17	    41(126) -> 127*
9.33/3.17	    41(51) -> 52*
9.33/3.17	    41(562) -> 563*
9.33/3.17	    41(118) -> 119*
9.33/3.17	    41(280) -> 281*
9.33/3.17	    41(48) -> 49*
9.33/3.17	    41(437) -> 438*
9.33/3.17	    41(210) -> 211*
9.33/3.17	    41(150) -> 151*
9.33/3.17	    41(140) -> 141*
9.33/3.17	    42(541) -> 542*
9.33/3.17	    42(511) -> 512*
9.33/3.17	    42(548) -> 549*
9.33/3.17	    42(550) -> 551*
9.33/3.17	    42(525) -> 526*
9.33/3.17	    42(490) -> 491*
9.33/3.17	    42(542) -> 543*
9.33/3.17	    42(512) -> 513*
9.33/3.17	    20(7) -> 7*
9.33/3.17	    02(546) -> 547*
9.33/3.17	    02(521) -> 522*
9.33/3.17	    02(523) -> 524*
9.33/3.17	    02(510) -> 511*
9.33/3.17	    02(547) -> 548*
9.33/3.17	    02(527) -> 528*
9.33/3.17	    02(549) -> 550*
9.33/3.17	    02(524) -> 525*
9.33/3.17	    02(509) -> 510*
9.33/3.17	    50(7) -> 7*
9.33/3.17	    22(545) -> 546*
9.33/3.17	    22(505) -> 506*
9.33/3.17	    22(544) -> 545*
9.33/3.17	    22(504) -> 505*
9.33/3.17	    30(7) -> 7*
9.33/3.17	    32(489) -> 490*
9.33/3.17	    32(506) -> 507*
9.33/3.17	    32(578) -> 579*
9.33/3.17	    32(543) -> 544*
9.33/3.17	    32(508) -> 509*
9.33/3.17	    32(503) -> 504*
9.33/3.17	    32(483) -> 484*
9.33/3.17	    32(507) -> 508*
9.33/3.17	    32(482) -> 483*
9.33/3.17	    32(514) -> 515*
9.33/3.17	    00(7) -> 7*
9.33/3.17	    52(484) -> 485*
9.33/3.17	    52(481) -> 482*
9.33/3.17	    52(528) -> 529*
9.33/3.17	    52(522) -> 523*
9.33/3.17	    52(492) -> 493*
9.33/3.17	    52(594) -> 595*
9.33/3.17	    52(529) -> 530*
9.33/3.17	    10(7) -> 7*
9.33/3.17	    12(526) -> 527*
9.33/3.17	    12(486) -> 487*
9.33/3.17	    12(488) -> 489*
9.33/3.17	    12(520) -> 521*
9.33/3.17	    12(485) -> 486*
9.33/3.17	    12(487) -> 488*
9.33/3.17	    40(7) -> 7*
9.33/3.17	    7 -> 110,77,70,55,30,19
9.33/3.17	    19 -> 516*
9.33/3.17	    20 -> 7,77,55,19,30,70,110,388,101
9.33/3.17	    29 -> 483,57,111,20,186,101,7
9.33/3.17	    31 -> 146,45
9.33/3.17	    39 -> 424*
9.33/3.17	    40 -> 483,57,111,20,101,31,45,146,7
9.33/3.17	    53 -> 492*
9.33/3.17	    54 -> 493,517,134,72,56,133,124,185,7
9.33/3.17	    55 -> 481*
9.33/3.17	    56 -> 482,7,77,55,19,30,70,110,185,133,124
9.33/3.17	    63 -> 393,239
9.33/3.17	    65 -> 483,517,57,111,71,177,176,56,133,72,124,185,7
9.33/3.17	    71 -> 7,176
9.33/3.17	    76 -> 36*
9.33/3.17	    79 -> 155*
9.33/3.17	    86 -> 541,520,437,395,254
9.33/3.17	    87 -> 111,7
9.33/3.17	    109 -> 39*
9.33/3.17	    113 -> 494*
9.33/3.17	    119 -> 64*
9.33/3.17	    132 -> 64*
9.33/3.17	    141 -> 53*
9.33/3.17	    152 -> 514,420,410
9.33/3.17	    154 -> 53*
9.33/3.17	    162 -> 503,422,418,277,207
9.33/3.17	    163 -> 483,57,111,7
9.33/3.17	    183 -> 448*
9.33/3.17	    184 -> 64*
9.33/3.17	    193 -> 28*
9.33/3.17	    217 -> 20,186,7,101
9.33/3.17	    248 -> 518*
9.33/3.17	    249 -> 31,45,7,146
9.33/3.17	    255 -> 426,240
9.33/3.17	    285 -> 28*
9.33/3.17	    392 -> 284*
9.33/3.17	    394 -> 78*
9.33/3.17	    396 -> 78*
9.33/3.17	    417 -> 183*
9.33/3.17	    419 -> 411*
9.33/3.17	    421 -> 124*
9.33/3.17	    423 -> 459,124
9.33/3.17	    425 -> 133*
9.33/3.17	    427 -> 147*
9.33/3.17	    445 -> 552*
9.33/3.17	    447 -> 483,57,7,77,55,19,30,70,110,111
9.33/3.17	    458 -> 483,57,7,77,55,19,30,70,110,111
9.33/3.17	    460 -> 450*
9.33/3.17	    489 -> 566,554
9.33/3.17	    490 -> 560*
9.33/3.17	    491 -> 517,56,133,72,7,124,185
9.33/3.17	    493 -> 482*
9.33/3.17	    495 -> 105*
9.33/3.17	    512 -> 562*
9.33/3.17	    513 -> 71,177,7,176
9.33/3.17	    515 -> 504*
9.33/3.17	    517 -> 53*
9.33/3.17	    519 -> 53*
9.33/3.17	    527 -> 584,580,578
9.33/3.17	    529 -> 556*
9.33/3.17	    530 -> 493,54,492,56,133,134,7,124,185
9.33/3.17	    551 -> 483,57,111
9.33/3.17	    553 -> 185*
9.33/3.17	    555 -> 31*
9.33/3.17	    556 -> 594*
9.33/3.17	    557 -> 56*
9.33/3.17	    561 -> 53*
9.33/3.17	    563 -> 53*
9.33/3.17	    567 -> 78*
9.33/3.17	    579 -> 504*
9.33/3.17	    581 -> 111*
9.33/3.17	    585 -> 124*
9.33/3.17	    595 -> 482*
9.33/3.17	  problem:
9.33/3.17	   
9.33/3.17	  Qed
9.33/3.17	EOF