YES(?,O(n^1))
0.16/0.26	YES(?,O(n^1))
0.16/0.26	
0.16/0.26	Problem:
0.16/0.26	 a(f(),a(f(),x)) -> a(x,g())
0.16/0.26	 a(x,g()) -> a(f(),a(g(),a(f(),x)))
0.16/0.26	
0.16/0.26	Proof:
0.16/0.26	 Bounds Processor:
0.16/0.26	  bound: 4
0.16/0.26	  enrichment: match
0.16/0.26	  automaton:
0.16/0.26	   final states: {4}
0.16/0.26	   transitions:
0.16/0.26	    f3() -> 18*
0.16/0.26	    g3() -> 16*
0.16/0.26	    a4(27,26) -> 28*
0.16/0.26	    a4(25,15) -> 26*
0.16/0.26	    a4(25,20) -> 26*
0.16/0.26	    a4(25,28) -> 14*
0.16/0.26	    f4() -> 25*
0.16/0.26	    a0(4,4) -> 4*
0.16/0.26	    g4() -> 27*
0.16/0.26	    f0() -> 4*
0.16/0.26	    g0() -> 4*
0.16/0.26	    a1(4,6) -> 14,8,4
0.16/0.26	    a1(6,6) -> 4*
0.16/0.26	    a1(6,8) -> 6*
0.16/0.26	    a1(4,7) -> 8*
0.16/0.26	    a1(4,13) -> 8*
0.16/0.26	    a1(20,6) -> 4*
0.16/0.26	    a1(15,6) -> 4*
0.16/0.26	    a1(7,4) -> 8*
0.16/0.26	    f1() -> 4,7
0.16/0.26	    g1() -> 6*
0.16/0.26	    a2(13,15) -> 14,8,4
0.16/0.26	    a2(9,14) -> 15*
0.16/0.26	    a2(20,9) -> 8*
0.16/0.26	    a2(15,9) -> 8*
0.16/0.26	    a2(13,4) -> 14*
0.16/0.26	    a2(13,18) -> 29*
0.16/0.26	    a2(13,20) -> 4*
0.16/0.26	    a2(13,30) -> 19*
0.16/0.26	    a2(9,29) -> 30*
0.16/0.26	    a2(6,9) -> 14,8
0.16/0.26	    f2() -> 13*
0.16/0.26	    g2() -> 9*
0.16/0.26	    a3(18,15) -> 19*
0.16/0.26	    a3(16,8) -> 20*
0.16/0.26	    a3(18,6) -> 19*
0.16/0.26	    a3(18,20) -> 14,8
0.16/0.26	    a3(20,16) -> 14*
0.16/0.26	    a3(15,16) -> 14*
0.16/0.26	    a3(16,19) -> 20*
0.16/0.26	  problem:
0.16/0.26	   
0.16/0.26	  Qed
0.16/0.26	EOF