YES(?,O(n^1))
0.16/0.27	YES(?,O(n^1))
0.16/0.27	
0.16/0.27	Problem:
0.16/0.27	 g(f(x,y),z) -> f(x,g(y,z))
0.16/0.27	 g(h(x,y),z) -> g(x,f(y,z))
0.16/0.27	 g(x,h(y,z)) -> h(g(x,y),z)
0.16/0.27	
0.16/0.27	Proof:
0.16/0.27	 Bounds Processor:
0.16/0.27	  bound: 1
0.16/0.27	  enrichment: match
0.16/0.27	  automaton:
0.16/0.27	   final states: {3}
0.16/0.27	   transitions:
0.16/0.27	    h1(5,1) -> 5,3
0.16/0.27	    h1(6,2) -> 5,3
0.16/0.27	    h1(5,2) -> 5,3
0.16/0.27	    h1(6,1) -> 5,3
0.16/0.27	    g1(1,2) -> 5*
0.16/0.27	    g1(1,10) -> 5,3
0.16/0.27	    g1(2,1) -> 5*
0.16/0.27	    g1(2,9) -> 5,3
0.16/0.27	    g1(1,1) -> 6*
0.16/0.27	    g1(1,9) -> 5,3
0.16/0.27	    g1(2,2) -> 5*
0.16/0.27	    g1(2,10) -> 5,3
0.16/0.27	    f1(1,2) -> 10*
0.16/0.27	    f1(1,6) -> 6,3
0.16/0.27	    f1(1,10) -> 9*
0.16/0.27	    f1(2,1) -> 9*
0.16/0.27	    f1(2,3) -> 3*
0.16/0.27	    f1(2,5) -> 5,6,3
0.16/0.27	    f1(2,9) -> 9*
0.16/0.27	    f1(1,1) -> 9*
0.16/0.27	    f1(1,3) -> 3*
0.16/0.27	    f1(1,5) -> 5,6,3
0.16/0.27	    f1(1,9) -> 9*
0.16/0.27	    f1(2,2) -> 9*
0.16/0.27	    f1(2,6) -> 6,3
0.16/0.27	    f1(2,10) -> 9*
0.16/0.27	    g0(1,2) -> 3*
0.16/0.27	    g0(2,1) -> 3*
0.16/0.27	    g0(1,1) -> 3*
0.16/0.27	    g0(2,2) -> 3*
0.16/0.27	    f0(1,2) -> 1*
0.16/0.27	    f0(2,1) -> 1*
0.16/0.27	    f0(1,1) -> 1*
0.16/0.27	    f0(2,2) -> 1*
0.16/0.27	    h0(1,2) -> 2*
0.16/0.27	    h0(2,1) -> 2*
0.16/0.27	    h0(1,1) -> 2*
0.16/0.27	    h0(2,2) -> 2*
0.16/0.27	  problem:
0.16/0.27	   
0.16/0.27	  Qed
0.16/0.27	EOF