WORST_CASE(?,O(n^1)) * Step 1: NaturalMI 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: 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) = [2] p(add) = [13] x1 + [4] x2 + [1] p(cons) = [1] x1 + [0] p(dbl) = [7] x1 + [2] p(first) = [4] x1 + [6] x2 + [1] p(nil) = [0] p(recip) = [1] x1 + [4] p(s) = [2] p(sqr) = [6] x1 + [4] p(terms) = [8] x1 + [10] Following rules are strictly oriented: add(0(),X) = [4] X + [27] > [1] X + [0] = X add(s(),Y) = [4] Y + [27] > [2] = s() dbl(0()) = [16] > [2] = 0() dbl(s()) = [16] > [2] = s() first(0(),X) = [6] X + [9] > [0] = nil() first(s(),cons(Y)) = [6] Y + [9] > [1] Y + [0] = cons(Y) sqr(0()) = [16] > [2] = 0() sqr(s()) = [16] > [2] = s() terms(N) = [8] N + [10] > [6] N + [8] = cons(recip(sqr(N))) Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))