YES(?,O(n^1))
0.24/0.83	YES(?,O(n^1))
0.24/0.83	
0.24/0.83	Problem:
0.24/0.83	 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
0.24/0.83	 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
0.24/0.83	 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
0.24/0.83	 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
0.24/0.83	 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))
0.24/0.83	 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))
0.24/0.83	 0(1(2(1(x1)))) ->
0.24/0.83	 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))
0.24/0.83	
0.24/0.83	Proof:
0.24/0.83	 Bounds Processor:
0.24/0.83	  bound: 3
0.24/0.83	  enrichment: match
0.24/0.83	  automaton:
0.24/0.83	   final states: {4}
0.24/0.83	   transitions:
0.24/0.83	    13(107) -> 108*
0.24/0.83	    13(102) -> 103*
0.24/0.83	    13(136) -> 137*
0.24/0.83	    13(138) -> 139*
0.24/0.83	    13(133) -> 134*
0.24/0.83	    13(108) -> 109*
0.24/0.83	    13(135) -> 136*
0.24/0.83	    13(130) -> 131*
0.24/0.83	    13(110) -> 111*
0.24/0.83	    13(105) -> 106*
0.24/0.83	    11(25) -> 26*
0.24/0.83	    11(20) -> 21*
0.24/0.83	    11(22) -> 23*
0.24/0.83	    11(17) -> 18*
0.24/0.83	    11(23) -> 24*
0.24/0.83	    23(157) -> 158*
0.24/0.83	    23(137) -> 138*
0.24/0.83	    23(132) -> 133*
0.24/0.83	    23(127) -> 128*
0.24/0.83	    23(112) -> 113*
0.24/0.83	    23(144) -> 145*
0.24/0.83	    23(129) -> 130*
0.24/0.83	    23(109) -> 110*
0.24/0.83	    23(104) -> 105*
0.24/0.83	    23(101) -> 102*
0.24/0.83	    21(35) -> 36*
0.24/0.83	    21(27) -> 28*
0.24/0.83	    21(24) -> 25*
0.24/0.83	    21(19) -> 20*
0.24/0.83	    21(16) -> 17*
0.24/0.83	    21(33) -> 34*
0.24/0.83	    03(134) -> 135*
0.24/0.83	    03(131) -> 132*
0.24/0.83	    03(106) -> 107*
0.24/0.83	    03(103) -> 104*
0.24/0.83	    01(21) -> 22*
0.24/0.83	    01(18) -> 19*
0.24/0.83	    12(65) -> 66*
0.24/0.83	    12(60) -> 61*
0.24/0.83	    12(50) -> 51*
0.24/0.83	    12(45) -> 46*
0.24/0.83	    12(62) -> 63*
0.24/0.83	    12(57) -> 58*
0.24/0.83	    12(47) -> 48*
0.24/0.83	    12(42) -> 43*
0.24/0.83	    12(63) -> 64*
0.24/0.83	    12(48) -> 49*
0.24/0.83	    00(4) -> 4*
0.24/0.83	    22(97) -> 98*
0.24/0.83	    22(64) -> 65*
0.24/0.83	    22(59) -> 60*
0.24/0.83	    22(54) -> 55*
0.24/0.83	    22(49) -> 50*
0.24/0.83	    22(44) -> 45*
0.24/0.83	    22(56) -> 57*
0.24/0.83	    22(41) -> 42*
0.24/0.83	    22(95) -> 96*
0.24/0.83	    22(80) -> 81*
0.24/0.83	    10(4) -> 4*
0.24/0.83	    02(61) -> 62*
0.24/0.83	    02(46) -> 47*
0.24/0.83	    02(58) -> 59*
0.24/0.83	    02(43) -> 44*
0.24/0.83	    20(4) -> 4*
0.24/0.83	    4 -> 16*
0.24/0.83	    22 -> 80,27
0.24/0.83	    23 -> 33*
0.24/0.83	    25 -> 41,35
0.24/0.83	    26 -> 19,4
0.24/0.83	    28 -> 20*
0.24/0.83	    34 -> 17*
0.24/0.83	    36 -> 17*
0.24/0.83	    47 -> 54*
0.24/0.83	    50 -> 112,56
0.24/0.83	    51 -> 22,27,19
0.24/0.83	    55 -> 45*
0.24/0.83	    62 -> 95*
0.24/0.83	    65 -> 101,97
0.24/0.83	    66 -> 22,27
0.24/0.83	    81 -> 42*
0.24/0.83	    96 -> 45*
0.24/0.83	    98 -> 42*
0.24/0.83	    107 -> 127*
0.24/0.83	    110 -> 129*
0.24/0.83	    111 -> 44*
0.24/0.83	    113 -> 102*
0.24/0.83	    128 -> 105*
0.24/0.83	    135 -> 144*
0.24/0.83	    138 -> 157*
0.24/0.83	    139 -> 47,54
0.24/0.83	    145 -> 133*
0.24/0.83	    158 -> 130*
0.24/0.83	  problem:
0.24/0.83	   
0.24/0.83	  Qed
0.24/0.83	EOF