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(b(a(a(x1)))) -> a(a(b(a(a(b(c(b(a(c(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(137) -> 138*
0.16/0.29	    a3(132) -> 133*
0.16/0.29	    a3(102) -> 103*
0.16/0.29	    a3(97) -> 98*
0.16/0.29	    a3(139) -> 140*
0.16/0.29	    a3(129) -> 130*
0.16/0.29	    a3(104) -> 105*
0.16/0.29	    a3(136) -> 137*
0.16/0.29	    a3(126) -> 127*
0.16/0.29	    a3(121) -> 122*
0.16/0.29	    a3(101) -> 102*
0.16/0.29	    a3(128) -> 129*
0.16/0.29	    a3(140) -> 141*
0.16/0.29	    a3(125) -> 126*
0.16/0.29	    a3(105) -> 106*
0.16/0.29	    a1(25) -> 26*
0.16/0.29	    a1(22) -> 23*
0.16/0.29	    a1(17) -> 18*
0.16/0.29	    a1(24) -> 25*
0.16/0.29	    a1(21) -> 22*
0.16/0.29	    b3(127) -> 128*
0.16/0.29	    b3(122) -> 123*
0.16/0.29	    b3(124) -> 125*
0.16/0.29	    b3(138) -> 139*
0.16/0.29	    b3(133) -> 134*
0.16/0.29	    b3(103) -> 104*
0.16/0.29	    b3(98) -> 99*
0.16/0.29	    b3(135) -> 136*
0.16/0.29	    b3(100) -> 101*
0.16/0.29	    b1(20) -> 21*
0.16/0.29	    b1(23) -> 24*
0.16/0.29	    b1(18) -> 19*
0.16/0.29	    c3(134) -> 135*
0.16/0.29	    c3(99) -> 100*
0.16/0.29	    c3(131) -> 132*
0.16/0.29	    c3(96) -> 97*
0.16/0.29	    c3(123) -> 124*
0.16/0.29	    c3(120) -> 121*
0.16/0.29	    c1(27) -> 28*
0.16/0.29	    c1(19) -> 20*
0.16/0.29	    c1(16) -> 17*
0.16/0.29	    c1(33) -> 34*
0.16/0.29	    a2(55) -> 56*
0.16/0.29	    a2(45) -> 46*
0.16/0.29	    a2(40) -> 41*
0.16/0.29	    a2(47) -> 48*
0.16/0.29	    a2(94) -> 95*
0.16/0.29	    a2(59) -> 60*
0.16/0.29	    a2(44) -> 45*
0.16/0.29	    a2(91) -> 92*
0.16/0.29	    a2(86) -> 87*
0.16/0.29	    a2(56) -> 57*
0.16/0.29	    a2(51) -> 52*
0.16/0.29	    a2(93) -> 94*
0.16/0.29	    a2(58) -> 59*
0.16/0.29	    a2(48) -> 49*
0.16/0.29	    a2(90) -> 91*
0.16/0.29	    c0(4) -> 4*
0.16/0.29	    b2(92) -> 93*
0.16/0.29	    b2(87) -> 88*
0.16/0.29	    b2(57) -> 58*
0.16/0.29	    b2(52) -> 53*
0.16/0.29	    b2(89) -> 90*
0.16/0.29	    b2(54) -> 55*
0.16/0.29	    b2(46) -> 47*
0.16/0.29	    b2(41) -> 42*
0.16/0.29	    b2(43) -> 44*
0.16/0.29	    b0(4) -> 4*
0.16/0.29	    c2(50) -> 51*
0.16/0.29	    c2(72) -> 73*
0.16/0.29	    c2(42) -> 43*
0.16/0.29	    c2(39) -> 40*
0.16/0.29	    c2(88) -> 89*
0.16/0.29	    c2(53) -> 54*
0.16/0.29	    c2(85) -> 86*
0.16/0.29	    a0(4) -> 4*
0.16/0.29	    4 -> 16*
0.16/0.29	    21 -> 50*
0.16/0.29	    24 -> 27*
0.16/0.29	    25 -> 39,33
0.16/0.29	    26 -> 17,4
0.16/0.29	    28 -> 17*
0.16/0.29	    34 -> 17*
0.16/0.29	    44 -> 120*
0.16/0.29	    47 -> 85*
0.16/0.29	    49 -> 20*
0.16/0.29	    59 -> 72*
0.16/0.29	    60 -> 28,17
0.16/0.29	    73 -> 40*
0.16/0.29	    94 -> 96*
0.16/0.29	    95 -> 51*
0.16/0.29	    106 -> 54*
0.16/0.29	    129 -> 131*
0.16/0.29	    130 -> 86*
0.16/0.29	    141 -> 89*
0.16/0.29	  problem:
0.16/0.29	   
0.16/0.29	  Qed
0.16/0.29	EOF