WORST_CASE(?,O(n^1)) * Step 1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: 2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1))) 2nd(cons1(X,cons(Y,Z))) -> Y activate(X) -> X activate(n__from(X)) -> from(X) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) - Signature: {2nd/1,activate/1,from/1} / {cons/2,cons1/2,n__from/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {2nd,activate,from} and constructors {cons,cons1,n__from ,s} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 1 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(2nd) = {1}, uargs(cons1) = {2} Following symbols are considered usable: {2nd,activate,from} TcT has computed the following interpretation: p(2nd) = [1 4] x1 + [1] [4 4] [6] p(activate) = [1 1] x1 + [2] [0 1] [1] p(cons) = [1 2] x1 + [1 1] x2 + [0] [0 0] [0 0] [2] p(cons1) = [1 2] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] p(from) = [1 2] x1 + [4] [0 0] [4] p(n__from) = [1 2] x1 + [0] [0 0] [3] p(s) = [0] [0] Following rules are strictly oriented: 2nd(cons(X,X1)) = [1 2] X + [1 1] X1 + [9] [4 8] [4 4] [14] > [1 2] X + [1 1] X1 + [3] [4 8] [4 4] [14] = 2nd(cons1(X,activate(X1))) 2nd(cons1(X,cons(Y,Z))) = [1 2] X + [1 2] Y + [1 1] Z + [1] [4 8] [4 8] [4 4] [6] > [1 0] Y + [0] [0 1] [0] = Y activate(X) = [1 1] X + [2] [0 1] [1] > [1 0] X + [0] [0 1] [0] = X activate(n__from(X)) = [1 2] X + [5] [0 0] [4] > [1 2] X + [4] [0 0] [4] = from(X) from(X) = [1 2] X + [4] [0 0] [4] > [1 2] X + [3] [0 0] [2] = cons(X,n__from(s(X))) from(X) = [1 2] X + [4] [0 0] [4] > [1 2] X + [0] [0 0] [3] = n__from(X) Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))