YES(?,O(n^1))
0.16/0.27	YES(?,O(n^1))
0.16/0.28	
0.16/0.28	Problem:
0.16/0.28	 f(c(X,s(Y))) -> f(c(s(X),Y))
0.16/0.28	 g(c(s(X),Y)) -> f(c(X,s(Y)))
0.16/0.28	
0.16/0.28	Proof:
0.16/0.28	 Bounds Processor:
0.16/0.28	  bound: 4
0.16/0.28	  enrichment: match
0.16/0.28	  automaton:
0.16/0.28	   final states: {5}
0.16/0.28	   transitions:
0.16/0.28	    s3(10) -> 13*
0.16/0.28	    s3(13) -> 13*
0.16/0.28	    f1(9) -> 5*
0.16/0.28	    f4(18) -> 5*
0.16/0.28	    c1(8,5) -> 9*
0.16/0.28	    c1(5,8) -> 9*
0.16/0.28	    c4(17,13) -> 18*
0.16/0.28	    c4(17,10) -> 18*
0.16/0.28	    s1(10) -> 8*
0.16/0.28	    s1(5) -> 8*
0.16/0.28	    s1(13) -> 8*
0.16/0.28	    s1(8) -> 8*
0.16/0.28	    s4(17) -> 17*
0.16/0.28	    s4(13) -> 17*
0.16/0.28	    f2(11) -> 5*
0.16/0.28	    c2(10,5) -> 11*
0.16/0.28	    c2(10,13) -> 11*
0.16/0.28	    c2(10,8) -> 11*
0.16/0.28	    c2(10,10) -> 11*
0.16/0.28	    f0(5) -> 5*
0.16/0.28	    s2(10) -> 10*
0.16/0.28	    s2(5) -> 10*
0.16/0.28	    c0(5,5) -> 5*
0.16/0.28	    f3(14) -> 5*
0.16/0.28	    s0(5) -> 5*
0.16/0.28	    c3(13,5) -> 14*
0.16/0.28	    c3(13,13) -> 14*
0.16/0.28	    c3(17,5) -> 14*
0.16/0.28	    c3(13,10) -> 14*
0.16/0.28	    g0(5) -> 5*
0.16/0.28	  problem:
0.16/0.28	   
0.16/0.28	  Qed
0.16/0.28	EOF