YES(?,O(n^1))
0.16/0.32	YES(?,O(n^1))
0.16/0.32	
0.16/0.32	Problem:
0.16/0.32	 a(b(a(a(x1)))) -> c(b(a(b(a(x1)))))
0.16/0.32	 a(c(b(x1))) -> a(a(b(c(b(a(x1))))))
0.16/0.32	
0.16/0.32	Proof:
0.16/0.32	 Bounds Processor:
0.16/0.32	  bound: 3
0.16/0.32	  enrichment: match
0.16/0.32	  automaton:
0.16/0.32	   final states: {4}
0.16/0.32	   transitions:
0.16/0.32	    a3(92) -> 93*
0.16/0.32	    a3(93) -> 94*
0.16/0.32	    a3(88) -> 89*
0.16/0.32	    a1(20) -> 21*
0.16/0.32	    a1(49) -> 50*
0.16/0.32	    a1(19) -> 20*
0.16/0.32	    a1(11) -> 12*
0.16/0.32	    a1(13) -> 14*
0.16/0.32	    b3(89) -> 90*
0.16/0.32	    b3(91) -> 92*
0.16/0.32	    b1(45) -> 46*
0.16/0.32	    b1(12) -> 13*
0.16/0.32	    b1(14) -> 15*
0.16/0.32	    b1(43) -> 44*
0.16/0.32	    b1(18) -> 19*
0.16/0.32	    c3(90) -> 91*
0.16/0.32	    c1(15) -> 16*
0.16/0.32	    c1(17) -> 18*
0.16/0.32	    a2(57) -> 58*
0.16/0.32	    a2(84) -> 85*
0.16/0.32	    a2(79) -> 80*
0.16/0.32	    a2(64) -> 65*
0.16/0.32	    a2(26) -> 27*
0.16/0.32	    a2(83) -> 84*
0.16/0.32	    a2(73) -> 74*
0.16/0.32	    a2(58) -> 59*
0.16/0.32	    a2(53) -> 54*
0.16/0.32	    a2(28) -> 29*
0.16/0.32	    a0(4) -> 4*
0.16/0.32	    b2(102) -> 103*
0.16/0.32	    b2(82) -> 83*
0.16/0.32	    b2(62) -> 63*
0.16/0.32	    b2(27) -> 28*
0.16/0.32	    b2(54) -> 55*
0.16/0.32	    b2(29) -> 30*
0.16/0.32	    b2(56) -> 57*
0.16/0.32	    b2(80) -> 81*
0.16/0.32	    b0(4) -> 4*
0.16/0.32	    c2(55) -> 56*
0.16/0.32	    c2(30) -> 31*
0.16/0.32	    c2(81) -> 82*
0.16/0.32	    c0(4) -> 4*
0.16/0.32	    4 -> 11*
0.16/0.32	    13 -> 73,17
0.16/0.32	    14 -> 53,49
0.16/0.32	    16 -> 74,27,12,14,4
0.16/0.32	    19 -> 64*
0.16/0.32	    20 -> 43,26
0.16/0.32	    21 -> 12,45,4
0.16/0.32	    29 -> 88,79
0.16/0.32	    31 -> 74,27,29,14
0.16/0.32	    44 -> 13*
0.16/0.32	    46 -> 13*
0.16/0.32	    50 -> 12*
0.16/0.32	    58 -> 62*
0.16/0.32	    59 -> 54,50,12
0.16/0.32	    63 -> 28*
0.16/0.32	    65 -> 27*
0.16/0.32	    74 -> 27*
0.16/0.32	    84 -> 102*
0.16/0.32	    85 -> 50*
0.16/0.32	    94 -> 89,80,54
0.16/0.32	    103 -> 28*
0.16/0.32	  problem:
0.16/0.32	   
0.16/0.32	  Qed
0.16/0.32	EOF