YES(?,O(n^1))
3.85/1.24	YES(?,O(n^1))
3.85/1.25	
3.85/1.25	Problem:
3.85/1.25	 b(a(b(a(a(a(x1)))))) -> a(a(a(b(a(b(a(b(a(x1)))))))))
3.85/1.25	
3.85/1.25	Proof:
3.85/1.25	 Bounds Processor:
3.85/1.25	  bound: 5
3.85/1.25	  enrichment: match
3.85/1.25	  automaton:
3.85/1.25	   final states: {2,1}
3.85/1.25	   transitions:
3.85/1.25	    b3(187) -> 188*
3.85/1.25	    b3(162) -> 163*
3.85/1.25	    b3(92) -> 93*
3.85/1.25	    b3(164) -> 165*
3.85/1.25	    b3(149) -> 150*
3.85/1.25	    b3(94) -> 95*
3.85/1.25	    b3(166) -> 167*
3.85/1.25	    b3(151) -> 152*
3.85/1.25	    b3(183) -> 184*
3.85/1.25	    b3(153) -> 154*
3.85/1.25	    b3(210) -> 211*
3.85/1.25	    b3(185) -> 186*
3.85/1.25	    b3(90) -> 91*
3.85/1.25	    a4(252) -> 253*
3.85/1.25	    a4(242) -> 243*
3.85/1.25	    a4(212) -> 213*
3.85/1.25	    a4(202) -> 203*
3.85/1.25	    a4(244) -> 245*
3.85/1.25	    a4(234) -> 235*
3.85/1.25	    a4(219) -> 220*
3.85/1.25	    a4(214) -> 215*
3.85/1.25	    a4(204) -> 205*
3.85/1.25	    a4(251) -> 252*
3.85/1.25	    a4(246) -> 247*
3.85/1.25	    a4(241) -> 242*
3.85/1.25	    a4(236) -> 237*
3.85/1.25	    a4(216) -> 217*
3.85/1.25	    a4(196) -> 197*
3.85/1.25	    a4(248) -> 249*
3.85/1.25	    a4(238) -> 239*
3.85/1.25	    a4(218) -> 219*
3.85/1.25	    a4(203) -> 204*
3.85/1.25	    a4(198) -> 199*
3.85/1.25	    a4(250) -> 251*
3.85/1.25	    a4(240) -> 241*
3.85/1.25	    a4(220) -> 221*
3.85/1.25	    a4(200) -> 201*
3.85/1.25	    b4(247) -> 248*
3.85/1.25	    b4(237) -> 238*
3.85/1.25	    b4(217) -> 218*
3.85/1.25	    b4(197) -> 198*
3.85/1.25	    b4(249) -> 250*
3.85/1.25	    b4(239) -> 240*
3.85/1.25	    b4(199) -> 200*
3.85/1.25	    b4(201) -> 202*
3.85/1.25	    b4(213) -> 214*
3.85/1.25	    b4(245) -> 246*
3.85/1.25	    b4(235) -> 236*
3.85/1.25	    b4(215) -> 216*
3.85/1.25	    b0(2) -> 1*
3.85/1.25	    b0(1) -> 1*
3.85/1.25	    a5(262) -> 263*
3.85/1.25	    a5(254) -> 255*
3.85/1.25	    a5(261) -> 262*
3.85/1.25	    a5(256) -> 257*
3.85/1.25	    a5(258) -> 259*
3.85/1.25	    a5(260) -> 261*
3.85/1.25	    a0(2) -> 2*
3.85/1.25	    a0(1) -> 2*
3.85/1.25	    b5(257) -> 258*
3.85/1.25	    b5(259) -> 260*
3.85/1.25	    b5(255) -> 256*
3.85/1.25	    a1(10) -> 11*
3.85/1.25	    a1(12) -> 13*
3.85/1.25	    a1(34) -> 35*
3.85/1.25	    a1(4) -> 5*
3.85/1.25	    a1(11) -> 12*
3.85/1.25	    a1(6) -> 7*
3.85/1.25	    a1(8) -> 9*
3.85/1.25	    b1(55) -> 56*
3.85/1.25	    b1(5) -> 6*
3.85/1.25	    b1(7) -> 8*
3.85/1.25	    b1(9) -> 10*
3.85/1.25	    b1(61) -> 62*
3.85/1.25	    b1(63) -> 64*
3.85/1.25	    a2(70) -> 71*
3.85/1.25	    a2(40) -> 41*
3.85/1.25	    a2(87) -> 88*
3.85/1.25	    a2(72) -> 73*
3.85/1.25	    a2(42) -> 43*
3.85/1.25	    a2(109) -> 110*
3.85/1.25	    a2(104) -> 105*
3.85/1.25	    a2(44) -> 45*
3.85/1.25	    a2(106) -> 107*
3.85/1.25	    a2(71) -> 72*
3.85/1.25	    a2(66) -> 67*
3.85/1.25	    a2(36) -> 37*
3.85/1.25	    a2(108) -> 109*
3.85/1.25	    a2(68) -> 69*
3.85/1.25	    a2(43) -> 44*
3.85/1.25	    a2(38) -> 39*
3.85/1.25	    a2(110) -> 111*
3.85/1.25	    b2(65) -> 66*
3.85/1.25	    b2(112) -> 113*
3.85/1.25	    b2(107) -> 108*
3.85/1.25	    b2(67) -> 68*
3.85/1.25	    b2(37) -> 38*
3.85/1.25	    b2(69) -> 70*
3.85/1.25	    b2(39) -> 40*
3.85/1.25	    b2(146) -> 147*
3.85/1.25	    b2(41) -> 42*
3.85/1.25	    b2(158) -> 159*
3.85/1.25	    b2(103) -> 104*
3.85/1.25	    b2(105) -> 106*
3.85/1.25	    a3(192) -> 193*
3.85/1.25	    a3(167) -> 168*
3.85/1.25	    a3(152) -> 153*
3.85/1.25	    a3(97) -> 98*
3.85/1.25	    a3(189) -> 190*
3.85/1.25	    a3(184) -> 185*
3.85/1.25	    a3(169) -> 170*
3.85/1.25	    a3(154) -> 155*
3.85/1.25	    a3(89) -> 90*
3.85/1.25	    a3(186) -> 187*
3.85/1.25	    a3(171) -> 172*
3.85/1.25	    a3(156) -> 157*
3.85/1.25	    a3(96) -> 97*
3.85/1.25	    a3(91) -> 92*
3.85/1.25	    a3(188) -> 189*
3.85/1.25	    a3(168) -> 169*
3.85/1.25	    a3(163) -> 164*
3.85/1.25	    a3(148) -> 149*
3.85/1.25	    a3(133) -> 134*
3.85/1.25	    a3(93) -> 94*
3.85/1.25	    a3(190) -> 191*
3.85/1.25	    a3(165) -> 166*
3.85/1.25	    a3(155) -> 156*
3.85/1.25	    a3(150) -> 151*
3.85/1.25	    a3(95) -> 96*
3.85/1.25	    1 -> 34*
3.85/1.25	    2 -> 4*
3.85/1.25	    10 -> 87*
3.85/1.25	    11 -> 63,36
3.85/1.25	    12 -> 61*
3.85/1.25	    13 -> 6,55,8,1
3.85/1.25	    35 -> 5*
3.85/1.25	    42 -> 148*
3.85/1.25	    43 -> 89*
3.85/1.25	    44 -> 65*
3.85/1.25	    45 -> 38,103,64,6,10,8
3.85/1.25	    56 -> 6*
3.85/1.25	    62 -> 6*
3.85/1.25	    64 -> 6*
3.85/1.25	    70 -> 192*
3.85/1.25	    71 -> 133*
3.85/1.25	    72 -> 112*
3.85/1.25	    73 -> 146,38,8,10,64,6
3.85/1.25	    88 -> 37*
3.85/1.25	    95 -> 234*
3.85/1.25	    96 -> 196*
3.85/1.25	    97 -> 162*
3.85/1.25	    98 -> 183,42,40
3.85/1.25	    109 -> 171*
3.85/1.25	    110 -> 158*
3.85/1.25	    111 -> 8,40
3.85/1.25	    113 -> 38*
3.85/1.25	    134 -> 90*
3.85/1.25	    147 -> 104*
3.85/1.25	    157 -> 106*
3.85/1.25	    159 -> 38*
3.85/1.25	    168 -> 212*
3.85/1.25	    170 -> 150*
3.85/1.25	    172 -> 162*
3.85/1.25	    189 -> 244*
3.85/1.25	    190 -> 210*
3.85/1.25	    191 -> 93,68
3.85/1.25	    193 -> 149*
3.85/1.25	    205 -> 152*
3.85/1.25	    211 -> 163*
3.85/1.25	    221 -> 154*
3.85/1.25	    243 -> 186*
3.85/1.25	    251 -> 254*
3.85/1.25	    253 -> 236*
3.85/1.25	    263 -> 240*
3.85/1.25	  problem:
3.85/1.25	   
3.85/1.25	  Qed
3.85/1.25	EOF