YES(?,O(n^1))
9.02/2.54	YES(?,O(n^1))
9.02/2.54	
9.02/2.54	Problem:
9.02/2.54	 1(2(1(1(0(0(1(0(2(1(1(0(2(x1))))))))))))) -> 1(2(2(1(0(0(2(0(1(2(2(0(1(0(0(2(2(x1)))))))))))))))))
9.02/2.54	 2(0(1(2(1(2(1(2(1(0(0(1(0(x1))))))))))))) -> 2(2(0(0(2(1(1(1(0(0(0(1(1(1(2(2(0(x1)))))))))))))))))
9.02/2.54	 2(1(0(0(2(1(1(1(0(1(2(2(0(x1))))))))))))) -> 0(0(2(1(0(0(1(1(2(2(2(2(2(1(2(1(0(x1)))))))))))))))))
9.02/2.54	 2(2(0(0(1(0(2(1(1(1(0(0(1(x1))))))))))))) -> 2(2(1(1(2(0(0(1(2(2(0(2(0(0(2(2(2(x1)))))))))))))))))
9.02/2.54	 2(2(1(0(1(0(1(1(0(0(0(2(0(x1))))))))))))) -> 0(2(2(1(0(0(1(0(0(1(1(1(1(0(0(2(0(x1)))))))))))))))))
9.02/2.54	 2(2(1(1(0(2(0(0(0(2(2(0(0(x1))))))))))))) -> 0(0(1(2(0(0(0(2(2(0(1(2(2(2(2(0(0(x1)))))))))))))))))
9.02/2.54	 2(2(2(1(0(2(0(0(1(0(1(0(2(x1))))))))))))) -> 0(2(2(0(0(2(2(2(1(2(0(0(2(2(0(2(2(x1)))))))))))))))))
9.02/2.54	
9.02/2.54	Proof:
9.02/2.54	 Bounds Processor:
9.02/2.54	  bound: 1
9.02/2.54	  enrichment: match
9.02/2.54	  automaton:
9.02/2.54	   final states: {3,2,1}
9.02/2.54	   transitions:
9.02/2.54	    01(247) -> 248*
9.02/2.54	    01(232) -> 233*
9.02/2.54	    01(222) -> 223*
9.02/2.54	    01(10) -> 11*
9.02/2.54	    01(197) -> 198*
9.02/2.54	    01(192) -> 193*
9.02/2.54	    01(157) -> 158*
9.02/2.54	    01(324) -> 325*
9.02/2.54	    01(314) -> 315*
9.02/2.54	    01(112) -> 113*
9.02/2.54	    01(107) -> 108*
9.02/2.54	    01(102) -> 103*
9.02/2.54	    01(274) -> 275*
9.02/2.54	    01(239) -> 240*
9.02/2.54	    01(17) -> 18*
9.02/2.54	    01(7) -> 8*
9.02/2.54	    01(179) -> 180*
9.02/2.54	    01(144) -> 145*
9.02/2.54	    01(331) -> 332*
9.02/2.54	    01(311) -> 312*
9.02/2.54	    01(94) -> 95*
9.02/2.54	    01(281) -> 282*
9.02/2.54	    01(251) -> 252*
9.02/2.54	    01(246) -> 247*
9.02/2.54	    01(231) -> 232*
9.02/2.54	    01(14) -> 15*
9.02/2.54	    01(201) -> 202*
9.02/2.54	    01(191) -> 192*
9.02/2.54	    01(186) -> 187*
9.02/2.54	    01(181) -> 182*
9.02/2.54	    01(161) -> 162*
9.02/2.54	    01(156) -> 157*
9.02/2.54	    01(101) -> 102*
9.02/2.54	    01(273) -> 274*
9.02/2.54	    01(233) -> 234*
9.02/2.54	    01(228) -> 229*
9.02/2.54	    01(16) -> 17*
9.02/2.54	    01(198) -> 199*
9.02/2.54	    01(178) -> 179*
9.02/2.54	    01(325) -> 326*
9.02/2.54	    01(315) -> 316*
9.02/2.54	    01(310) -> 311*
9.02/2.54	    01(108) -> 109*
9.02/2.54	    01(280) -> 281*
9.02/2.54	    01(275) -> 276*
9.02/2.54	    01(240) -> 241*
9.02/2.54	    01(8) -> 9*
9.02/2.54	    01(200) -> 201*
9.02/2.54	    01(185) -> 186*
9.02/2.54	    01(160) -> 161*
9.02/2.54	    01(332) -> 333*
9.02/2.54	    01(327) -> 328*
9.02/2.54	    01(100) -> 101*
9.02/2.54	    21(237) -> 238*
9.02/2.54	    21(20) -> 21*
9.02/2.54	    21(15) -> 16*
9.02/2.54	    21(5) -> 6*
9.02/2.54	    21(187) -> 188*
9.02/2.54	    21(182) -> 183*
9.02/2.54	    21(177) -> 178*
9.02/2.54	    21(354) -> 355*
9.02/2.54	    21(152) -> 153*
9.02/2.54	    21(147) -> 148*
9.02/2.54	    21(329) -> 330*
9.02/2.54	    21(304) -> 305*
9.02/2.54	    21(279) -> 280*
9.02/2.54	    21(249) -> 250*
9.02/2.54	    21(244) -> 245*
9.02/2.54	    21(234) -> 235*
9.02/2.54	    21(229) -> 230*
9.02/2.54	    21(224) -> 225*
9.02/2.54	    21(12) -> 13*
9.02/2.54	    21(204) -> 205*
9.02/2.54	    21(159) -> 160*
9.02/2.54	    21(149) -> 150*
9.02/2.54	    21(326) -> 327*
9.02/2.54	    21(321) -> 322*
9.02/2.54	    21(109) -> 110*
9.02/2.54	    21(306) -> 307*
9.02/2.54	    21(301) -> 302*
9.02/2.54	    21(59) -> 60*
9.02/2.54	    21(241) -> 242*
9.02/2.54	    21(226) -> 227*
9.02/2.54	    21(19) -> 20*
9.02/2.54	    21(151) -> 152*
9.02/2.54	    21(333) -> 334*
9.02/2.54	    21(328) -> 329*
9.02/2.54	    21(323) -> 324*
9.02/2.54	    21(313) -> 314*
9.02/2.54	    21(106) -> 107*
9.02/2.54	    21(303) -> 304*
9.02/2.54	    21(96) -> 97*
9.02/2.54	    21(61) -> 62*
9.02/2.54	    21(243) -> 244*
9.02/2.54	    21(238) -> 239*
9.02/2.54	    21(223) -> 224*
9.02/2.54	    21(11) -> 12*
9.02/2.54	    21(6) -> 7*
9.02/2.54	    21(203) -> 204*
9.02/2.54	    21(183) -> 184*
9.02/2.54	    21(153) -> 154*
9.02/2.54	    21(305) -> 306*
9.02/2.54	    21(245) -> 246*
9.02/2.54	    21(230) -> 231*
9.02/2.54	    21(225) -> 226*
9.02/2.54	    21(180) -> 181*
9.02/2.54	    21(150) -> 151*
9.02/2.54	    21(337) -> 338*
9.02/2.54	    21(322) -> 323*
9.02/2.54	    21(110) -> 111*
9.02/2.54	    21(307) -> 308*
9.02/2.54	    21(95) -> 96*
9.02/2.54	    11(277) -> 278*
9.02/2.54	    11(272) -> 273*
9.02/2.54	    11(242) -> 243*
9.02/2.54	    11(227) -> 228*
9.02/2.54	    11(202) -> 203*
9.02/2.54	    11(334) -> 335*
9.02/2.54	    11(309) -> 310*
9.02/2.54	    11(97) -> 98*
9.02/2.54	    11(199) -> 200*
9.02/2.54	    11(194) -> 195*
9.02/2.54	    11(189) -> 190*
9.02/2.54	    11(184) -> 185*
9.02/2.54	    11(366) -> 367*
9.02/2.54	    11(154) -> 155*
9.02/2.54	    11(104) -> 105*
9.02/2.54	    11(99) -> 100*
9.02/2.54	    11(276) -> 277*
9.02/2.54	    11(271) -> 272*
9.02/2.54	    11(9) -> 10*
9.02/2.54	    11(196) -> 197*
9.02/2.54	    11(368) -> 369*
9.02/2.54	    11(146) -> 147*
9.02/2.54	    11(308) -> 309*
9.02/2.54	    11(278) -> 279*
9.02/2.54	    11(21) -> 22*
9.02/2.54	    11(193) -> 194*
9.02/2.54	    11(188) -> 189*
9.02/2.54	    11(370) -> 371*
9.02/2.54	    11(158) -> 159*
9.02/2.54	    11(148) -> 149*
9.02/2.54	    11(335) -> 336*
9.02/2.54	    11(330) -> 331*
9.02/2.54	    11(103) -> 104*
9.02/2.54	    11(300) -> 301*
9.02/2.54	    11(98) -> 99*
9.02/2.54	    11(270) -> 271*
9.02/2.54	    11(235) -> 236*
9.02/2.54	    11(18) -> 19*
9.02/2.54	    11(13) -> 14*
9.02/2.54	    11(195) -> 196*
9.02/2.54	    11(155) -> 156*
9.02/2.54	    11(352) -> 353*
9.02/2.54	    11(317) -> 318*
9.02/2.54	    11(312) -> 313*
9.02/2.54	    11(105) -> 106*
9.02/2.54	    11(302) -> 303*
9.02/2.54	    10(2) -> 1*
9.02/2.54	    10(1) -> 1*
9.02/2.54	    10(3) -> 1*
9.02/2.54	    20(2) -> 2*
9.02/2.54	    20(1) -> 2*
9.02/2.54	    20(3) -> 2*
9.02/2.54	    00(2) -> 3*
9.02/2.54	    00(1) -> 3*
9.02/2.54	    00(3) -> 3*
9.02/2.54	    1 -> 112,59
9.02/2.54	    2 -> 94,5
9.02/2.55	    3 -> 144,61
9.02/2.55	    6 -> 62,96,2,5,94,191,251
9.02/2.55	    7 -> 270,177
9.02/2.55	    8 -> 237*
9.02/2.55	    21 -> 337*
9.02/2.55	    22 -> 1*
9.02/2.55	    60 -> 6*
9.02/2.55	    62 -> 6*
9.02/2.55	    95 -> 222,146
9.02/2.55	    96 -> 191*
9.02/2.55	    97 -> 354*
9.02/2.55	    109 -> 300*
9.02/2.55	    111 -> 225,6,2
9.02/2.55	    113 -> 95*
9.02/2.55	    145 -> 95*
9.02/2.55	    150 -> 366*
9.02/2.55	    162 -> 355,97,178,7,148,60,317,2
9.02/2.55	    178 -> 352*
9.02/2.55	    190 -> 109*
9.02/2.55	    205 -> 249,161
9.02/2.55	    223 -> 370*
9.02/2.55	    225 -> 6,97,2,7
9.02/2.55	    235 -> 321*
9.02/2.55	    236 -> 160*
9.02/2.55	    248 -> 203*
9.02/2.55	    250 -> 7*
9.02/2.55	    252 -> 8*
9.02/2.55	    282 -> 368,110
9.02/2.55	    316 -> 148,60
9.02/2.55	    318 -> 301*
9.02/2.55	    336 -> 223*
9.02/2.55	    338 -> 322*
9.02/2.55	    353 -> 228*
9.02/2.55	    355 -> 177*
9.02/2.55	    367 -> 149*
9.02/2.55	    369 -> 147*
9.02/2.55	    371 -> 147*
9.02/2.55	  problem:
9.02/2.55	   
9.02/2.55	  Qed
9.02/2.55	EOF