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