YES(?,O(n^1))
0.15/0.32	YES(?,O(n^1))
0.15/0.32	
0.15/0.32	Problem:
0.15/0.32	 f(a()) -> g(h(a()))
0.15/0.32	 h(g(x)) -> g(h(f(x)))
0.15/0.32	 k(x,h(x),a()) -> h(x)
0.15/0.32	 k(f(x),y,x) -> f(x)
0.15/0.32	
0.15/0.32	Proof:
0.15/0.32	 Bounds Processor:
0.15/0.32	  bound: 2
0.15/0.32	  enrichment: match
0.15/0.32	  automaton:
0.15/0.32	   final states: {5,4,3}
0.15/0.32	   transitions:
0.15/0.32	    f0(2) -> 3*
0.15/0.32	    f0(1) -> 3*
0.15/0.32	    a0() -> 1*
0.15/0.32	    g0(2) -> 2*
0.15/0.32	    g0(1) -> 2*
0.15/0.32	    h0(2) -> 4*
0.15/0.32	    h0(1) -> 4*
0.15/0.32	    k0(1,1,1) -> 5*
0.15/0.32	    k0(2,2,1) -> 5*
0.15/0.32	    k0(1,1,2) -> 5*
0.15/0.32	    k0(2,2,2) -> 5*
0.15/0.32	    k0(1,2,1) -> 5*
0.15/0.32	    k0(2,1,1) -> 5*
0.15/0.32	    k0(1,2,2) -> 5*
0.15/0.32	    k0(2,1,2) -> 5*
0.15/0.32	    g1(10) -> 4*
0.15/0.32	    g1(4) -> 3*
0.15/0.32	    h1(1) -> 4*
0.15/0.32	    h1(3) -> 10*
0.15/0.32	    f1(2) -> 3*
0.15/0.32	    f1(1) -> 3*
0.15/0.32	    a1() -> 1*
0.15/0.32	    g2(15) -> 10*
0.15/0.32	    g2(4) -> 3*
0.15/0.32	    h2(14) -> 15*
0.15/0.32	    h2(1) -> 4*
0.15/0.32	    a2() -> 1*
0.15/0.32	    f2(4) -> 14*
0.15/0.32	  problem:
0.15/0.32	   
0.15/0.32	  Qed
0.15/0.32	EOF