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 = Just any strict-rules} + 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 + [6] p(0) = [1] p(s) = [1] x1 + [8] p(sum) = [1] x1 + [8] p(sum1) = [2] x1 + [10] Following rules are strictly oriented: sum(0()) = [9] > [1] = 0() sum(s(x)) = [1] x + [16] > [1] x + [14] = +(sum(x),s(x)) sum1(0()) = [12] > [1] = 0() sum1(s(x)) = [2] x + [26] > [2] x + [24] = s(+(sum1(x),+(x,x))) Following rules are (at-least) weakly oriented: * Step 2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak 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: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))