YES(?,O(n^1))
0.16/0.37	YES(?,O(n^1))
0.16/0.38	
0.16/0.38	Problem:
0.16/0.38	 b(a(b(a(a(x1))))) -> a(a(a(b(a(b(a(b(x1))))))))
0.16/0.38	
0.16/0.38	Proof:
0.16/0.38	 Bounds Processor:
0.16/0.38	  bound: 5
0.16/0.38	  enrichment: match
0.16/0.38	  automaton:
0.16/0.38	   final states: {2,1}
0.16/0.38	   transitions:
0.16/0.38	    b3(172) -> 173*
0.16/0.38	    b3(152) -> 153*
0.16/0.38	    b3(147) -> 148*
0.16/0.38	    b3(127) -> 128*
0.16/0.38	    b3(87) -> 88*
0.16/0.38	    b3(129) -> 130*
0.16/0.38	    b3(96) -> 97*
0.16/0.38	    b3(143) -> 144*
0.16/0.38	    b3(98) -> 99*
0.16/0.38	    b3(83) -> 84*
0.16/0.38	    b3(145) -> 146*
0.16/0.38	    b3(125) -> 126*
0.16/0.38	    b3(100) -> 101*
0.16/0.38	    b3(85) -> 86*
0.16/0.38	    a4(247) -> 248*
0.16/0.38	    a4(242) -> 243*
0.16/0.38	    a4(217) -> 218*
0.16/0.38	    a4(212) -> 213*
0.16/0.38	    a4(192) -> 193*
0.16/0.38	    a4(177) -> 178*
0.16/0.38	    a4(244) -> 245*
0.16/0.38	    a4(219) -> 220*
0.16/0.38	    a4(179) -> 180*
0.16/0.38	    a4(246) -> 247*
0.16/0.38	    a4(221) -> 222*
0.16/0.38	    a4(211) -> 212*
0.16/0.38	    a4(206) -> 207*
0.16/0.38	    a4(191) -> 192*
0.16/0.38	    a4(186) -> 187*
0.16/0.38	    a4(181) -> 182*
0.16/0.38	    a4(248) -> 249*
0.16/0.38	    a4(208) -> 209*
0.16/0.38	    a4(188) -> 189*
0.16/0.38	    a4(220) -> 221*
0.16/0.38	    a4(215) -> 216*
0.16/0.38	    a4(210) -> 211*
0.16/0.38	    a4(190) -> 191*
0.16/0.38	    a4(180) -> 181*
0.16/0.38	    a4(175) -> 176*
0.16/0.38	    b4(207) -> 208*
0.16/0.38	    b4(187) -> 188*
0.16/0.38	    b4(214) -> 215*
0.16/0.38	    b4(209) -> 210*
0.16/0.38	    b4(189) -> 190*
0.16/0.38	    b4(174) -> 175*
0.16/0.38	    b4(241) -> 242*
0.16/0.38	    b4(216) -> 217*
0.16/0.38	    b4(176) -> 177*
0.16/0.38	    b4(243) -> 244*
0.16/0.38	    b4(218) -> 219*
0.16/0.38	    b4(178) -> 179*
0.16/0.38	    b4(245) -> 246*
0.16/0.38	    b4(205) -> 206*
0.16/0.38	    b4(185) -> 186*
0.16/0.38	    b0(2) -> 1*
0.16/0.38	    b0(1) -> 1*
0.16/0.38	    a5(257) -> 258*
0.16/0.38	    a5(259) -> 260*
0.16/0.38	    a5(229) -> 230*
0.16/0.38	    a5(224) -> 225*
0.16/0.38	    a5(226) -> 227*
0.16/0.38	    a5(258) -> 259*
0.16/0.38	    a5(253) -> 254*
0.16/0.38	    a5(228) -> 229*
0.16/0.38	    a5(255) -> 256*
0.16/0.38	    a5(230) -> 231*
0.16/0.38	    a0(2) -> 2*
0.16/0.38	    a0(1) -> 2*
0.16/0.38	    b5(252) -> 253*
0.16/0.38	    b5(227) -> 228*
0.16/0.38	    b5(254) -> 255*
0.16/0.38	    b5(256) -> 257*
0.16/0.38	    b5(223) -> 224*
0.16/0.38	    b5(225) -> 226*
0.16/0.38	    a1(10) -> 11*
0.16/0.38	    a1(5) -> 6*
0.16/0.38	    a1(7) -> 8*
0.16/0.38	    a1(9) -> 10*
0.16/0.38	    a1(11) -> 12*
0.16/0.38	    b1(35) -> 36*
0.16/0.38	    b1(4) -> 5*
0.16/0.38	    b1(46) -> 47*
0.16/0.38	    b1(31) -> 32*
0.16/0.38	    b1(6) -> 7*
0.16/0.38	    b1(8) -> 9*
0.16/0.38	    a2(60) -> 61*
0.16/0.38	    a2(40) -> 41*
0.16/0.38	    a2(62) -> 63*
0.16/0.38	    a2(42) -> 43*
0.16/0.38	    a2(64) -> 65*
0.16/0.38	    a2(44) -> 45*
0.16/0.38	    a2(63) -> 64*
0.16/0.38	    a2(58) -> 59*
0.16/0.38	    a2(43) -> 44*
0.16/0.38	    a2(38) -> 39*
0.16/0.38	    b2(70) -> 71*
0.16/0.38	    b2(57) -> 58*
0.16/0.38	    b2(37) -> 38*
0.16/0.38	    b2(59) -> 60*
0.16/0.38	    b2(39) -> 40*
0.16/0.38	    b2(66) -> 67*
0.16/0.38	    b2(61) -> 62*
0.16/0.38	    b2(41) -> 42*
0.16/0.38	    b2(123) -> 124*
0.16/0.38	    a3(132) -> 133*
0.16/0.38	    a3(102) -> 103*
0.16/0.38	    a3(97) -> 98*
0.16/0.38	    a3(149) -> 150*
0.16/0.38	    a3(144) -> 145*
0.16/0.38	    a3(99) -> 100*
0.16/0.38	    a3(89) -> 90*
0.16/0.38	    a3(84) -> 85*
0.16/0.38	    a3(146) -> 147*
0.16/0.38	    a3(131) -> 132*
0.16/0.38	    a3(126) -> 127*
0.16/0.38	    a3(101) -> 102*
0.16/0.38	    a3(86) -> 87*
0.16/0.38	    a3(148) -> 149*
0.16/0.38	    a3(128) -> 129*
0.16/0.38	    a3(103) -> 104*
0.16/0.38	    a3(88) -> 89*
0.16/0.38	    a3(150) -> 151*
0.16/0.38	    a3(130) -> 131*
0.16/0.38	    a3(90) -> 91*
0.16/0.38	    1 -> 31*
0.16/0.38	    2 -> 4*
0.16/0.38	    9 -> 70*
0.16/0.38	    10 -> 46,37
0.16/0.38	    11 -> 66,35
0.16/0.38	    12 -> 5,7,1
0.16/0.38	    32 -> 5*
0.16/0.38	    36 -> 5*
0.16/0.38	    42 -> 83*
0.16/0.38	    44 -> 152,57
0.16/0.38	    45 -> 60,7
0.16/0.38	    47 -> 5*
0.16/0.38	    62 -> 172*
0.16/0.38	    63 -> 125*
0.16/0.38	    64 -> 123,96
0.16/0.38	    65 -> 40,7,38,9,47
0.16/0.38	    67 -> 58*
0.16/0.38	    71 -> 38*
0.16/0.38	    88 -> 205*
0.16/0.38	    90 -> 214,143
0.16/0.38	    91 -> 146,99,60
0.16/0.38	    102 -> 174*
0.16/0.38	    104 -> 42*
0.16/0.38	    124 -> 58*
0.16/0.38	    133 -> 40*
0.16/0.38	    148 -> 241*
0.16/0.38	    150 -> 185*
0.16/0.38	    151 -> 126*
0.16/0.38	    153 -> 144*
0.16/0.38	    173 -> 84*
0.16/0.38	    182 -> 86*
0.16/0.38	    193 -> 130*
0.16/0.38	    213 -> 217,146
0.16/0.38	    219 -> 252*
0.16/0.38	    221 -> 223*
0.16/0.38	    222 -> 175*
0.16/0.38	    231 -> 179*
0.16/0.38	    249 -> 188*
0.16/0.38	    260 -> 226*
0.16/0.38	  problem:
0.16/0.38	   
0.16/0.38	  Qed
0.16/0.38	EOF