YES(?,O(n^1))
0.16/0.25	YES(?,O(n^1))
0.16/0.26	
0.16/0.26	Problem:
0.16/0.26	 g(c(x,s(y))) -> g(c(s(x),y))
0.16/0.26	 f(c(s(x),y)) -> f(c(x,s(y)))
0.16/0.26	 f(f(x)) -> f(d(f(x)))
0.16/0.26	 f(x) -> x
0.16/0.26	
0.16/0.26	Proof:
0.16/0.26	 Bounds Processor:
0.16/0.26	  bound: 2
0.16/0.26	  enrichment: match
0.16/0.26	  automaton:
0.16/0.26	   final states: {6}
0.16/0.26	   transitions:
0.16/0.26	    f1(11) -> 12,6
0.16/0.26	    f1(6) -> 12*
0.16/0.26	    d1(12) -> 11*
0.16/0.26	    c1(9,6) -> 10*
0.16/0.26	    c1(9,9) -> 10*
0.16/0.26	    c1(6,9) -> 11*
0.16/0.26	    s1(9) -> 9*
0.16/0.26	    s1(6) -> 9*
0.16/0.26	    g1(10) -> 6*
0.16/0.26	    f2(14) -> 12*
0.16/0.26	    f2(11) -> 13*
0.16/0.26	    g0(6) -> 6*
0.16/0.26	    d2(13) -> 14*
0.16/0.26	    c0(6,6) -> 6*
0.16/0.26	    g2(17) -> 6,12
0.16/0.26	    s0(6) -> 6*
0.16/0.26	    c2(16,6) -> 17*
0.16/0.26	    c2(16,9) -> 17*
0.16/0.26	    f0(6) -> 6*
0.16/0.26	    s2(9) -> 16*
0.16/0.26	    s2(16) -> 16*
0.16/0.26	    d0(6) -> 6*
0.16/0.26	    6 -> 12*
0.16/0.26	    11 -> 13,6
0.16/0.26	    14 -> 12*
0.16/0.26	  problem:
0.16/0.26	   
0.16/0.26	  Qed
0.16/0.26	EOF