YES(?,O(n^1))
0.15/0.25	YES(?,O(n^1))
0.15/0.25	
0.15/0.25	Problem:
0.15/0.25	 terms(N) -> cons(recip(sqr(N)))
0.15/0.25	 sqr(0()) -> 0()
0.15/0.25	 sqr(s()) -> s()
0.15/0.25	 dbl(0()) -> 0()
0.15/0.25	 dbl(s()) -> s()
0.15/0.25	 add(0(),X) -> X
0.15/0.25	 add(s(),Y) -> s()
0.15/0.25	 first(0(),X) -> nil()
0.15/0.25	 first(s(),cons(Y)) -> cons(Y)
0.15/0.25	
0.15/0.25	Proof:
0.15/0.25	 Bounds Processor:
0.15/0.25	  bound: 1
0.15/0.25	  enrichment: match
0.15/0.25	  automaton:
0.15/0.25	   final states: {10,9,8,7,6}
0.15/0.25	   transitions:
0.15/0.25	    cons1(5) -> 10*
0.15/0.25	    cons1(12) -> 6*
0.15/0.25	    cons1(2) -> 10*
0.15/0.25	    cons1(4) -> 10*
0.15/0.25	    cons1(1) -> 10*
0.15/0.25	    cons1(3) -> 10*
0.15/0.25	    nil1() -> 10*
0.15/0.25	    s1() -> 11,9,8,7
0.15/0.25	    01() -> 11,8,7
0.15/0.25	    recip1(11) -> 12*
0.15/0.25	    sqr1(5) -> 11*
0.15/0.25	    sqr1(2) -> 11*
0.15/0.25	    sqr1(4) -> 11*
0.15/0.25	    sqr1(1) -> 11*
0.15/0.25	    sqr1(3) -> 11*
0.15/0.25	    terms0(5) -> 6*
0.15/0.25	    terms0(2) -> 6*
0.15/0.25	    terms0(4) -> 6*
0.15/0.25	    terms0(1) -> 6*
0.15/0.25	    terms0(3) -> 6*
0.15/0.25	    cons0(5) -> 1*
0.15/0.25	    cons0(2) -> 1*
0.15/0.25	    cons0(4) -> 1*
0.15/0.25	    cons0(1) -> 1*
0.15/0.25	    cons0(3) -> 1*
0.15/0.25	    recip0(5) -> 2*
0.15/0.25	    recip0(2) -> 2*
0.15/0.25	    recip0(4) -> 2*
0.15/0.25	    recip0(1) -> 2*
0.15/0.25	    recip0(3) -> 2*
0.15/0.25	    sqr0(5) -> 7*
0.15/0.25	    sqr0(2) -> 7*
0.15/0.25	    sqr0(4) -> 7*
0.15/0.25	    sqr0(1) -> 7*
0.15/0.25	    sqr0(3) -> 7*
0.15/0.25	    00() -> 3*
0.15/0.25	    s0() -> 4*
0.15/0.26	    dbl0(5) -> 8*
0.15/0.26	    dbl0(2) -> 8*
0.15/0.26	    dbl0(4) -> 8*
0.15/0.26	    dbl0(1) -> 8*
0.15/0.26	    dbl0(3) -> 8*
0.15/0.26	    add0(3,1) -> 9*
0.15/0.26	    add0(3,3) -> 9*
0.15/0.26	    add0(3,5) -> 9*
0.15/0.26	    add0(4,2) -> 9*
0.15/0.26	    add0(4,4) -> 9*
0.15/0.26	    add0(5,1) -> 9*
0.15/0.26	    add0(5,3) -> 9*
0.15/0.26	    add0(5,5) -> 9*
0.15/0.26	    add0(1,2) -> 9*
0.15/0.26	    add0(1,4) -> 9*
0.15/0.26	    add0(2,1) -> 9*
0.15/0.26	    add0(2,3) -> 9*
0.15/0.26	    add0(2,5) -> 9*
0.15/0.26	    add0(3,2) -> 9*
0.15/0.26	    add0(3,4) -> 9*
0.15/0.26	    add0(4,1) -> 9*
0.15/0.26	    add0(4,3) -> 9*
0.15/0.26	    add0(4,5) -> 9*
0.15/0.26	    add0(5,2) -> 9*
0.15/0.26	    add0(5,4) -> 9*
0.15/0.26	    add0(1,1) -> 9*
0.15/0.26	    add0(1,3) -> 9*
0.15/0.26	    add0(1,5) -> 9*
0.15/0.26	    add0(2,2) -> 9*
0.15/0.26	    add0(2,4) -> 9*
0.15/0.26	    first0(3,1) -> 10*
0.15/0.26	    first0(3,3) -> 10*
0.15/0.26	    first0(3,5) -> 10*
0.15/0.26	    first0(4,2) -> 10*
0.15/0.26	    first0(4,4) -> 10*
0.15/0.26	    first0(5,1) -> 10*
0.15/0.26	    first0(5,3) -> 10*
0.15/0.26	    first0(5,5) -> 10*
0.15/0.26	    first0(1,2) -> 10*
0.15/0.26	    first0(1,4) -> 10*
0.15/0.26	    first0(2,1) -> 10*
0.15/0.26	    first0(2,3) -> 10*
0.15/0.26	    first0(2,5) -> 10*
0.15/0.26	    first0(3,2) -> 10*
0.15/0.26	    first0(3,4) -> 10*
0.15/0.26	    first0(4,1) -> 10*
0.15/0.26	    first0(4,3) -> 10*
0.15/0.26	    first0(4,5) -> 10*
0.15/0.26	    first0(5,2) -> 10*
0.15/0.26	    first0(5,4) -> 10*
0.15/0.26	    first0(1,1) -> 10*
0.15/0.26	    first0(1,3) -> 10*
0.15/0.26	    first0(1,5) -> 10*
0.15/0.26	    first0(2,2) -> 10*
0.15/0.26	    first0(2,4) -> 10*
0.15/0.26	    nil0() -> 5*
0.15/0.26	    1 -> 9*
0.15/0.26	    2 -> 9*
0.15/0.26	    3 -> 9*
0.15/0.26	    4 -> 9*
0.15/0.26	    5 -> 9*
0.15/0.26	  problem:
0.15/0.26	   
0.15/0.26	  Qed
0.15/0.26	EOF