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	 b(a(b(a(c(b(a(x1))))))) -> a(b(a(c(b(b(a(b(a(c(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(96) -> 97*
0.16/0.32	    a3(98) -> 99*
0.16/0.32	    a3(90) -> 91*
0.16/0.32	    a1(25) -> 26*
0.16/0.32	    a1(17) -> 18*
0.16/0.32	    a1(19) -> 20*
0.16/0.32	    a1(23) -> 24*
0.16/0.32	    b3(97) -> 98*
0.16/0.32	    b3(94) -> 95*
0.16/0.32	    b3(91) -> 92*
0.16/0.32	    b3(93) -> 94*
0.16/0.32	    b1(20) -> 21*
0.16/0.32	    b1(24) -> 25*
0.16/0.32	    b1(21) -> 22*
0.16/0.32	    b1(18) -> 19*
0.16/0.32	    c3(89) -> 90*
0.16/0.32	    c3(95) -> 96*
0.16/0.32	    c1(57) -> 58*
0.16/0.32	    c1(27) -> 28*
0.16/0.32	    c1(22) -> 23*
0.16/0.32	    c1(16) -> 17*
0.16/0.32	    a2(55) -> 56*
0.16/0.32	    a2(40) -> 41*
0.16/0.32	    a2(47) -> 48*
0.16/0.32	    a2(42) -> 43*
0.16/0.32	    a2(49) -> 50*
0.16/0.32	    a2(34) -> 35*
0.16/0.32	    a2(36) -> 37*
0.16/0.32	    a2(53) -> 54*
0.16/0.32	    b0(4) -> 4*
0.16/0.32	    b2(50) -> 51*
0.16/0.32	    b2(35) -> 36*
0.16/0.32	    b2(37) -> 38*
0.16/0.32	    b2(54) -> 55*
0.16/0.32	    b2(51) -> 52*
0.16/0.32	    b2(41) -> 42*
0.16/0.32	    b2(48) -> 49*
0.16/0.32	    b2(38) -> 39*
0.16/0.32	    a0(4) -> 4*
0.16/0.32	    c2(87) -> 88*
0.16/0.32	    c2(52) -> 53*
0.16/0.32	    c2(39) -> 40*
0.16/0.32	    c2(81) -> 82*
0.16/0.32	    c2(46) -> 47*
0.16/0.32	    c2(33) -> 34*
0.16/0.32	    c0(4) -> 4*
0.16/0.32	    4 -> 16*
0.16/0.32	    23 -> 46*
0.16/0.32	    25 -> 33,27
0.16/0.32	    26 -> 21,4
0.16/0.32	    28 -> 17*
0.16/0.32	    43 -> 22*
0.16/0.32	    53 -> 89,87
0.16/0.32	    55 -> 81,57
0.16/0.32	    56 -> 38,21
0.16/0.32	    58 -> 17*
0.16/0.32	    82 -> 34*
0.16/0.32	    88 -> 47*
0.16/0.32	    99 -> 38*
0.16/0.32	  problem:
0.16/0.32	   
0.16/0.32	  Qed
0.16/0.33	EOF