YES(?,O(n^1))
0.15/0.35	YES(?,O(n^1))
0.15/0.36	
0.15/0.36	Problem:
0.15/0.36	 b(a(a(b(a(b(a(x1))))))) -> a(a(b(a(b(b(a(a(b(x1)))))))))
0.15/0.36	
0.15/0.36	Proof:
0.15/0.36	 Bounds Processor:
0.15/0.36	  bound: 4
0.15/0.36	  enrichment: match
0.15/0.36	  automaton:
0.15/0.36	   final states: {3}
0.15/0.36	   transitions:
0.15/0.36	    b3(182) -> 183*
0.15/0.36	    b3(122) -> 123*
0.15/0.36	    b3(164) -> 165*
0.15/0.36	    b3(154) -> 155*
0.15/0.36	    b3(166) -> 167*
0.15/0.36	    b3(156) -> 157*
0.15/0.36	    b3(126) -> 127*
0.15/0.36	    b3(153) -> 154*
0.15/0.36	    b3(128) -> 129*
0.15/0.36	    b3(150) -> 151*
0.15/0.36	    b3(125) -> 126*
0.15/0.36	    a4(189) -> 190*
0.15/0.36	    a4(196) -> 197*
0.15/0.36	    a4(193) -> 194*
0.15/0.36	    a4(195) -> 196*
0.15/0.36	    a4(190) -> 191*
0.15/0.36	    b4(192) -> 193*
0.15/0.36	    b4(194) -> 195*
0.15/0.36	    b4(191) -> 192*
0.15/0.36	    b4(188) -> 189*
0.15/0.36	    b0(3) -> 3*
0.15/0.36	    a0(3) -> 3*
0.15/0.36	    a1(25) -> 26*
0.15/0.36	    a1(15) -> 16*
0.15/0.36	    a1(32) -> 33*
0.15/0.36	    a1(22) -> 23*
0.15/0.36	    a1(29) -> 30*
0.15/0.36	    a1(19) -> 20*
0.15/0.36	    a1(31) -> 32*
0.15/0.36	    a1(26) -> 27*
0.15/0.36	    a1(21) -> 22*
0.15/0.36	    a1(16) -> 17*
0.15/0.36	    b1(30) -> 31*
0.15/0.36	    b1(20) -> 21*
0.15/0.36	    b1(27) -> 28*
0.15/0.36	    b1(17) -> 18*
0.15/0.36	    b1(24) -> 25*
0.15/0.36	    b1(14) -> 15*
0.15/0.36	    b1(96) -> 97*
0.15/0.36	    b1(46) -> 47*
0.15/0.36	    b1(148) -> 149*
0.15/0.36	    b1(28) -> 29*
0.15/0.36	    b1(18) -> 19*
0.15/0.36	    a2(65) -> 66*
0.15/0.36	    a2(60) -> 61*
0.15/0.36	    a2(87) -> 88*
0.15/0.36	    a2(109) -> 110*
0.15/0.36	    a2(89) -> 90*
0.15/0.36	    a2(84) -> 85*
0.15/0.36	    a2(59) -> 60*
0.15/0.36	    a2(116) -> 117*
0.15/0.36	    a2(66) -> 67*
0.15/0.36	    a2(113) -> 114*
0.15/0.36	    a2(83) -> 84*
0.15/0.36	    a2(63) -> 64*
0.15/0.36	    a2(115) -> 116*
0.15/0.36	    a2(110) -> 111*
0.15/0.36	    a2(90) -> 91*
0.15/0.36	    b2(132) -> 133*
0.15/0.36	    b2(112) -> 113*
0.15/0.36	    b2(82) -> 83*
0.15/0.36	    b2(62) -> 63*
0.15/0.36	    b2(134) -> 135*
0.15/0.36	    b2(114) -> 115*
0.15/0.36	    b2(94) -> 95*
0.15/0.36	    b2(64) -> 65*
0.15/0.36	    b2(111) -> 112*
0.15/0.36	    b2(86) -> 87*
0.15/0.36	    b2(61) -> 62*
0.15/0.36	    b2(108) -> 109*
0.15/0.36	    b2(88) -> 89*
0.15/0.36	    b2(68) -> 69*
0.15/0.36	    b2(58) -> 59*
0.15/0.36	    b2(180) -> 181*
0.15/0.36	    b2(85) -> 86*
0.15/0.36	    a3(157) -> 158*
0.15/0.36	    a3(152) -> 153*
0.15/0.36	    a3(127) -> 128*
0.15/0.36	    a3(129) -> 130*
0.15/0.36	    a3(124) -> 125*
0.15/0.36	    a3(151) -> 152*
0.15/0.36	    a3(158) -> 159*
0.15/0.36	    a3(123) -> 124*
0.15/0.36	    a3(155) -> 156*
0.15/0.36	    a3(130) -> 131*
0.15/0.36	    3 -> 14*
0.15/0.36	    19 -> 82*
0.15/0.36	    22 -> 68,24
0.15/0.36	    23 -> 18,15,3
0.15/0.36	    29 -> 108*
0.15/0.36	    32 -> 58,46
0.15/0.36	    33 -> 18,3,14,15
0.15/0.36	    47 -> 15*
0.15/0.36	    67 -> 15,19
0.15/0.36	    69 -> 59*
0.15/0.36	    87 -> 132,122
0.15/0.36	    90 -> 164,96,94
0.15/0.36	    91 -> 62,28
0.15/0.36	    95 -> 59*
0.15/0.36	    97 -> 15*
0.15/0.36	    113 -> 182,180
0.15/0.36	    116 -> 150,148,134
0.15/0.36	    117 -> 62,18
0.15/0.36	    127 -> 188*
0.15/0.36	    130 -> 166*
0.15/0.36	    131 -> 154,62
0.15/0.36	    133 -> 109*
0.15/0.36	    135 -> 59*
0.15/0.36	    149 -> 15*
0.15/0.36	    159 -> 83*
0.15/0.36	    165 -> 151*
0.15/0.36	    167 -> 151*
0.15/0.36	    181 -> 109*
0.15/0.36	    183 -> 123*
0.15/0.36	    197 -> 154*
0.15/0.36	  problem:
0.15/0.36	   
0.15/0.36	  Qed
0.15/0.36	EOF