YES(?,O(n^1))
4.03/1.28	YES(?,O(n^1))
4.03/1.29	
4.03/1.29	Problem:
4.03/1.29	 1(4(x1)) -> 3(1(1(2(2(4(x1))))))
4.03/1.29	 5(4(x1)) -> 4(2(3(1(1(1(x1))))))
4.03/1.29	 0(3(0(x1))) -> 2(1(1(0(2(0(x1))))))
4.03/1.29	 0(5(5(x1))) -> 1(0(1(3(4(2(x1))))))
4.03/1.29	 1(5(4(x1))) -> 0(2(5(2(0(4(x1))))))
4.03/1.29	 3(5(4(x1))) -> 4(1(3(4(2(3(x1))))))
4.03/1.29	 4(1(4(x1))) -> 3(3(2(2(3(1(x1))))))
4.03/1.29	 5(4(0(x1))) -> 2(4(0(4(4(0(x1))))))
4.03/1.29	 5(4(0(x1))) -> 5(1(5(2(1(0(x1))))))
4.03/1.29	 5(4(4(x1))) -> 4(1(1(3(2(4(x1))))))
4.03/1.29	 5(5(4(x1))) -> 3(4(4(1(2(2(x1))))))
4.03/1.29	 0(5(5(0(x1)))) -> 0(2(0(0(3(0(x1))))))
4.03/1.29	 0(5(5(4(x1)))) -> 0(1(3(4(3(4(x1))))))
4.03/1.29	 1(4(5(4(x1)))) -> 0(4(5(0(2(1(x1))))))
4.03/1.29	 1(4(5(5(x1)))) -> 0(0(1(3(4(1(x1))))))
4.03/1.29	 2(5(4(0(x1)))) -> 0(4(1(2(4(0(x1))))))
4.03/1.29	 4(3(0(5(x1)))) -> 3(3(2(3(5(5(x1))))))
4.03/1.29	 5(4(0(0(x1)))) -> 1(0(4(0(2(2(x1))))))
4.03/1.29	 5(4(0(2(x1)))) -> 3(0(4(5(0(2(x1))))))
4.03/1.29	
4.03/1.29	Proof:
4.03/1.29	 Bounds Processor:
4.03/1.29	  bound: 2
4.03/1.29	  enrichment: match
4.03/1.29	  automaton:
4.03/1.29	   final states: {7}
4.03/1.29	   transitions:
4.03/1.29	    31(75) -> 76*
4.03/1.29	    31(60) -> 61*
4.03/1.29	    31(25) -> 26*
4.03/1.29	    31(20) -> 21*
4.03/1.29	    31(404) -> 405*
4.03/1.29	    31(132) -> 133*
4.03/1.29	    31(117) -> 118*
4.03/1.29	    31(92) -> 93*
4.03/1.29	    31(72) -> 73*
4.03/1.29	    31(57) -> 58*
4.03/1.29	    31(42) -> 43*
4.03/1.29	    31(361) -> 362*
4.03/1.29	    31(119) -> 120*
4.03/1.29	    31(104) -> 105*
4.03/1.29	    31(397) -> 398*
4.03/1.29	    31(145) -> 146*
4.03/1.29	    31(297) -> 298*
4.03/1.29	    01(55) -> 56*
4.03/1.29	    01(35) -> 36*
4.03/1.29	    01(414) -> 415*
4.03/1.29	    01(162) -> 163*
4.03/1.29	    01(147) -> 148*
4.03/1.29	    01(299) -> 300*
4.03/1.29	    01(159) -> 160*
4.03/1.29	    01(134) -> 135*
4.03/1.29	    01(79) -> 80*
4.03/1.29	    01(44) -> 45*
4.03/1.29	    01(413) -> 414*
4.03/1.29	    01(106) -> 107*
4.03/1.29	    01(51) -> 52*
4.03/1.29	    01(340) -> 341*
4.03/1.29	    01(123) -> 124*
4.03/1.29	    01(33) -> 34*
4.03/1.29	    01(105) -> 106*
4.03/1.29	    41(80) -> 81*
4.03/1.29	    41(15) -> 16*
4.03/1.29	    41(102) -> 103*
4.03/1.29	    41(77) -> 78*
4.03/1.29	    41(27) -> 28*
4.03/1.29	    41(296) -> 297*
4.03/1.29	    41(59) -> 60*
4.03/1.29	    41(428) -> 429*
4.03/1.29	    41(403) -> 404*
4.03/1.29	    41(161) -> 162*
4.03/1.29	    41(131) -> 132*
4.03/1.29	    41(101) -> 102*
4.03/1.29	    41(41) -> 42*
4.03/1.29	    41(420) -> 421*
4.03/1.29	    41(380) -> 381*
4.03/1.29	    41(148) -> 149*
4.03/1.29	    41(118) -> 119*
4.03/1.29	    41(78) -> 79*
4.03/1.29	    41(402) -> 403*
4.03/1.29	    41(125) -> 126*
4.03/1.29	    51(386) -> 387*
4.03/1.29	    51(144) -> 145*
4.03/1.29	    51(124) -> 125*
4.03/1.29	    51(338) -> 339*
4.03/1.29	    51(430) -> 431*
4.03/1.29	    51(143) -> 144*
4.03/1.29	    51(88) -> 89*
4.03/1.29	    51(53) -> 54*
4.03/1.29	    51(160) -> 161*
4.03/1.29	    51(90) -> 91*
4.03/1.29	    21(40) -> 41*
4.03/1.29	    21(424) -> 425*
4.03/1.29	    21(399) -> 400*
4.03/1.29	    21(339) -> 340*
4.03/1.29	    21(122) -> 123*
4.03/1.29	    21(501) -> 502*
4.03/1.29	    21(87) -> 88*
4.03/1.29	    21(52) -> 53*
4.03/1.29	    21(426) -> 427*
4.03/1.29	    21(17) -> 18*
4.03/1.29	    21(503) -> 504*
4.03/1.29	    21(99) -> 100*
4.03/1.29	    21(483) -> 484*
4.03/1.29	    21(74) -> 75*
4.03/1.29	    21(54) -> 55*
4.03/1.29	    21(34) -> 35*
4.03/1.29	    21(136) -> 137*
4.03/1.29	    21(238) -> 239*
4.03/1.29	    21(26) -> 27*
4.03/1.29	    21(16) -> 17*
4.03/1.29	    21(400) -> 401*
4.03/1.29	    21(295) -> 296*
4.03/1.29	    21(73) -> 74*
4.03/1.29	    21(58) -> 59*
4.03/1.29	    21(38) -> 39*
4.03/1.29	    21(220) -> 221*
4.03/1.29	    11(45) -> 46*
4.03/1.29	    11(137) -> 138*
4.03/1.29	    11(481) -> 482*
4.03/1.29	    11(37) -> 38*
4.03/1.29	    11(22) -> 23*
4.03/1.29	    11(219) -> 220*
4.03/1.29	    11(401) -> 402*
4.03/1.29	    11(189) -> 190*
4.03/1.29	    11(179) -> 180*
4.03/1.29	    11(89) -> 90*
4.03/1.29	    11(24) -> 25*
4.03/1.29	    11(19) -> 20*
4.03/1.29	    11(298) -> 299*
4.03/1.29	    11(86) -> 87*
4.03/1.29	    11(61) -> 62*
4.03/1.29	    11(36) -> 37*
4.03/1.29	    11(218) -> 219*
4.03/1.29	    11(133) -> 134*
4.03/1.29	    11(300) -> 301*
4.03/1.29	    11(93) -> 94*
4.03/1.29	    11(43) -> 44*
4.03/1.29	    11(23) -> 24*
4.03/1.29	    11(422) -> 423*
4.03/1.29	    11(18) -> 19*
4.03/1.29	    11(120) -> 121*
4.03/1.29	    11(100) -> 101*
4.03/1.29	    32(469) -> 470*
4.03/1.29	    32(476) -> 477*
4.03/1.29	    32(411) -> 412*
4.03/1.29	    32(194) -> 195*
4.03/1.29	    32(169) -> 170*
4.03/1.29	    32(366) -> 367*
4.03/1.29	    32(363) -> 364*
4.03/1.29	    32(490) -> 491*
4.03/1.29	    32(435) -> 436*
4.03/1.29	    32(487) -> 488*
4.03/1.29	    32(472) -> 473*
4.03/1.29	    32(367) -> 368*
4.03/1.29	    32(489) -> 490*
4.03/1.29	    10(7) -> 7*
4.03/1.29	    42(474) -> 475*
4.03/1.29	    42(409) -> 410*
4.03/1.29	    42(471) -> 472*
4.03/1.29	    42(164) -> 165*
4.03/1.29	    42(196) -> 197*
4.03/1.29	    42(410) -> 411*
4.03/1.29	    42(437) -> 438*
4.03/1.29	    40(7) -> 7*
4.03/1.29	    12(444) -> 445*
4.03/1.29	    12(434) -> 435*
4.03/1.29	    12(192) -> 193*
4.03/1.29	    12(167) -> 168*
4.03/1.29	    12(254) -> 255*
4.03/1.29	    12(473) -> 474*
4.03/1.29	    12(433) -> 434*
4.03/1.29	    12(211) -> 212*
4.03/1.29	    12(408) -> 409*
4.03/1.29	    12(191) -> 192*
4.03/1.29	    12(253) -> 254*
4.03/1.29	    12(445) -> 446*
4.03/1.29	    12(193) -> 194*
4.03/1.29	    12(168) -> 169*
4.03/1.29	    12(432) -> 433*
4.03/1.29	    12(210) -> 211*
4.03/1.29	    30(7) -> 7*
4.03/1.29	    22(212) -> 213*
4.03/1.29	    22(364) -> 365*
4.03/1.29	    22(446) -> 447*
4.03/1.29	    22(436) -> 437*
4.03/1.29	    22(406) -> 407*
4.03/1.29	    22(488) -> 489*
4.03/1.29	    22(251) -> 252*
4.03/1.29	    22(166) -> 167*
4.03/1.29	    22(470) -> 471*
4.03/1.29	    22(208) -> 209*
4.03/1.29	    22(365) -> 366*
4.03/1.29	    22(255) -> 256*
4.03/1.29	    22(442) -> 443*
4.03/1.29	    22(407) -> 408*
4.03/1.29	    22(195) -> 196*
4.03/1.29	    22(165) -> 166*
4.03/1.29	    20(7) -> 7*
4.03/1.29	    02(252) -> 253*
4.03/1.29	    02(207) -> 208*
4.03/1.29	    02(441) -> 442*
4.03/1.29	    02(209) -> 210*
4.03/1.29	    02(448) -> 449*
4.03/1.29	    02(443) -> 444*
4.03/1.29	    02(250) -> 251*
4.03/1.29	    50(7) -> 7*
4.03/1.29	    52(486) -> 487*
4.03/1.29	    52(485) -> 486*
4.03/1.29	    00(7) -> 7*
4.03/1.29	    7 -> 143,57,40,33,22,15
4.03/1.29	    16 -> 380,117,51
4.03/1.29	    17 -> 481,92
4.03/1.29	    21 -> 421,119,145,144,16,51,132,117,23,122,7
4.03/1.29	    23 -> 131,122,72
4.03/1.29	    27 -> 476,406,399,361,191,189,164
4.03/1.29	    28 -> 58,144,7
4.03/1.29	    33 -> 501,250
4.03/1.29	    34 -> 251,7,143,40,22,15,33,57,250,430,104,86,77
4.03/1.29	    35 -> 338*
4.03/1.29	    39 -> 251,414,144,34,86,77,104,7
4.03/1.29	    41 -> 397,159,99
4.03/1.29	    46 -> 251,144,34,86,77,104,7
4.03/1.29	    55 -> 441,426
4.03/1.29	    56 -> 502,41,99,159,34,86,77,104,23,122,72,131,7
4.03/1.29	    58 -> 420,413
4.03/1.29	    62 -> 27*
4.03/1.29	    76 -> 20*
4.03/1.29	    78 -> 136*
4.03/1.29	    81 -> 38*
4.03/1.29	    90 -> 485,422,295
4.03/1.29	    91 -> 144,7
4.03/1.29	    94 -> 61*
4.03/1.29	    100 -> 147*
4.03/1.29	    101 -> 179*
4.03/1.29	    103 -> 20*
4.03/1.29	    107 -> 54*
4.03/1.29	    121 -> 55*
4.03/1.29	    123 -> 386*
4.03/1.29	    126 -> 55*
4.03/1.29	    134 -> 424*
4.03/1.29	    135 -> 55*
4.03/1.29	    138 -> 125*
4.03/1.29	    144 -> 428*
4.03/1.29	    146 -> 74*
4.03/1.29	    149 -> 44*
4.03/1.29	    160 -> 218*
4.03/1.29	    162 -> 207*
4.03/1.29	    163 -> 238,20
4.03/1.29	    170 -> 23,122
4.03/1.29	    180 -> 20*
4.03/1.29	    190 -> 23*
4.03/1.29	    192 -> 363*
4.03/1.29	    196 -> 469,432
4.03/1.29	    197 -> 145,144
4.03/1.29	    212 -> 503*
4.03/1.29	    213 -> 251,52,34,86,77,104
4.03/1.29	    221 -> 251,34,86,7,77,104
4.03/1.29	    239 -> 35*
4.03/1.29	    256 -> 414,106
4.03/1.29	    301 -> 251,34,86,7,57,33,15,22,40,143,77,104
4.03/1.29	    340 -> 483,448
4.03/1.29	    341 -> 23,122,7,57,33,15,22,40,143,72,131
4.03/1.29	    362 -> 58*
4.03/1.29	    368 -> 132*
4.03/1.29	    381 -> 79*
4.03/1.29	    387 -> 89*
4.03/1.29	    398 -> 93*
4.03/1.29	    405 -> 7,22,40,143,57,33,15,144
4.03/1.29	    412 -> 145*
4.03/1.29	    415 -> 38*
4.03/1.29	    421 -> 119*
4.03/1.29	    423 -> 131*
4.03/1.29	    425 -> 99*
4.03/1.29	    427 -> 99*
4.03/1.29	    429 -> 162*
4.03/1.29	    431 -> 161*
4.03/1.29	    438 -> 145*
4.03/1.29	    447 -> 106,414
4.03/1.29	    449 -> 442*
4.03/1.29	    475 -> 146*
4.03/1.29	    477 -> 470*
4.03/1.29	    482 -> 125*
4.03/1.29	    484 -> 99*
4.03/1.29	    491 -> 421,119
4.03/1.29	    502 -> 99*
4.03/1.29	    504 -> 33*
4.03/1.29	  problem:
4.03/1.29	   
4.03/1.29	  Qed
4.03/1.29	EOF