YES(?,O(n^1))
0.15/0.33	YES(?,O(n^1))
0.15/0.33	
0.15/0.33	Problem:
0.15/0.33	 b(c(a(x1))) -> a(b(a(b(x1))))
0.15/0.33	 b(x1) -> c(c(x1))
0.15/0.33	 a(a(x1)) -> a(c(b(a(x1))))
0.15/0.33	
0.15/0.33	Proof:
0.15/0.33	 Bounds Processor:
0.15/0.33	  bound: 4
0.15/0.33	  enrichment: match
0.15/0.33	  automaton:
0.15/0.33	   final states: {4}
0.15/0.33	   transitions:
0.15/0.33	    a3(121) -> 122*
0.15/0.33	    a3(118) -> 119*
0.15/0.33	    b3(119) -> 120*
0.15/0.33	    c4(127) -> 128*
0.15/0.33	    c4(126) -> 127*
0.15/0.33	    b0(4) -> 4*
0.15/0.33	    c0(4) -> 4*
0.15/0.33	    a0(4) -> 4*
0.15/0.33	    a1(22) -> 23*
0.15/0.33	    a1(11) -> 12*
0.15/0.33	    a1(13) -> 14*
0.15/0.33	    c1(15) -> 16*
0.15/0.33	    c1(24) -> 25*
0.15/0.33	    c1(16) -> 17*
0.15/0.33	    c1(53) -> 54*
0.15/0.33	    b1(10) -> 11*
0.15/0.33	    b1(12) -> 13*
0.15/0.33	    b1(26) -> 27*
0.15/0.33	    b1(23) -> 24*
0.15/0.33	    a2(65) -> 66*
0.15/0.33	    a2(55) -> 56*
0.15/0.33	    a2(67) -> 68*
0.15/0.33	    a2(58) -> 59*
0.15/0.33	    c2(77) -> 78*
0.15/0.33	    c2(57) -> 58*
0.15/0.33	    c2(47) -> 48*
0.15/0.33	    c2(44) -> 45*
0.15/0.33	    c2(34) -> 35*
0.15/0.33	    c2(46) -> 47*
0.15/0.33	    c2(78) -> 79*
0.15/0.33	    c2(43) -> 44*
0.15/0.33	    c2(33) -> 34*
0.15/0.33	    b2(64) -> 65*
0.15/0.33	    b2(66) -> 67*
0.15/0.33	    b2(56) -> 57*
0.15/0.33	    b2(93) -> 94*
0.15/0.33	    b2(105) -> 106*
0.15/0.33	    c3(80) -> 81*
0.15/0.33	    c3(107) -> 108*
0.15/0.33	    c3(97) -> 98*
0.15/0.33	    c3(116) -> 117*
0.15/0.33	    c3(101) -> 102*
0.15/0.33	    c3(81) -> 82*
0.15/0.33	    c3(108) -> 109*
0.15/0.33	    c3(98) -> 99*
0.15/0.33	    c3(120) -> 121*
0.15/0.33	    c3(115) -> 116*
0.15/0.33	    c3(100) -> 101*
0.15/0.33	    4 -> 22,15,10
0.15/0.33	    10 -> 46*
0.15/0.33	    11 -> 53*
0.15/0.33	    12 -> 33*
0.15/0.33	    13 -> 64,55,26
0.15/0.33	    14 -> 23,11,4
0.15/0.33	    17 -> 4*
0.15/0.33	    23 -> 43*
0.15/0.33	    25 -> 13*
0.15/0.33	    26 -> 77*
0.15/0.33	    27 -> 11*
0.15/0.33	    35 -> 13*
0.15/0.33	    45 -> 24*
0.15/0.33	    48 -> 11*
0.15/0.33	    54 -> 13*
0.15/0.33	    56 -> 80*
0.15/0.33	    59 -> 12,33,23
0.15/0.33	    64 -> 100*
0.15/0.33	    66 -> 97*
0.15/0.33	    67 -> 118,93
0.15/0.33	    68 -> 105,65,27,11,53
0.15/0.33	    79 -> 27*
0.15/0.33	    82 -> 57*
0.15/0.33	    93 -> 107*
0.15/0.33	    94 -> 65*
0.15/0.33	    99 -> 67*
0.15/0.33	    102 -> 65*
0.15/0.33	    105 -> 115*
0.15/0.33	    106 -> 57*
0.15/0.33	    109 -> 94*
0.15/0.33	    117 -> 106*
0.15/0.33	    119 -> 126*
0.15/0.33	    122 -> 66,97
0.15/0.33	    128 -> 120*
0.15/0.33	  problem:
0.15/0.33	   
0.15/0.33	  Qed
0.15/0.33	EOF