WORST_CASE(?,O(n^1)) * Step 1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: add(0(),X) -> X add(s(),Y) -> s() dbl(0()) -> 0() dbl(s()) -> s() first(0(),X) -> nil() first(s(),cons(Y)) -> cons(Y) sqr(0()) -> 0() sqr(s()) -> s() terms(N) -> cons(recip(sqr(N))) - Signature: {add/2,dbl/1,first/2,sqr/1,terms/1} / {0/0,cons/1,nil/0,recip/1,s/0} - Obligation: innermost runtime complexity wrt. defined symbols {add,dbl,first,sqr,terms} and constructors {0,cons,nil ,recip,s} + Applied Processor: NaturalPI {shape = Linear, restrict = NoRestrict, uargs = UArgs, urules = URules, selector = Nothing} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(cons) = {1}, uargs(recip) = {1} Following symbols are considered usable: {add,dbl,first,sqr,terms} TcT has computed the following interpretation: p(0) = 0 p(add) = 11 + 8*x2 p(cons) = x1 p(dbl) = 4 + 2*x1 p(first) = 10 + 2*x1 + 8*x2 p(nil) = 7 p(recip) = 4 + x1 p(s) = 3 p(sqr) = 8 p(terms) = 14 Following rules are strictly oriented: add(0(),X) = 11 + 8*X > X = X add(s(),Y) = 11 + 8*Y > 3 = s() dbl(0()) = 4 > 0 = 0() dbl(s()) = 10 > 3 = s() first(0(),X) = 10 + 8*X > 7 = nil() first(s(),cons(Y)) = 16 + 8*Y > Y = cons(Y) sqr(0()) = 8 > 0 = 0() sqr(s()) = 8 > 3 = s() terms(N) = 14 > 12 = cons(recip(sqr(N))) Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))