YES(?,O(n^1))
0.16/0.34	YES(?,O(n^1))
0.16/0.34	
0.16/0.34	Problem:
0.16/0.34	 c(a(b(a(b(x1))))) -> a(b(a(b(b(a(b(b(c(a(b(c(a(x1)))))))))))))
0.16/0.34	
0.16/0.34	Proof:
0.16/0.34	 Bounds Processor:
0.16/0.34	  bound: 3
0.16/0.34	  enrichment: match
0.16/0.34	  automaton:
0.16/0.34	   final states: {4}
0.16/0.34	   transitions:
0.16/0.34	    a3(122) -> 123*
0.16/0.34	    a3(129) -> 130*
0.16/0.34	    a3(119) -> 120*
0.16/0.34	    a3(131) -> 132*
0.16/0.34	    a3(126) -> 127*
0.16/0.34	    a1(22) -> 23*
0.16/0.34	    a1(39) -> 40*
0.16/0.34	    a1(29) -> 30*
0.16/0.34	    a1(19) -> 20*
0.16/0.34	    a1(31) -> 32*
0.16/0.34	    a1(26) -> 27*
0.16/0.34	    a1(33) -> 34*
0.16/0.34	    b3(127) -> 128*
0.16/0.34	    b3(124) -> 125*
0.16/0.34	    b3(121) -> 122*
0.16/0.34	    b3(128) -> 129*
0.16/0.34	    b3(130) -> 131*
0.16/0.34	    b3(125) -> 126*
0.16/0.34	    b1(30) -> 31*
0.16/0.34	    b1(25) -> 26*
0.16/0.34	    b1(27) -> 28*
0.16/0.34	    b1(24) -> 25*
0.16/0.34	    b1(21) -> 22*
0.16/0.34	    b1(28) -> 29*
0.16/0.34	    c3(123) -> 124*
0.16/0.34	    c3(120) -> 121*
0.16/0.34	    c1(20) -> 21*
0.16/0.34	    c1(23) -> 24*
0.16/0.34	    a2(55) -> 56*
0.16/0.34	    a2(45) -> 46*
0.16/0.34	    a2(92) -> 93*
0.16/0.34	    a2(87) -> 88*
0.16/0.34	    a2(62) -> 63*
0.16/0.34	    a2(57) -> 58*
0.16/0.34	    a2(52) -> 53*
0.16/0.34	    a2(99) -> 100*
0.16/0.34	    a2(89) -> 90*
0.16/0.34	    a2(69) -> 70*
0.16/0.34	    a2(59) -> 60*
0.16/0.34	    a2(101) -> 102*
0.16/0.34	    a2(96) -> 97*
0.16/0.34	    a2(71) -> 72*
0.16/0.34	    a2(66) -> 67*
0.16/0.34	    a2(48) -> 49*
0.16/0.34	    c0(4) -> 4*
0.16/0.34	    b2(70) -> 71*
0.16/0.34	    b2(65) -> 66*
0.16/0.34	    b2(50) -> 51*
0.16/0.34	    b2(97) -> 98*
0.16/0.34	    b2(67) -> 68*
0.16/0.34	    b2(47) -> 48*
0.16/0.34	    b2(94) -> 95*
0.16/0.34	    b2(64) -> 65*
0.16/0.34	    b2(54) -> 55*
0.16/0.34	    b2(91) -> 92*
0.16/0.34	    b2(61) -> 62*
0.16/0.34	    b2(56) -> 57*
0.16/0.34	    b2(51) -> 52*
0.16/0.34	    b2(98) -> 99*
0.16/0.34	    b2(68) -> 69*
0.16/0.34	    b2(53) -> 54*
0.16/0.34	    b2(100) -> 101*
0.16/0.34	    b2(95) -> 96*
0.16/0.34	    a0(4) -> 4*
0.16/0.34	    c2(60) -> 61*
0.16/0.34	    c2(49) -> 50*
0.16/0.34	    c2(46) -> 47*
0.16/0.34	    c2(93) -> 94*
0.16/0.34	    c2(63) -> 64*
0.16/0.34	    c2(90) -> 91*
0.16/0.34	    b0(4) -> 4*
0.16/0.34	    4 -> 19*
0.16/0.34	    25 -> 59*
0.16/0.34	    28 -> 33*
0.16/0.34	    30 -> 45,39
0.16/0.34	    32 -> 21,4
0.16/0.34	    34 -> 20*
0.16/0.34	    40 -> 20*
0.16/0.34	    56 -> 89*
0.16/0.34	    58 -> 24*
0.16/0.34	    70 -> 87*
0.16/0.34	    72 -> 21*
0.16/0.34	    88 -> 46*
0.16/0.34	    100 -> 119*
0.16/0.34	    102 -> 61*
0.16/0.34	    132 -> 64*
0.16/0.34	  problem:
0.16/0.34	   
0.16/0.34	  Qed
0.16/0.34	EOF