WORST_CASE(?,O(n^1)) * Step 1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: sum(0()) -> 0() sum(s(x)) -> +(sum(x),s(x)) sum1(0()) -> 0() sum1(s(x)) -> s(+(sum1(x),+(x,x))) - Signature: {sum/1,sum1/1} / {+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {sum,sum1} and constructors {+,0,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(+) = {1}, uargs(s) = {1} Following symbols are considered usable: {sum,sum1} TcT has computed the following interpretation: p(+) = [1] x1 + [0] p(0) = [9] p(s) = [1] x1 + [8] p(sum) = [1] x1 + [10] p(sum1) = [2] x1 + [4] Following rules are strictly oriented: sum(0()) = [19] > [9] = 0() sum(s(x)) = [1] x + [18] > [1] x + [10] = +(sum(x),s(x)) sum1(0()) = [22] > [9] = 0() sum1(s(x)) = [2] x + [20] > [2] x + [12] = s(+(sum1(x),+(x,x))) Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))