YES(?,O(n^1))
3.45/1.17	YES(?,O(n^1))
3.45/1.17	
3.45/1.17	Problem:
3.45/1.17	 c(c(c(a(x,y)))) -> b(c(c(c(c(y)))),x)
3.45/1.17	 c(c(b(c(y),0()))) -> a(0(),c(c(a(y,0()))))
3.45/1.17	 c(c(a(a(y,0()),x))) -> c(y)
3.45/1.17	
3.45/1.17	Proof:
3.45/1.17	 Bounds Processor:
3.45/1.17	  bound: 3
3.45/1.17	  enrichment: match
3.45/1.17	  automaton:
3.45/1.17	   final states: {5}
3.45/1.17	   transitions:
3.45/1.17	    b3(85,5) -> 60,52
3.45/1.17	    b3(85,35) -> 60*
3.45/1.17	    b3(63,48) -> 62,55,54,63,25,24
3.45/1.17	    b3(85,24) -> 60,52
3.45/1.17	    b3(85,54) -> 60,52
3.45/1.17	    b3(85,62) -> 60,52
3.45/1.17	    c1(75) -> 76*
3.45/1.17	    c1(30) -> 31*
3.45/1.17	    c1(15) -> 16*
3.45/1.17	    c1(10) -> 11*
3.45/1.17	    c1(5) -> 63,55,62,54,61,53,60,52,51,25,24,23,13,22,12,11,17,5,10
3.45/1.17	    c1(12) -> 13*
3.45/1.17	    c1(94) -> 95*
3.45/1.17	    c1(76) -> 77*
3.45/1.17	    c1(31) -> 32*
3.45/1.17	    c1(16) -> 17*
3.45/1.17	    c1(11) -> 12*
3.45/1.17	    c1(93) -> 94*
3.45/1.17	    c3(60) -> 61*
3.45/1.17	    c3(87) -> 88*
3.45/1.17	    c3(82) -> 83*
3.45/1.17	    c3(62) -> 63*
3.45/1.17	    c3(84) -> 85*
3.45/1.17	    c3(66) -> 60*
3.45/1.17	    c3(61) -> 62*
3.45/1.17	    c3(51) -> 60*
3.45/1.17	    c3(88) -> 89*
3.45/1.17	    c3(83) -> 84*
3.45/1.17	    c3(48) -> 82*
3.45/1.17	    a1(12,14) -> 30*
3.45/1.17	    a1(14,77) -> 24*
3.45/1.17	    a1(14,95) -> 62,54
3.45/1.17	    a1(84,14) -> 93*
3.45/1.17	    a1(39,14) -> 75*
3.45/1.17	    a1(14,32) -> 63,55,62,54,61,53,52,51,60,25,24,23,13,22,17,12,11,5,10
3.45/1.17	    a1(14,66) -> 12,5,11
3.45/1.17	    a1(14,17) -> 23,24,25,22,17,13,12,11,10,5
3.45/1.17	    a1(5,14) -> 15*
3.45/1.17	    a1(14,51) -> 5,11
3.45/1.17	    a3(86,89) -> 61,62,55,54,53,63,25,23,24
3.45/1.17	    a3(62,86) -> 87*
3.45/1.17	    a3(54,86) -> 87*
3.45/1.17	    01() -> 14*
3.45/1.17	    03() -> 86*
3.45/1.17	    b1(13,5) -> 5*
3.45/1.17	    b1(5,5) -> 63,55,62,54,61,53,51,52,60,25,24,23,13,17,22,11,12,10
3.45/1.17	    b1(36,14) -> 11,5
3.45/1.17	    b1(63,14) -> 11,12,5,13
3.45/1.17	    b1(63,48) -> 11,12,5,13
3.45/1.17	    b1(55,14) -> 11,5,12
3.45/1.17	    b1(25,14) -> 5*
3.45/1.17	    b1(55,48) -> 11,5,12
3.45/1.17	    b2(40,5) -> 22*
3.45/1.17	    b2(36,14) -> 62,55,54,63,61,53,51,52,60,25,24,23,10,11,12,5,13,17,22
3.45/1.17	    b2(63,14) -> 63,55,62,54,61,53,51,52,60,10,11,23,12,5,13,22,17,24,25
3.45/1.17	    b2(63,48) -> 61,53,51,52,60,10,11,23,12,5,13,22,17
3.45/1.17	    b2(55,14) -> 10,11,13,5,12,22,17,24,23
3.45/1.17	    b2(40,12) -> 33*
3.45/1.17	    b2(25,14) -> 63,55,62,54,61,53,51,52,60,25,24,23,13,17,22,11,12,5,10
3.45/1.17	    b2(55,48) -> 61,53,51,52,60,10,11,13,5,12,22,17,23
3.45/1.17	    c0(5) -> 5*
3.45/1.17	    c2(65) -> 66*
3.45/1.17	    c2(50) -> 51*
3.45/1.17	    c2(35) -> 36*
3.45/1.17	    c2(52) -> 53*
3.45/1.17	    c2(37) -> 38*
3.45/1.17	    c2(32) -> 33*
3.45/1.17	    c2(22) -> 23*
3.45/1.17	    c2(17) -> 22*
3.45/1.17	    c2(64) -> 65*
3.45/1.17	    c2(54) -> 55*
3.45/1.17	    c2(49) -> 50*
3.45/1.17	    c2(39) -> 40*
3.45/1.17	    c2(34) -> 35*
3.45/1.17	    c2(24) -> 25*
3.45/1.17	    c2(14) -> 37*
3.45/1.17	    c2(51) -> 52*
3.45/1.17	    c2(53) -> 54*
3.45/1.17	    c2(38) -> 39*
3.45/1.17	    c2(33) -> 34*
3.45/1.17	    c2(23) -> 24*
3.45/1.17	    a0(5,5) -> 5*
3.45/1.17	    a2(62,48) -> 49*
3.45/1.17	    a2(48,51) -> 61,62,55,54,53,63,52,51,60,23,24,25,22,17,13,5,12,11,10
3.45/1.17	    a2(54,48) -> 49*
3.45/1.17	    a2(24,48) -> 49*
3.45/1.17	    a2(48,66) -> 61,62,55,54,53,63,52,51,60,23,24,17,22,12,5,13,11,10,25
3.45/1.17	    a2(35,48) -> 64*
3.45/1.17	    a2(5,48) -> 49*
3.45/1.17	    b0(5,5) -> 5*
3.45/1.17	    02() -> 48*
3.45/1.17	    00() -> 5*
3.45/1.17	  problem:
3.45/1.17	   
3.45/1.17	  Qed
3.45/1.17	EOF