YES(?,O(n^1))
0.16/0.23	YES(?,O(n^1))
0.16/0.23	
0.16/0.23	Problem:
0.16/0.23	 f(0()) -> cons(0(),n__f(s(0())))
0.16/0.23	 f(s(0())) -> f(p(s(0())))
0.16/0.23	 p(s(0())) -> 0()
0.16/0.23	 f(X) -> n__f(X)
0.16/0.23	 activate(n__f(X)) -> f(X)
0.16/0.23	 activate(X) -> X
0.16/0.23	
0.16/0.23	Proof:
0.16/0.23	 Bounds Processor:
0.16/0.23	  bound: 2
0.16/0.23	  enrichment: match
0.16/0.23	  automaton:
0.16/0.23	   final states: {8}
0.16/0.23	   transitions:
0.16/0.23	    f1(15) -> 8*
0.16/0.23	    f1(8) -> 8*
0.16/0.23	    n__f1(13) -> 14*
0.16/0.23	    n__f1(8) -> 8*
0.16/0.23	    01() -> 8,12
0.16/0.23	    p1(13) -> 15*
0.16/0.23	    s1(12) -> 13*
0.16/0.23	    cons1(12,14) -> 8*
0.16/0.23	    n__f2(15) -> 8*
0.16/0.23	    n__f2(18) -> 19*
0.16/0.23	    n__f2(8) -> 8*
0.16/0.23	    02() -> 15,17
0.16/0.23	    f0(8) -> 8*
0.16/0.23	    cons2(17,19) -> 8*
0.16/0.23	    00() -> 8*
0.16/0.23	    s2(17) -> 18*
0.16/0.23	    cons0(8,8) -> 8*
0.16/0.23	    n__f0(8) -> 8*
0.16/0.23	    s0(8) -> 8*
0.16/0.23	    p0(8) -> 8*
0.16/0.23	    activate0(8) -> 8*
0.16/0.23	  problem:
0.16/0.23	   
0.16/0.23	  Qed
0.16/0.24	EOF