YES(?,O(n^1))
3.25/1.03	YES(?,O(n^1))
3.25/1.04	
3.25/1.04	Problem:
3.25/1.04	 4(2(4(x1))) -> 2(0(0(5(3(3(5(2(0(4(x1))))))))))
3.25/1.04	 4(4(2(4(2(x1))))) -> 2(0(5(2(1(4(0(2(0(1(x1))))))))))
3.25/1.04	 0(5(4(2(4(3(x1)))))) -> 5(1(5(5(3(5(3(0(0(0(x1))))))))))
3.25/1.04	 1(1(4(5(3(3(x1)))))) -> 1(3(1(1(3(0(1(2(2(1(x1))))))))))
3.25/1.04	 3(1(4(3(1(2(x1)))))) -> 0(0(1(1(4(2(3(0(0(3(x1))))))))))
3.25/1.04	 3(2(4(2(4(1(x1)))))) -> 0(2(1(1(1(5(3(1(3(3(x1))))))))))
3.25/1.04	 3(3(0(4(1(2(x1)))))) -> 3(5(1(2(0(2(0(5(3(1(x1))))))))))
3.25/1.04	 4(1(4(5(0(5(4(x1))))))) -> 4(1(5(3(1(0(5(3(1(0(x1))))))))))
3.25/1.04	 4(4(0(5(4(2(2(x1))))))) -> 4(0(4(3(4(4(4(5(4(1(x1))))))))))
3.25/1.04	 5(4(5(3(2(4(3(x1))))))) -> 2(5(5(5(0(4(5(0(1(4(x1))))))))))
3.25/1.04	
3.25/1.04	Proof:
3.25/1.04	 Bounds Processor:
3.25/1.04	  bound: 1
3.25/1.04	  enrichment: match
3.25/1.04	  automaton:
3.25/1.04	   final states: {7}
3.25/1.04	   transitions:
3.25/1.04	    21(55) -> 56*
3.25/1.04	    21(152) -> 153*
3.25/1.04	    21(102) -> 103*
3.25/1.04	    21(72) -> 73*
3.25/1.04	    21(32) -> 33*
3.25/1.04	    21(104) -> 105*
3.25/1.04	    21(261) -> 262*
3.25/1.04	    21(54) -> 55*
3.25/1.04	    21(86) -> 87*
3.25/1.04	    21(36) -> 37*
3.25/1.04	    21(21) -> 22*
3.25/1.04	    21(295) -> 296*
3.25/1.04	    21(260) -> 261*
3.25/1.04	    21(28) -> 29*
3.25/1.04	    21(145) -> 146*
3.25/1.04	    51(50) -> 51*
3.25/1.04	    51(25) -> 26*
3.25/1.04	    51(137) -> 138*
3.25/1.04	    51(329) -> 330*
3.25/1.04	    51(82) -> 83*
3.25/1.04	    51(52) -> 53*
3.25/1.04	    51(47) -> 48*
3.25/1.04	    51(37) -> 38*
3.25/1.04	    51(22) -> 23*
3.25/1.04	    51(209) -> 210*
3.25/1.04	    51(149) -> 150*
3.25/1.04	    51(139) -> 140*
3.25/1.04	    51(134) -> 135*
3.25/1.04	    51(124) -> 125*
3.25/1.04	    51(49) -> 50*
3.25/1.04	    51(211) -> 212*
3.25/1.04	    51(206) -> 207*
3.25/1.04	    51(146) -> 147*
3.25/1.04	    51(111) -> 112*
3.25/1.04	    51(106) -> 107*
3.25/1.04	    51(208) -> 209*
3.25/1.04	    51(138) -> 139*
3.25/1.04	    51(115) -> 116*
3.25/1.04	    51(100) -> 101*
3.25/1.04	    01(70) -> 71*
3.25/1.04	    01(45) -> 46*
3.25/1.04	    01(20) -> 21*
3.25/1.04	    01(202) -> 203*
3.25/1.04	    01(112) -> 113*
3.25/1.04	    01(299) -> 300*
3.25/1.04	    01(77) -> 78*
3.25/1.04	    01(57) -> 58*
3.25/1.04	    01(27) -> 28*
3.25/1.04	    01(204) -> 205*
3.25/1.04	    01(326) -> 327*
3.25/1.04	    01(69) -> 70*
3.25/1.04	    01(44) -> 45*
3.25/1.04	    01(151) -> 152*
3.25/1.04	    01(136) -> 137*
3.25/1.04	    01(101) -> 102*
3.25/1.04	    01(293) -> 294*
3.25/1.04	    01(76) -> 77*
3.25/1.04	    01(263) -> 264*
3.25/1.04	    01(31) -> 32*
3.25/1.04	    01(26) -> 27*
3.25/1.04	    01(203) -> 204*
3.25/1.04	    01(133) -> 134*
3.25/1.04	    01(330) -> 331*
3.25/1.04	    01(103) -> 104*
3.25/1.04	    01(300) -> 301*
3.25/1.04	    01(43) -> 44*
3.25/1.04	    01(33) -> 34*
3.25/1.04	    01(357) -> 358*
3.25/1.04	    01(150) -> 151*
3.25/1.04	    01(130) -> 131*
3.25/1.04	    01(292) -> 293*
3.25/1.04	    41(334) -> 335*
3.25/1.04	    41(127) -> 128*
3.25/1.04	    41(117) -> 118*
3.25/1.04	    41(129) -> 130*
3.25/1.04	    41(296) -> 297*
3.25/1.04	    41(34) -> 35*
3.25/1.04	    41(19) -> 20*
3.25/1.04	    41(126) -> 127*
3.25/1.04	    41(123) -> 124*
3.25/1.04	    41(73) -> 74*
3.25/1.04	    41(135) -> 136*
3.25/1.04	    41(125) -> 126*
3.25/1.04	    11(85) -> 86*
3.25/1.04	    11(80) -> 81*
3.25/1.04	    11(75) -> 76*
3.25/1.04	    11(262) -> 263*
3.25/1.04	    11(60) -> 61*
3.25/1.04	    11(35) -> 36*
3.25/1.04	    11(30) -> 31*
3.25/1.04	    11(187) -> 188*
3.25/1.04	    11(349) -> 350*
3.25/1.04	    11(132) -> 133*
3.25/1.04	    11(62) -> 63*
3.25/1.04	    11(259) -> 260*
3.25/1.04	    11(331) -> 332*
3.25/1.04	    11(109) -> 110*
3.25/1.04	    11(84) -> 85*
3.25/1.04	    11(74) -> 75*
3.25/1.04	    11(266) -> 267*
3.25/1.04	    11(59) -> 60*
3.25/1.04	    11(116) -> 117*
3.25/1.04	    11(298) -> 299*
3.25/1.04	    11(56) -> 57*
3.25/1.04	    11(51) -> 52*
3.25/1.04	    11(113) -> 114*
3.25/1.04	    11(83) -> 84*
3.25/1.04	    11(265) -> 266*
3.25/1.04	    11(210) -> 211*
3.25/1.04	    11(327) -> 328*
3.25/1.04	    11(105) -> 106*
3.25/1.04	    11(297) -> 298*
3.25/1.04	    31(207) -> 208*
3.25/1.04	    31(359) -> 360*
3.25/1.04	    31(147) -> 148*
3.25/1.04	    31(107) -> 108*
3.25/1.04	    31(294) -> 295*
3.25/1.04	    31(264) -> 265*
3.25/1.04	    31(351) -> 352*
3.25/1.04	    31(114) -> 115*
3.25/1.04	    31(99) -> 100*
3.25/1.04	    31(291) -> 292*
3.25/1.04	    31(79) -> 80*
3.25/1.04	    31(24) -> 25*
3.25/1.04	    31(353) -> 354*
3.25/1.04	    31(328) -> 329*
3.25/1.04	    31(313) -> 314*
3.25/1.04	    31(81) -> 82*
3.25/1.04	    31(71) -> 72*
3.25/1.04	    31(61) -> 62*
3.25/1.04	    31(46) -> 47*
3.25/1.04	    31(355) -> 356*
3.25/1.04	    31(148) -> 149*
3.25/1.04	    31(128) -> 129*
3.25/1.04	    31(315) -> 316*
3.25/1.04	    31(68) -> 69*
3.25/1.04	    31(58) -> 59*
3.25/1.04	    31(48) -> 49*
3.25/1.04	    31(23) -> 24*
3.25/1.04	    31(205) -> 206*
3.25/1.04	    31(332) -> 333*
3.25/1.04	    31(110) -> 111*
3.25/1.04	    40(7) -> 7*
3.25/1.04	    20(7) -> 7*
3.25/1.04	    00(7) -> 7*
3.25/1.04	    50(7) -> 7*
3.25/1.04	    30(7) -> 7*
3.25/1.04	    10(7) -> 7*
3.25/1.04	    7 -> 68,43,30,19
3.25/1.04	    19 -> 357*
3.25/1.04	    20 -> 7,132
3.25/1.04	    28 -> 291,187
3.25/1.04	    29 -> 20,132,7
3.25/1.04	    30 -> 353*
3.25/1.04	    31 -> 7,43,19,30,68,123,99,54
3.25/1.04	    38 -> 27*
3.25/1.04	    44 -> 145,109
3.25/1.04	    53 -> 358,44,109,7
3.25/1.04	    62 -> 315*
3.25/1.04	    63 -> 31,99,54,123,7
3.25/1.04	    69 -> 79*
3.25/1.04	    78 -> 354,100,69,7
3.25/1.04	    87 -> 77*
3.25/1.04	    107 -> 334,259,202
3.25/1.04	    108 -> 354,80,69,7
3.25/1.04	    116 -> 313*
3.25/1.04	    117 -> 326*
3.25/1.04	    118 -> 20,124,132,7
3.25/1.04	    131 -> 117*
3.25/1.04	    140 -> 28*
3.25/1.04	    152 -> 351,349
3.25/1.04	    153 -> 20,7,43,19,30,68,132
3.25/1.04	    187 -> 355*
3.25/1.04	    188 -> 31*
3.25/1.04	    212 -> 358,44,7,43,19,30,68,109
3.25/1.04	    267 -> 107*
3.25/1.04	    301 -> 354,100,7,69
3.25/1.04	    314 -> 79*
3.25/1.04	    316 -> 79*
3.25/1.04	    333 -> 52*
3.25/1.04	    335 -> 132*
3.25/1.04	    349 -> 359*
3.25/1.04	    350 -> 31*
3.25/1.04	    352 -> 69*
3.25/1.04	    354 -> 79*
3.25/1.04	    356 -> 79*
3.25/1.04	    358 -> 109*
3.25/1.04	    360 -> 79*
3.25/1.04	  problem:
3.25/1.04	   
3.25/1.04	  Qed
3.25/1.04	EOF