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