YES(?,O(n^1))
0.16/0.31	YES(?,O(n^1))
0.16/0.31	
0.16/0.31	Problem:
0.16/0.31	 c(a(a(b(c(a(x1)))))) -> a(a(b(c(c(a(a(b(c(x1)))))))))
0.16/0.31	
0.16/0.31	Proof:
0.16/0.31	 Bounds Processor:
0.16/0.31	  bound: 3
0.16/0.31	  enrichment: match
0.16/0.31	  automaton:
0.16/0.31	   final states: {4}
0.16/0.31	   transitions:
0.16/0.31	    a3(89) -> 90*
0.16/0.31	    a3(84) -> 85*
0.16/0.31	    a3(111) -> 112*
0.16/0.31	    a3(106) -> 107*
0.16/0.31	    a3(88) -> 89*
0.16/0.31	    a3(83) -> 84*
0.16/0.31	    a3(110) -> 111*
0.16/0.31	    a3(105) -> 106*
0.16/0.31	    a1(22) -> 23*
0.16/0.31	    a1(17) -> 18*
0.16/0.31	    a1(23) -> 24*
0.16/0.31	    a1(18) -> 19*
0.16/0.31	    b3(87) -> 88*
0.16/0.31	    b3(82) -> 83*
0.16/0.31	    b3(109) -> 110*
0.16/0.31	    b3(104) -> 105*
0.16/0.31	    b1(21) -> 22*
0.16/0.31	    b1(16) -> 17*
0.16/0.31	    c3(107) -> 108*
0.16/0.31	    c3(86) -> 87*
0.16/0.31	    c3(81) -> 82*
0.16/0.31	    c3(108) -> 109*
0.16/0.31	    c3(103) -> 104*
0.16/0.31	    c3(85) -> 86*
0.16/0.31	    c1(75) -> 76*
0.16/0.31	    c1(20) -> 21*
0.16/0.31	    c1(15) -> 16*
0.16/0.31	    c1(39) -> 40*
0.16/0.31	    c1(19) -> 20*
0.16/0.31	    a2(32) -> 33*
0.16/0.31	    a2(27) -> 28*
0.16/0.31	    a2(59) -> 60*
0.16/0.31	    a2(54) -> 55*
0.16/0.31	    a2(58) -> 59*
0.16/0.31	    a2(53) -> 54*
0.16/0.31	    a2(33) -> 34*
0.16/0.31	    a2(28) -> 29*
0.16/0.31	    c0(4) -> 4*
0.16/0.31	    b2(57) -> 58*
0.16/0.31	    b2(52) -> 53*
0.16/0.31	    b2(31) -> 32*
0.16/0.31	    b2(26) -> 27*
0.16/0.31	    a0(4) -> 4*
0.16/0.31	    c2(55) -> 56*
0.16/0.31	    c2(30) -> 31*
0.16/0.31	    c2(25) -> 26*
0.16/0.31	    c2(29) -> 30*
0.16/0.32	    c2(91) -> 92*
0.16/0.32	    c2(56) -> 57*
0.16/0.32	    c2(51) -> 52*
0.16/0.32	    c2(63) -> 64*
0.16/0.32	    b0(4) -> 4*
0.16/0.32	    4 -> 15*
0.16/0.32	    22 -> 63*
0.16/0.32	    23 -> 39,25
0.16/0.32	    24 -> 16,20,4
0.16/0.32	    32 -> 103,91
0.16/0.32	    33 -> 81,75,51
0.16/0.32	    34 -> 30,16,21,20
0.16/0.32	    40 -> 16*
0.16/0.32	    60 -> 16,21
0.16/0.32	    64 -> 26*
0.16/0.32	    76 -> 16*
0.16/0.32	    90 -> 31*
0.16/0.32	    92 -> 26*
0.16/0.32	    112 -> 86,56
0.16/0.32	  problem:
0.16/0.32	   
0.16/0.32	  Qed
0.16/0.32	EOF