YES(?,O(n^1))
0.16/0.29	YES(?,O(n^1))
0.16/0.29	
0.16/0.29	Problem:
0.16/0.29	 c(a(b(a(x1)))) -> a(b(a(a(c(a(b(c(a(b(x1))))))))))
0.16/0.29	
0.16/0.29	Proof:
0.16/0.29	 Bounds Processor:
0.16/0.29	  bound: 3
0.16/0.29	  enrichment: match
0.16/0.29	  automaton:
0.16/0.29	   final states: {4}
0.16/0.29	   transitions:
0.16/0.29	    a3(117) -> 118*
0.16/0.29	    a3(112) -> 113*
0.16/0.29	    a3(94) -> 95*
0.16/0.29	    a3(96) -> 97*
0.16/0.29	    a3(91) -> 92*
0.16/0.29	    a3(118) -> 119*
0.16/0.29	    a3(93) -> 94*
0.16/0.29	    a3(88) -> 89*
0.16/0.29	    a3(120) -> 121*
0.16/0.29	    a3(115) -> 116*
0.16/0.29	    a1(25) -> 26*
0.16/0.29	    a1(20) -> 21*
0.16/0.29	    a1(22) -> 23*
0.16/0.29	    a1(17) -> 18*
0.16/0.29	    a1(23) -> 24*
0.16/0.29	    b3(87) -> 88*
0.16/0.29	    b3(119) -> 120*
0.16/0.29	    b3(114) -> 115*
0.16/0.29	    b3(111) -> 112*
0.16/0.29	    b3(98) -> 99*
0.16/0.29	    b3(95) -> 96*
0.16/0.29	    b3(90) -> 91*
0.16/0.29	    b1(27) -> 28*
0.16/0.29	    b1(24) -> 25*
0.16/0.29	    b1(19) -> 20*
0.16/0.29	    b1(16) -> 17*
0.16/0.29	    b1(33) -> 34*
0.16/0.29	    c3(92) -> 93*
0.16/0.29	    c3(89) -> 90*
0.16/0.29	    c3(116) -> 117*
0.16/0.29	    c3(113) -> 114*
0.16/0.29	    c1(21) -> 22*
0.16/0.29	    c1(18) -> 19*
0.16/0.29	    a2(70) -> 71*
0.16/0.29	    a2(72) -> 73*
0.16/0.29	    a2(67) -> 68*
0.16/0.29	    a2(42) -> 43*
0.16/0.29	    a2(69) -> 70*
0.16/0.29	    a2(64) -> 65*
0.16/0.29	    a2(44) -> 45*
0.16/0.29	    a2(39) -> 40*
0.16/0.29	    a2(41) -> 42*
0.16/0.29	    a2(36) -> 37*
0.16/0.29	    c0(4) -> 4*
0.16/0.29	    b2(50) -> 51*
0.16/0.29	    b2(35) -> 36*
0.16/0.29	    b2(71) -> 72*
0.16/0.29	    b2(66) -> 67*
0.16/0.29	    b2(63) -> 64*
0.16/0.29	    b2(43) -> 44*
0.16/0.29	    b2(38) -> 39*
0.16/0.29	    a0(4) -> 4*
0.16/0.29	    c2(65) -> 66*
0.16/0.29	    c2(40) -> 41*
0.16/0.29	    c2(37) -> 38*
0.16/0.29	    c2(68) -> 69*
0.16/0.29	    b0(4) -> 4*
0.16/0.29	    4 -> 16*
0.16/0.29	    22 -> 50*
0.16/0.29	    23 -> 27*
0.16/0.29	    25 -> 35,33
0.16/0.29	    26 -> 19,4
0.16/0.29	    28 -> 17*
0.16/0.29	    34 -> 17*
0.16/0.29	    44 -> 98,63
0.16/0.29	    45 -> 22,19
0.16/0.29	    51 -> 36*
0.16/0.29	    72 -> 87*
0.16/0.29	    73 -> 22*
0.16/0.29	    96 -> 111*
0.16/0.29	    97 -> 38*
0.16/0.29	    99 -> 88*
0.16/0.29	    121 -> 41*
0.16/0.29	  problem:
0.16/0.29	   
0.16/0.29	  Qed
0.16/0.29	EOF