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