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	 b(a(b(a(a(a(x1)))))) -> a(a(a(a(b(a(b(a(b(x1)))))))))
0.16/0.40	
0.16/0.40	Proof:
0.16/0.40	 Bounds Processor:
0.16/0.40	  bound: 4
0.16/0.40	  enrichment: match
0.16/0.40	  automaton:
0.16/0.40	   final states: {2,1}
0.16/0.40	   transitions:
0.16/0.40	    b3(202) -> 203*
0.16/0.40	    b3(192) -> 193*
0.16/0.40	    b3(194) -> 195*
0.16/0.40	    b3(134) -> 135*
0.16/0.40	    b3(246) -> 247*
0.16/0.40	    b3(166) -> 167*
0.16/0.40	    b3(136) -> 137*
0.16/0.40	    b3(106) -> 107*
0.16/0.40	    b3(248) -> 249*
0.16/0.40	    b3(198) -> 199*
0.16/0.40	    b3(168) -> 169*
0.16/0.40	    b3(138) -> 139*
0.16/0.40	    b3(108) -> 109*
0.16/0.40	    b3(240) -> 241*
0.16/0.40	    b3(200) -> 201*
0.16/0.40	    b3(170) -> 171*
0.16/0.40	    b3(110) -> 111*
0.16/0.40	    a4(224) -> 225*
0.16/0.40	    a4(219) -> 220*
0.16/0.40	    a4(214) -> 215*
0.16/0.40	    a4(209) -> 210*
0.16/0.40	    a4(226) -> 227*
0.16/0.40	    a4(221) -> 222*
0.16/0.40	    a4(216) -> 217*
0.16/0.40	    a4(211) -> 212*
0.16/0.40	    a4(223) -> 224*
0.16/0.40	    a4(213) -> 214*
0.16/0.40	    a4(225) -> 226*
0.16/0.40	    a4(215) -> 216*
0.16/0.40	    b4(222) -> 223*
0.16/0.40	    b4(212) -> 213*
0.16/0.40	    b4(218) -> 219*
0.16/0.40	    b4(208) -> 209*
0.16/0.40	    b4(220) -> 221*
0.16/0.40	    b4(210) -> 211*
0.16/0.40	    b0(2) -> 1*
0.16/0.40	    b0(1) -> 1*
0.16/0.40	    a0(2) -> 2*
0.16/0.40	    a0(1) -> 2*
0.16/0.40	    a1(10) -> 11*
0.16/0.40	    a1(5) -> 6*
0.16/0.40	    a1(12) -> 13*
0.16/0.40	    a1(7) -> 8*
0.16/0.40	    a1(9) -> 10*
0.16/0.40	    a1(11) -> 12*
0.16/0.40	    b1(62) -> 63*
0.16/0.40	    b1(64) -> 65*
0.16/0.40	    b1(34) -> 35*
0.16/0.40	    b1(4) -> 5*
0.16/0.40	    b1(6) -> 7*
0.16/0.40	    b1(58) -> 59*
0.16/0.40	    b1(8) -> 9*
0.16/0.40	    a2(102) -> 103*
0.16/0.40	    a2(97) -> 98*
0.16/0.40	    a2(72) -> 73*
0.16/0.40	    a2(67) -> 68*
0.16/0.40	    a2(42) -> 43*
0.16/0.40	    a2(37) -> 38*
0.16/0.40	    a2(104) -> 105*
0.16/0.40	    a2(99) -> 100*
0.16/0.40	    a2(74) -> 75*
0.16/0.40	    a2(69) -> 70*
0.16/0.40	    a2(44) -> 45*
0.16/0.40	    a2(39) -> 40*
0.16/0.40	    a2(101) -> 102*
0.16/0.40	    a2(71) -> 72*
0.16/0.40	    a2(41) -> 42*
0.16/0.40	    a2(103) -> 104*
0.16/0.40	    a2(73) -> 74*
0.16/0.40	    a2(43) -> 44*
0.16/0.40	    b2(70) -> 71*
0.16/0.40	    b2(40) -> 41*
0.16/0.40	    b2(144) -> 145*
0.16/0.40	    b2(176) -> 177*
0.16/0.40	    b2(96) -> 97*
0.16/0.40	    b2(76) -> 77*
0.16/0.40	    b2(66) -> 67*
0.16/0.40	    b2(36) -> 37*
0.16/0.40	    b2(98) -> 99*
0.16/0.40	    b2(78) -> 79*
0.16/0.40	    b2(68) -> 69*
0.16/0.40	    b2(38) -> 39*
0.16/0.40	    b2(120) -> 121*
0.16/0.40	    b2(100) -> 101*
0.16/0.40	    a3(172) -> 173*
0.16/0.40	    a3(167) -> 168*
0.16/0.40	    a3(142) -> 143*
0.16/0.40	    a3(137) -> 138*
0.16/0.40	    a3(112) -> 113*
0.16/0.40	    a3(107) -> 108*
0.16/0.40	    a3(204) -> 205*
0.16/0.40	    a3(199) -> 200*
0.16/0.40	    a3(174) -> 175*
0.16/0.40	    a3(169) -> 170*
0.16/0.40	    a3(139) -> 140*
0.16/0.40	    a3(114) -> 115*
0.16/0.40	    a3(109) -> 110*
0.16/0.40	    a3(206) -> 207*
0.16/0.40	    a3(201) -> 202*
0.16/0.40	    a3(171) -> 172*
0.16/0.40	    a3(141) -> 142*
0.16/0.40	    a3(111) -> 112*
0.16/0.40	    a3(203) -> 204*
0.16/0.40	    a3(173) -> 174*
0.16/0.40	    a3(113) -> 114*
0.16/0.40	    a3(205) -> 206*
0.16/0.40	    a3(140) -> 141*
0.16/0.40	    a3(135) -> 136*
0.16/0.40	    1 -> 34*
0.16/0.40	    2 -> 4*
0.16/0.40	    9 -> 78*
0.16/0.40	    10 -> 64,36
0.16/0.40	    11 -> 76,62
0.16/0.40	    12 -> 58*
0.16/0.40	    13 -> 5,7,1
0.16/0.40	    35 -> 5*
0.16/0.40	    43 -> 198,66
0.16/0.40	    45 -> 69,7
0.16/0.40	    59 -> 5*
0.16/0.40	    63 -> 5*
0.16/0.40	    65 -> 5*
0.16/0.40	    71 -> 194*
0.16/0.40	    72 -> 106*
0.16/0.40	    73 -> 134,96
0.16/0.40	    74 -> 120*
0.16/0.40	    75 -> 39,7,37,9,65
0.16/0.40	    77 -> 67*
0.16/0.40	    79 -> 37*
0.16/0.40	    101 -> 240*
0.16/0.40	    102 -> 192*
0.16/0.40	    103 -> 248,176
0.16/0.40	    104 -> 144*
0.16/0.40	    105 -> 65,5,37,7,9,39
0.16/0.40	    115 -> 39*
0.16/0.40	    121 -> 37*
0.16/0.40	    139 -> 208*
0.16/0.40	    142 -> 166*
0.16/0.40	    143 -> 41*
0.16/0.40	    145 -> 37*
0.16/0.40	    173 -> 246*
0.16/0.40	    175 -> 201,69
0.16/0.40	    177 -> 67*
0.16/0.40	    193 -> 107*
0.16/0.40	    195 -> 107*
0.16/0.40	    205 -> 218*
0.16/0.40	    207 -> 107*
0.16/0.40	    217 -> 169*
0.16/0.40	    227 -> 111*
0.16/0.40	    241 -> 107*
0.16/0.40	    247 -> 199*
0.16/0.40	    249 -> 135*
0.16/0.40	  problem:
0.16/0.40	   
0.16/0.40	  Qed
0.16/0.40	EOF