YES(?,O(n^1))
5.61/1.73	YES(?,O(n^1))
5.61/1.74	
5.61/1.74	Problem:
5.61/1.74	 b(b(a(b(b(a(b(b(b(b(b(b(a(b(x1)))))))))))))) ->
5.61/1.74	 b(b(b(b(b(a(b(b(a(b(b(a(b(b(b(b(b(b(x1))))))))))))))))))
5.61/1.74	
5.61/1.74	Proof:
5.61/1.74	 Bounds Processor:
5.61/1.74	  bound: 1
5.61/1.74	  enrichment: match
5.61/1.74	  automaton:
5.61/1.74	   final states: {2,1}
5.61/1.74	   transitions:
5.61/1.74	    b1(60) -> 61*
5.61/1.74	    b1(55) -> 56*
5.61/1.74	    b1(20) -> 21*
5.61/1.74	    b1(15) -> 16*
5.61/1.74	    b1(5) -> 6*
5.61/1.74	    b1(67) -> 68*
5.61/1.74	    b1(57) -> 58*
5.61/1.74	    b1(17) -> 18*
5.61/1.74	    b1(12) -> 13*
5.61/1.74	    b1(7) -> 8*
5.61/1.74	    b1(109) -> 110*
5.61/1.74	    b1(64) -> 65*
5.61/1.74	    b1(59) -> 60*
5.61/1.74	    b1(19) -> 20*
5.61/1.74	    b1(14) -> 15*
5.61/1.74	    b1(9) -> 10*
5.61/1.74	    b1(4) -> 5*
5.61/1.74	    b1(111) -> 112*
5.61/1.74	    b1(66) -> 67*
5.61/1.74	    b1(61) -> 62*
5.61/1.74	    b1(21) -> 22*
5.61/1.74	    b1(11) -> 12*
5.61/1.74	    b1(6) -> 7*
5.61/1.74	    b1(103) -> 104*
5.61/1.74	    b1(63) -> 64*
5.61/1.74	    b1(58) -> 59*
5.61/1.74	    b1(18) -> 19*
5.61/1.74	    b1(8) -> 9*
5.61/1.74	    b1(95) -> 96*
5.61/1.74	    a1(65) -> 66*
5.61/1.74	    a1(10) -> 11*
5.61/1.74	    a1(72) -> 73*
5.61/1.74	    a1(62) -> 63*
5.61/1.74	    a1(16) -> 17*
5.61/1.74	    a1(68) -> 69*
5.61/1.74	    a1(13) -> 14*
5.61/1.74	    b0(2) -> 1*
5.61/1.74	    b0(1) -> 1*
5.61/1.74	    a0(2) -> 2*
5.61/1.74	    a0(1) -> 2*
5.61/1.74	    1 -> 55*
5.61/1.74	    2 -> 4*
5.61/1.74	    6 -> 19,68,16,1,55
5.61/1.74	    9 -> 72*
5.61/1.74	    10 -> 109*
5.61/1.74	    16 -> 57*
5.61/1.74	    22 -> 20,56,6,5,1
5.61/1.74	    56 -> 5*
5.61/1.74	    62 -> 111*
5.61/1.74	    65 -> 103*
5.61/1.74	    68 -> 95*
5.61/1.74	    69 -> 18*
5.61/1.74	    73 -> 63*
5.61/1.74	    96 -> 5*
5.61/1.74	    104 -> 5*
5.61/1.74	    110 -> 6*
5.61/1.74	    112 -> 5*
5.61/1.74	  problem:
5.61/1.74	   
5.61/1.74	  Qed
5.61/1.74	EOF