YES(?,O(n^1))
0.16/0.42	YES(?,O(n^1))
0.16/0.42	
0.16/0.42	Problem:
0.16/0.42	 f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) ->
0.16/0.42	 f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))))))
0.16/0.42	
0.16/0.42	Proof:
0.16/0.42	 Bounds Processor:
0.16/0.42	  bound: 3
0.16/0.42	  enrichment: match
0.16/0.42	  automaton:
0.16/0.42	   final states: {4}
0.16/0.42	   transitions:
0.16/0.42	    f3(79,87) -> 88*
0.16/0.42	    f3(79,89) -> 90*
0.16/0.42	    f3(79,91) -> 92*
0.16/0.42	    f3(77,48) -> 78*
0.16/0.42	    f3(77,82) -> 83*
0.16/0.42	    f3(77,90) -> 91*
0.16/0.42	    f3(79,78) -> 80*
0.16/0.42	    f3(79,80) -> 81*
0.16/0.42	    f3(79,84) -> 85*
0.16/0.42	    f3(79,86) -> 93,41
0.16/0.42	    f3(79,88) -> 89*
0.16/0.42	    f3(79,92) -> 93*
0.16/0.42	    f3(79,94) -> 90,38
0.16/0.42	    f3(77,45) -> 87*
0.16/0.42	    f3(77,85) -> 86*
0.16/0.42	    f3(77,93) -> 94*
0.16/0.42	    f3(79,81) -> 82*
0.16/0.42	    f3(79,83) -> 84*
0.16/0.42	    f1(17,16) -> 18*
0.16/0.42	    f1(17,18) -> 19*
0.16/0.42	    f1(17,22) -> 23*
0.16/0.42	    f1(17,24) -> 37,19,4
0.16/0.42	    f1(15,19) -> 16*
0.16/0.42	    f1(15,23) -> 24*
0.16/0.42	    f1(17,19) -> 20*
0.16/0.42	    f1(17,21) -> 22*
0.16/0.42	    f1(15,4) -> 16*
0.16/0.42	    f1(15,20) -> 21*
0.16/0.42	    f1(15,22) -> 16*
0.16/0.42	    f1(15,24) -> 16*
0.16/0.42	    f1(15,34) -> 16*
0.16/0.42	    f1(15,42) -> 16*
0.16/0.42	    a3() -> 79*
0.16/0.42	    a1() -> 17*
0.16/0.42	    b3() -> 77*
0.16/0.42	    b1() -> 15*
0.16/0.42	    f2(27,26) -> 28*
0.16/0.42	    f2(27,28) -> 29*
0.16/0.42	    f2(27,32) -> 33*
0.16/0.42	    f2(27,34) -> 41,23
0.16/0.42	    f2(27,36) -> 37*
0.16/0.42	    f2(27,40) -> 41*
0.16/0.42	    f2(27,42) -> 38,20
0.16/0.42	    f2(27,44) -> 45*
0.16/0.42	    f2(27,48) -> 49*
0.16/0.42	    f2(27,50) -> 89,37,19
0.16/0.42	    f2(25,19) -> 35*
0.16/0.42	    f2(25,21) -> 43*
0.16/0.42	    f2(25,33) -> 34*
0.16/0.42	    f2(25,41) -> 42*
0.16/0.42	    f2(25,45) -> 35*
0.16/0.42	    f2(25,49) -> 50*
0.16/0.42	    f2(27,29) -> 30*
0.16/0.42	    f2(27,31) -> 32*
0.16/0.42	    f2(27,35) -> 36*
0.16/0.42	    f2(27,37) -> 38*
0.16/0.42	    f2(27,39) -> 40*
0.16/0.42	    f2(27,43) -> 44*
0.16/0.42	    f2(27,45) -> 46*
0.16/0.42	    f2(27,47) -> 48*
0.16/0.42	    f2(25,16) -> 43*
0.16/0.42	    f2(25,18) -> 43*
0.16/0.42	    f2(25,22) -> 26*
0.16/0.42	    f2(25,24) -> 43*
0.16/0.42	    f2(25,30) -> 31*
0.16/0.42	    f2(25,34) -> 26*
0.16/0.42	    f2(25,38) -> 39*
0.16/0.42	    f2(25,42) -> 35*
0.16/0.42	    f2(25,46) -> 47*
0.16/0.42	    f2(25,48) -> 26*
0.16/0.42	    f2(25,50) -> 43*
0.16/0.42	    f0(4,4) -> 4*
0.16/0.42	    a2() -> 27*
0.16/0.42	    a0() -> 4*
0.16/0.42	    b2() -> 25*
0.16/0.42	    b0() -> 4*
0.16/0.42	  problem:
0.16/0.42	   
0.16/0.42	  Qed
0.16/0.43	EOF