YES(?,O(n^1))
0.16/0.57	YES(?,O(n^1))
0.16/0.57	
0.16/0.57	Problem:
0.16/0.57	 h(f(x,y)) -> f(y,f(h(h(x)),a()))
0.16/0.57	
0.16/0.57	Proof:
0.16/0.57	 Bounds Processor:
0.16/0.57	  bound: 2
0.16/0.57	  enrichment: match
0.16/0.57	  automaton:
0.16/0.57	   final states: {3}
0.16/0.57	   transitions:
0.16/0.57	    f1(16,4) -> 17*
0.16/0.57	    f1(6,4) -> 7*
0.16/0.57	    f1(2,7) -> 19,5,3
0.16/0.57	    f1(2,17) -> 19,5,3
0.16/0.57	    f1(1,7) -> 19,5,3
0.16/0.57	    f1(1,17) -> 19,5,3
0.16/0.57	    h1(15) -> 16*
0.16/0.57	    h1(5) -> 6*
0.16/0.57	    h1(2) -> 15*
0.16/0.57	    h1(1) -> 5*
0.16/0.57	    a1() -> 4*
0.16/0.57	    f2(17,21) -> 20,6
0.16/0.57	    f2(7,21) -> 20,6
0.16/0.57	    f2(20,18) -> 21*
0.16/0.57	    h0(2) -> 3*
0.16/0.57	    h0(1) -> 3*
0.16/0.57	    h2(2) -> 19*
0.16/0.57	    h2(19) -> 20*
0.16/0.57	    h2(1) -> 19*
0.16/0.57	    f0(1,2) -> 1*
0.16/0.57	    f0(2,1) -> 1*
0.16/0.57	    f0(1,1) -> 1*
0.16/0.57	    f0(2,2) -> 1*
0.16/0.57	    a2() -> 18*
0.16/0.57	    a0() -> 2*
0.16/0.57	  problem:
0.16/0.57	   
0.16/0.57	  Qed
0.16/0.57	EOF