YES(?,O(n^1))
0.16/0.40	YES(?,O(n^1))
0.16/0.40	
0.16/0.40	Problem:
0.16/0.40	 a(a(b(a(a(b(a(x1))))))) -> a(b(a(a(b(a(a(a(b(x1)))))))))
0.16/0.40	
0.16/0.40	Proof:
0.16/0.40	 Bounds Processor:
0.16/0.40	  bound: 3
0.16/0.40	  enrichment: match
0.16/0.40	  automaton:
0.16/0.40	   final states: {3}
0.16/0.40	   transitions:
0.16/0.40	    a3(162) -> 163*
0.16/0.40	    a3(157) -> 158*
0.16/0.40	    a3(142) -> 143*
0.16/0.40	    a3(137) -> 138*
0.16/0.40	    a3(159) -> 160*
0.16/0.40	    a3(139) -> 140*
0.16/0.40	    a3(156) -> 157*
0.16/0.40	    a3(136) -> 137*
0.16/0.40	    a3(160) -> 161*
0.16/0.40	    a3(155) -> 156*
0.16/0.40	    a3(140) -> 141*
0.16/0.40	    a3(135) -> 136*
0.16/0.40	    a1(20) -> 21*
0.16/0.40	    a1(15) -> 16*
0.16/0.40	    a1(22) -> 23*
0.16/0.40	    a1(17) -> 18*
0.16/0.40	    a1(19) -> 20*
0.16/0.40	    a1(16) -> 17*
0.16/0.40	    b3(154) -> 155*
0.16/0.40	    b3(134) -> 135*
0.16/0.40	    b3(161) -> 162*
0.16/0.40	    b3(141) -> 142*
0.16/0.40	    b3(158) -> 159*
0.16/0.40	    b3(138) -> 139*
0.16/0.40	    b1(30) -> 31*
0.16/0.40	    b1(32) -> 33*
0.16/0.40	    b1(24) -> 25*
0.16/0.40	    b1(14) -> 15*
0.16/0.40	    b1(21) -> 22*
0.16/0.40	    b1(118) -> 119*
0.16/0.40	    b1(18) -> 19*
0.16/0.40	    b1(120) -> 121*
0.16/0.40	    a2(60) -> 61*
0.16/0.40	    a2(40) -> 41*
0.16/0.40	    a2(92) -> 93*
0.16/0.40	    a2(87) -> 88*
0.16/0.40	    a2(94) -> 95*
0.16/0.40	    a2(89) -> 90*
0.16/0.40	    a2(64) -> 65*
0.16/0.40	    a2(59) -> 60*
0.16/0.40	    a2(44) -> 45*
0.16/0.40	    a2(39) -> 40*
0.16/0.40	    a2(91) -> 92*
0.16/0.40	    a2(66) -> 67*
0.16/0.40	    a2(61) -> 62*
0.16/0.40	    a2(46) -> 47*
0.16/0.40	    a2(41) -> 42*
0.16/0.40	    a2(88) -> 89*
0.16/0.40	    a2(63) -> 64*
0.16/0.40	    a2(43) -> 44*
0.16/0.40	    a0(3) -> 3*
0.16/0.40	    b2(65) -> 66*
0.16/0.40	    b2(45) -> 46*
0.16/0.40	    b2(112) -> 113*
0.16/0.40	    b2(82) -> 83*
0.16/0.40	    b2(62) -> 63*
0.16/0.40	    b2(42) -> 43*
0.16/0.40	    b2(174) -> 175*
0.16/0.40	    b2(126) -> 127*
0.16/0.40	    b2(96) -> 97*
0.16/0.40	    b2(86) -> 87*
0.16/0.40	    b2(128) -> 129*
0.16/0.40	    b2(93) -> 94*
0.16/0.40	    b2(68) -> 69*
0.16/0.40	    b2(58) -> 59*
0.16/0.40	    b2(38) -> 39*
0.16/0.40	    b2(110) -> 111*
0.16/0.40	    b2(90) -> 91*
0.16/0.40	    b0(3) -> 3*
0.16/0.40	    3 -> 14*
0.16/0.40	    15 -> 174*
0.16/0.40	    16 -> 82*
0.16/0.40	    17 -> 38,24
0.16/0.40	    19 -> 58*
0.16/0.40	    20 -> 86,30
0.16/0.40	    22 -> 68,32
0.16/0.40	    23 -> 41,17,3
0.16/0.40	    25 -> 15*
0.16/0.40	    31 -> 15*
0.16/0.40	    33 -> 15*
0.16/0.40	    46 -> 128,120
0.16/0.40	    47 -> 42,18
0.16/0.40	    61 -> 154,126
0.16/0.40	    64 -> 134,96
0.16/0.40	    66 -> 112*
0.16/0.40	    67 -> 157,41,17,24
0.16/0.40	    69 -> 59*
0.16/0.40	    83 -> 59*
0.16/0.40	    94 -> 118,110
0.16/0.40	    95 -> 45,21
0.16/0.40	    97 -> 87*
0.16/0.40	    111 -> 87*
0.16/0.40	    113 -> 59*
0.16/0.40	    119 -> 15*
0.16/0.40	    121 -> 15*
0.16/0.40	    127 -> 39*
0.16/0.40	    129 -> 39*
0.16/0.40	    143 -> 161,45
0.16/0.40	    163 -> 158,42
0.16/0.40	    175 -> 59*
0.16/0.40	  problem:
0.16/0.40	   
0.16/0.40	  Qed
0.16/0.41	EOF