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	 terms(N) -> cons(recip(sqr(N)))
0.16/0.24	 sqr(0()) -> 0()
0.16/0.24	 sqr(s()) -> s()
0.16/0.24	 dbl(0()) -> 0()
0.16/0.24	 dbl(s()) -> s()
0.16/0.24	 add(0(),X) -> X
0.16/0.24	 add(s(),Y) -> s()
0.16/0.24	 first(0(),X) -> nil()
0.16/0.24	 first(s(),cons(Y)) -> cons(Y)
0.16/0.24	
0.16/0.24	Proof:
0.16/0.24	 Bounds Processor:
0.16/0.24	  bound: 2
0.16/0.24	  enrichment: match
0.16/0.24	  automaton:
0.16/0.24	   final states: {11}
0.16/0.24	   transitions:
0.16/0.24	    cons1(15) -> 11*
0.16/0.24	    cons1(11) -> 11*
0.16/0.24	    nil1() -> 11*
0.16/0.24	    s1() -> 14,11
0.16/0.24	    01() -> 14,11
0.16/0.24	    recip1(14) -> 15*
0.16/0.24	    sqr1(11) -> 14*
0.16/0.24	    s2() -> 14*
0.16/0.24	    02() -> 14*
0.16/0.24	    terms0(11) -> 11*
0.16/0.24	    cons0(11) -> 11*
0.16/0.24	    recip0(11) -> 11*
0.16/0.24	    sqr0(11) -> 11*
0.16/0.24	    00() -> 11*
0.16/0.24	    s0() -> 11*
0.16/0.24	    dbl0(11) -> 11*
0.16/0.24	    add0(11,11) -> 11*
0.16/0.24	    first0(11,11) -> 11*
0.16/0.24	    nil0() -> 11*
0.16/0.24	  problem:
0.16/0.24	   
0.16/0.24	  Qed
0.16/0.25	EOF