YES(?,O(n^1))
4.35/1.37	YES(?,O(n^1))
4.35/1.38	
4.35/1.38	Problem:
4.35/1.38	 0(1(2(3(4(5(1(x1))))))) -> 0(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))
4.35/1.38	 0(1(2(3(4(5(1(x1))))))) ->
4.35/1.38	 1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))))))))
4.35/1.38	 0(1(2(3(4(5(1(x1))))))) ->
4.35/1.38	 1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x1)))))))))))))))))))))))))))))))
4.35/1.38	
4.35/1.38	Proof:
4.35/1.38	 Bounds Processor:
4.35/1.38	  bound: 3
4.35/1.38	  enrichment: match
4.35/1.38	  automaton:
4.35/1.38	   final states: {7}
4.35/1.38	   transitions:
4.35/1.38	    13(394) -> 395*
4.35/1.38	    13(496) -> 497*
4.35/1.38	    13(451) -> 452*
4.35/1.38	    13(386) -> 387*
4.35/1.38	    13(356) -> 357*
4.35/1.38	    13(351) -> 352*
4.35/1.38	    13(331) -> 332*
4.35/1.38	    13(498) -> 499*
4.35/1.38	    13(448) -> 449*
4.35/1.38	    13(418) -> 419*
4.35/1.38	    13(413) -> 414*
4.35/1.38	    13(348) -> 349*
4.35/1.38	    13(328) -> 329*
4.35/1.38	    13(450) -> 451*
4.35/1.38	    13(410) -> 411*
4.35/1.38	    13(395) -> 396*
4.35/1.38	    13(350) -> 351*
4.35/1.38	    13(330) -> 331*
4.35/1.38	    13(442) -> 443*
4.35/1.38	    13(412) -> 413*
4.35/1.38	    13(392) -> 393*
4.35/1.38	    13(322) -> 323*
4.35/1.38	    13(504) -> 505*
4.35/1.38	    13(499) -> 500*
4.35/1.38	    11(60) -> 61*
4.35/1.38	    11(55) -> 56*
4.35/1.38	    11(40) -> 41*
4.35/1.38	    11(52) -> 53*
4.35/1.38	    11(32) -> 33*
4.35/1.38	    11(54) -> 55*
4.35/1.38	    11(41) -> 42*
4.35/1.38	    11(38) -> 39*
4.35/1.38	    23(409) -> 410*
4.35/1.38	    23(399) -> 400*
4.35/1.38	    23(441) -> 442*
4.35/1.38	    23(391) -> 392*
4.35/1.38	    23(321) -> 322*
4.35/1.38	    23(503) -> 504*
4.35/1.38	    23(495) -> 496*
4.35/1.38	    23(455) -> 456*
4.35/1.38	    23(385) -> 386*
4.35/1.38	    23(355) -> 356*
4.35/1.38	    23(335) -> 336*
4.35/1.38	    23(447) -> 448*
4.35/1.38	    23(417) -> 418*
4.35/1.38	    23(347) -> 348*
4.35/1.38	    23(327) -> 328*
4.35/1.38	    21(45) -> 46*
4.35/1.38	    21(37) -> 38*
4.35/1.38	    21(59) -> 60*
4.35/1.38	    21(51) -> 52*
4.35/1.38	    21(31) -> 32*
4.35/1.38	    33(494) -> 495*
4.35/1.38	    33(454) -> 455*
4.35/1.38	    33(384) -> 385*
4.35/1.38	    33(354) -> 355*
4.35/1.38	    33(334) -> 335*
4.35/1.38	    33(446) -> 447*
4.35/1.38	    33(416) -> 417*
4.35/1.38	    33(346) -> 347*
4.35/1.38	    33(326) -> 327*
4.35/1.38	    33(408) -> 409*
4.35/1.38	    33(398) -> 399*
4.35/1.38	    33(440) -> 441*
4.35/1.38	    33(390) -> 391*
4.35/1.38	    33(320) -> 321*
4.35/1.38	    33(502) -> 503*
4.35/1.38	    31(50) -> 51*
4.35/1.38	    31(30) -> 31*
4.35/1.38	    31(44) -> 45*
4.35/1.38	    31(36) -> 37*
4.35/1.38	    31(58) -> 59*
4.35/1.38	    43(439) -> 440*
4.35/1.38	    43(389) -> 390*
4.35/1.38	    43(319) -> 320*
4.35/1.38	    43(501) -> 502*
4.35/1.38	    43(493) -> 494*
4.35/1.38	    43(453) -> 454*
4.35/1.38	    43(383) -> 384*
4.35/1.38	    43(353) -> 354*
4.35/1.38	    43(333) -> 334*
4.35/1.38	    43(445) -> 446*
4.35/1.38	    43(415) -> 416*
4.35/1.38	    43(345) -> 346*
4.35/1.38	    43(325) -> 326*
4.35/1.38	    43(407) -> 408*
4.35/1.38	    43(397) -> 398*
4.35/1.38	    41(35) -> 36*
4.35/1.38	    41(57) -> 58*
4.35/1.38	    41(49) -> 50*
4.35/1.38	    41(29) -> 30*
4.35/1.38	    41(43) -> 44*
4.35/1.38	    53(444) -> 445*
4.35/1.38	    53(414) -> 415*
4.35/1.38	    53(344) -> 345*
4.35/1.38	    53(324) -> 325*
4.35/1.38	    53(436) -> 437*
4.35/1.38	    53(406) -> 407*
4.35/1.38	    53(396) -> 397*
4.35/1.38	    53(528) -> 529*
4.35/1.38	    53(438) -> 439*
4.35/1.38	    53(388) -> 389*
4.35/1.38	    53(358) -> 359*
4.35/1.38	    53(318) -> 319*
4.35/1.38	    53(500) -> 501*
4.35/1.38	    53(340) -> 341*
4.35/1.38	    53(492) -> 493*
4.35/1.38	    53(452) -> 453*
4.35/1.38	    53(382) -> 383*
4.35/1.38	    53(352) -> 353*
4.35/1.38	    53(544) -> 545*
4.35/1.38	    53(342) -> 343*
4.35/1.38	    53(332) -> 333*
4.35/1.38	    51(42) -> 43*
4.35/1.38	    51(74) -> 75*
4.35/1.38	    51(34) -> 35*
4.35/1.38	    51(66) -> 67*
4.35/1.38	    51(56) -> 57*
4.35/1.38	    51(68) -> 69*
4.35/1.38	    51(48) -> 49*
4.35/1.38	    51(28) -> 29*
4.35/1.38	    03(449) -> 450*
4.35/1.38	    03(349) -> 350*
4.35/1.38	    03(329) -> 330*
4.35/1.38	    03(456) -> 457*
4.35/1.38	    03(411) -> 412*
4.35/1.38	    03(336) -> 337*
4.35/1.38	    03(443) -> 444*
4.35/1.38	    03(393) -> 394*
4.35/1.38	    03(323) -> 324*
4.35/1.38	    03(400) -> 401*
4.35/1.38	    03(497) -> 498*
4.35/1.38	    03(387) -> 388*
4.35/1.38	    01(39) -> 40*
4.35/1.38	    01(46) -> 47*
4.35/1.38	    01(53) -> 54*
4.35/1.38	    01(33) -> 34*
4.35/1.38	    12(80) -> 81*
4.35/1.38	    12(257) -> 258*
4.35/1.38	    12(167) -> 168*
4.35/1.38	    12(254) -> 255*
4.35/1.38	    12(204) -> 205*
4.35/1.38	    12(199) -> 200*
4.35/1.38	    12(164) -> 165*
4.35/1.38	    12(124) -> 125*
4.35/1.38	    12(119) -> 120*
4.35/1.38	    12(89) -> 90*
4.35/1.38	    12(256) -> 257*
4.35/1.38	    12(196) -> 197*
4.35/1.38	    12(166) -> 167*
4.35/1.38	    12(116) -> 117*
4.35/1.38	    12(298) -> 299*
4.35/1.38	    12(293) -> 294*
4.35/1.38	    12(86) -> 87*
4.35/1.38	    12(248) -> 249*
4.35/1.38	    12(198) -> 199*
4.35/1.38	    12(158) -> 159*
4.35/1.38	    12(118) -> 119*
4.35/1.38	    12(290) -> 291*
4.35/1.38	    12(88) -> 89*
4.35/1.38	    12(292) -> 293*
4.35/1.38	    00(7) -> 7*
4.35/1.38	    22(85) -> 86*
4.35/1.38	    22(247) -> 248*
4.35/1.38	    22(157) -> 158*
4.35/1.38	    22(289) -> 290*
4.35/1.38	    22(79) -> 80*
4.35/1.38	    22(261) -> 262*
4.35/1.38	    22(171) -> 172*
4.35/1.38	    22(253) -> 254*
4.35/1.38	    22(203) -> 204*
4.35/1.38	    22(163) -> 164*
4.35/1.38	    22(123) -> 124*
4.35/1.38	    22(93) -> 94*
4.35/1.38	    22(195) -> 196*
4.35/1.38	    22(115) -> 116*
4.35/1.38	    22(297) -> 298*
4.35/1.38	    10(7) -> 7*
4.35/1.38	    32(252) -> 253*
4.35/1.38	    32(202) -> 203*
4.35/1.38	    32(162) -> 163*
4.35/1.38	    32(122) -> 123*
4.35/1.38	    32(92) -> 93*
4.35/1.38	    32(194) -> 195*
4.35/1.38	    32(114) -> 115*
4.35/1.38	    32(296) -> 297*
4.35/1.38	    32(84) -> 85*
4.35/1.38	    32(246) -> 247*
4.35/1.38	    32(156) -> 157*
4.35/1.38	    32(288) -> 289*
4.35/1.38	    32(78) -> 79*
4.35/1.38	    32(260) -> 261*
4.35/1.38	    32(170) -> 171*
4.35/1.38	    20(7) -> 7*
4.35/1.38	    42(287) -> 288*
4.35/1.38	    42(77) -> 78*
4.35/1.38	    42(259) -> 260*
4.35/1.38	    42(169) -> 170*
4.35/1.38	    42(251) -> 252*
4.35/1.38	    42(201) -> 202*
4.35/1.38	    42(161) -> 162*
4.35/1.38	    42(121) -> 122*
4.35/1.38	    42(91) -> 92*
4.35/1.38	    42(193) -> 194*
4.35/1.38	    42(113) -> 114*
4.35/1.38	    42(295) -> 296*
4.35/1.38	    42(83) -> 84*
4.35/1.38	    42(245) -> 246*
4.35/1.38	    42(155) -> 156*
4.35/1.38	    30(7) -> 7*
4.35/1.38	    52(90) -> 91*
4.35/1.38	    52(192) -> 193*
4.35/1.38	    52(314) -> 315*
4.35/1.38	    52(112) -> 113*
4.35/1.38	    52(294) -> 295*
4.35/1.38	    52(82) -> 83*
4.35/1.38	    52(244) -> 245*
4.35/1.38	    52(154) -> 155*
4.35/1.38	    52(316) -> 317*
4.35/1.38	    52(286) -> 287*
4.35/1.38	    52(76) -> 77*
4.35/1.38	    52(258) -> 259*
4.35/1.38	    52(228) -> 229*
4.35/1.38	    52(188) -> 189*
4.35/1.38	    52(168) -> 169*
4.35/1.38	    52(250) -> 251*
4.35/1.38	    52(200) -> 201*
4.35/1.38	    52(160) -> 161*
4.35/1.38	    52(130) -> 131*
4.35/1.38	    52(120) -> 121*
4.35/1.38	    40(7) -> 7*
4.35/1.38	    02(262) -> 263*
4.35/1.38	    02(197) -> 198*
4.35/1.38	    02(172) -> 173*
4.35/1.38	    02(117) -> 118*
4.35/1.38	    02(87) -> 88*
4.35/1.38	    02(249) -> 250*
4.35/1.38	    02(159) -> 160*
4.35/1.38	    02(94) -> 95*
4.35/1.38	    02(291) -> 292*
4.35/1.38	    02(81) -> 82*
4.35/1.38	    02(255) -> 256*
4.35/1.38	    02(165) -> 166*
4.35/1.38	    50(7) -> 7*
4.35/1.38	    7 -> 28*
4.35/1.38	    40 -> 48*
4.35/1.38	    47 -> 34,7
4.35/1.38	    54 -> 188,66
4.35/1.38	    55 -> 68*
4.35/1.38	    60 -> 76,74
4.35/1.38	    61 -> 34,7
4.35/1.38	    67 -> 49*
4.35/1.38	    69 -> 29*
4.35/1.38	    75 -> 29*
4.35/1.38	    88 -> 112*
4.35/1.38	    95 -> 40,48,34
4.35/1.38	    118 -> 130*
4.35/1.38	    124 -> 340,154
4.35/1.38	    125 -> 54,66,188,40,48,34
4.35/1.38	    131 -> 113*
4.35/1.38	    166 -> 192*
4.35/1.38	    173 -> 54,66,188,40,48
4.35/1.38	    189 -> 77*
4.35/1.38	    198 -> 228*
4.35/1.38	    204 -> 318,244
4.35/1.38	    205 -> 54,66,188,40,48
4.35/1.38	    229 -> 113*
4.35/1.38	    256 -> 286*
4.35/1.38	    263 -> 54,66,188
4.35/1.38	    292 -> 314*
4.35/1.38	    298 -> 342,316
4.35/1.38	    299 -> 54,66,188
4.35/1.38	    315 -> 193*
4.35/1.38	    317 -> 155*
4.35/1.38	    330 -> 344*
4.35/1.38	    337 -> 82*
4.35/1.38	    341 -> 319*
4.35/1.38	    343 -> 319*
4.35/1.38	    350 -> 358*
4.35/1.38	    356 -> 382*
4.35/1.38	    357 -> 82*
4.35/1.38	    359 -> 345*
4.35/1.38	    394 -> 406*
4.35/1.38	    401 -> 88,112
4.35/1.38	    412 -> 436*
4.35/1.38	    418 -> 438*
4.35/1.38	    419 -> 88,112
4.35/1.38	    437 -> 407*
4.35/1.38	    450 -> 492*
4.35/1.38	    457 -> 118,130
4.35/1.38	    498 -> 528*
4.35/1.38	    504 -> 544*
4.35/1.38	    505 -> 118,130
4.35/1.38	    529 -> 493*
4.35/1.38	    545 -> 439*
4.35/1.38	  problem:
4.35/1.38	   
4.35/1.38	  Qed
4.35/1.39	EOF