YES(?,O(n^1))
0.16/0.24	YES(?,O(n^1))
0.16/0.24	
0.16/0.24	Problem:
0.16/0.24	 f(a(),a()) -> f(a(),b())
0.16/0.24	 f(a(),b()) -> f(s(a()),c())
0.16/0.24	 f(s(X),c()) -> f(X,c())
0.16/0.24	 f(c(),c()) -> f(a(),a())
0.16/0.24	
0.16/0.24	Proof:
0.16/0.24	 Bounds Processor:
0.16/0.24	  bound: 4
0.16/0.24	  enrichment: match
0.16/0.24	  automaton:
0.16/0.24	   final states: {6}
0.16/0.24	   transitions:
0.16/0.24	    c3() -> 15*
0.16/0.24	    s3(16) -> 17*
0.16/0.24	    a3() -> 16*
0.16/0.24	    f4(16,20) -> 6*
0.16/0.24	    c4() -> 20*
0.16/0.24	    f0(6,6) -> 6*
0.16/0.24	    a0() -> 6*
0.16/0.24	    b0() -> 6*
0.16/0.24	    s0(6) -> 6*
0.16/0.24	    c0() -> 6*
0.16/0.24	    f1(10,9) -> 6*
0.16/0.24	    f1(10,10) -> 6*
0.16/0.24	    f1(6,9) -> 6*
0.16/0.24	    a1() -> 10*
0.16/0.24	    c1() -> 9*
0.16/0.24	    s1(10) -> 10*
0.16/0.24	    b1() -> 9*
0.16/0.24	    f2(10,13) -> 6*
0.16/0.24	    f2(14,13) -> 6*
0.16/0.24	    c2() -> 13*
0.16/0.24	    s2(14) -> 14*
0.16/0.24	    a2() -> 14*
0.16/0.24	    b2() -> 13*
0.16/0.24	    f3(17,15) -> 6*
0.16/0.24	    f3(14,15) -> 6*
0.16/0.24	  problem:
0.16/0.24	   
0.16/0.24	  Qed
0.16/0.24	EOF